Open ajewellamz opened 1 month ago
Sequence slices should avoid conversions to and from DafnyInt when possible
Given the code
function FindLength(s : seq<uint8>) : (ret : Result<uint64, Error>) method CheckSeq(bytes : seq<uint8>) { var result := FindLength(bytes); if result.Success? { var new_bytes := bytes[0..result.value]; ... }
The slice operation is generated as
let mut new_bytes: Sequence<u8> = bytes.slice(&int!(0), &Into::<DafnyInt>::into(result.value().clone()));
which unnecessarily converts the two numbers into DafnyInts, only to be converted back to native numbers in Sequence::slice.
Instead generate
let mut new_bytes: Sequence<u8> = bytes.slice_usize(0, result.value().clone() as usize);
where Sequence::slice_usize is the obvious extension of Sequence::slice
pub fn slice_usize(&self, start_index: usize, end_index: usize) -> Sequence<T> { let new_data = Sequence::from_array_owned(self.to_array()[start_index..end_index].to_vec()); new_data }
No response
@ajewellamz I edited your description just to add code blocks because I was having trouble parsing it, hope you don't mind. :)
Summary
Sequence slices should avoid conversions to and from DafnyInt when possible
Background and Motivation
Given the code
The slice operation is generated as
which unnecessarily converts the two numbers into DafnyInts, only to be converted back to native numbers in Sequence::slice.
Proposed Feature
Instead generate
where Sequence::slice_usize is the obvious extension of Sequence::slice
Alternatives
No response