A separation logic prover for pulse

[aseemr]

Diff in Pulse examples:

• Removes the trailing () from some cases (e.g., in CustomSyntax)
• A function that is not annotated ghost but only contains one ghost command in its body now succeeds, because the typechecker inserts a stateful return

Implementation files to look at:

These two files contain the main type definitions for prover state and type checker result:

• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Base.fsti
• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.Base.fsti

The following is the interface provided by the prover:

https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.fsti

To see a usage for the prover, please see the following implementation of stateful applications (specifically line 127):

https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.STApp.fst

Current prover steps are elim exists, elim pure, intro exists, intro pure, and match:

• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.ElimExists.fsti
• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.ElimPure.fsti
• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.IntroExists.fsti
• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.IntroPure.fsti
• https://github.com/FStarLang/steel/blob/_aseem_prover_integration/lib/steel/pulse/Pulse.Checker.Prover.Match.fsti