search

FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Remove `slice_pair` in favor of standard F* pairs #247

Closed tahina-pro closed 2 weeks ago

tahina-pro commented 2 weeks ago

The ongoing extension of Karamel by @msprotz and @R1kM to support extraction to Rust stumbles on the slice_pair type, which foils mutability analysis: the same type cannot be used to represent both mutable and immutable slice pairs.

Instead, Jonathan proposes to retire this type in favor of using standard F* pairs, which Karamel would then extract to standard Rust pairs with proper mutability per use.

gebner commented 2 weeks ago

LGTM! Karamel was the only reason we had them in the first place, if Jonathan is fixing that then I'm glad we can switch to normal pairs!

tahina-pro commented 2 weeks ago

I can confirm C extraction works well. Thanks Gabriel!

msprotz commented 2 weeks ago

If bump again into the issue you apparently had before with native pairs, please send a repro. Thanks!