search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.67k stars 231 forks source link

Better support for sladmit #2239

Open R1kM opened 3 years ago

R1kM commented 3 years ago

Some uses of sladmit block progress in scheduling constraints, for instance when the post of the previous computation contains an unresolved frame.

Proposed solution: Provide a special treatment for sladmit in framing by adding an attribute admit to its implicit pre/post, and preprocessing admitted slprops using reflexivity before jumping in the tactic.

R1kM commented 3 years ago

Commit 81a756 improves the situation slightly, allowing for instance to sladmits to be composed, by handling sladmit uvars first through reflexivity, before scheduling constraints

One problem that remains occurs when actual Steel computations separate two calls to sladmit.

Consider for instance ... sladmit (); write r1 0; write r2 0; sladmit (); ...

The problem is that the composition write r1 0; write r2 0 will contain two frames to infer, but the postcondition of the first sladmit and the precondition of the second sladmit will be uvars, hence frames will not be constrained enough to be inferred.

It seems like the only solution for this would be to implement AC-unification instead of AC-matching, with the simplification that we would still have only one frame uvar on both sides.