search

FStarLang / pulse

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

Use gensym from F* #235

Closed gebner closed 1 month ago

gebner commented 1 month ago

In Pulse, we create free variables to open terms (mainly to check abs terms) and then expect to be able to call F on those opened terms containing free variables created in Pulse (to normalize, to check equivalence, and to check typing). For this to work, F must not create variables that clash with Pulse's. (Otherwise the names can clash and we get bugs like #234.)

This PR changes the fresh function in Pulse.Typing.Env to use the F* gensym.

The typing of fresh is a bit questionable now. It promises to return a variable not present in the Pulse environment but that will only be true if all variables were created with fresh. But I suspect that the reflection API requires changes to address the name clash issue (e.g. equiv tokens probably allow you to derive false from a name clash) and this fix here should be workable until we have a proper solution across the board.

The fresh function also has the Dv effect now since it is non-deterministic; this propagates quite a bit (since typing judgements contain free variables) but it doesn't change much since those functions are used from tactics.

Fixes #234.

gebner commented 1 month ago

Aseem is happy with the change and it's blocking me, so I'm merging this.