search

FStarLang / pulse

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

Correctly extract inner ghost functions. #241

Closed gebner closed 1 month ago

gebner commented 1 month ago

Inner ghost functions used to be extracted as Obj.magic (fun _ -> ()) (that's the definition, not the call site). Changing the let to have a pure effect allows extraction to remove the definition and the associated magic (which in turn breaks pulse2rust).

More generally, I'm not sure if we need to put a DIV-effect on let-bindings with a C_Tot effect at all.

gebner commented 1 month ago

This is a repeat of #182. Guido added a test case there, but that test didn't catch this. The slices code used to break pulse2rust and serves as another test.