Rocq Postcondition and Invariants #206
Conversation
| @@ -0,0 +1,323 @@ | |||
| constructor of Token | |||
There was a problem hiding this comment.
Do we have to inline Token or can we use the json config to point at a different file?
There was a problem hiding this comment.
The implementation for reading the json config was created with the HEVM equivalence checking requirements in mind, and, while not difficult, porting it to other modes of Act would require some adjustments. It will be implemented in the future.
| parens (T.pack name <+> envVar <+> arguments i) <+> stateVar | ||
|
|
||
| -- | definition of constructor preconditions | ||
| initPrecs :: Constructor -> T.Text |
There was a problem hiding this comment.
It seems that there are some duplicates in the preconditions for constructors and behaviors. Can we apply a deduplication pass? I'm not sure if this should happen here or earlier when we generate bounds.
|
|
||
| creates | ||
|
|
||
| Token token0 := create Token(200) |
There was a problem hiding this comment.
When we handle pointers in the Rocq backend, let's use the real AMM here that does casting.
2 participants
This PR modifies the Rocq translation to include the postconditions and invariants provided in the Act specifiaction. There is also some restructuring in the Rocq generation code.
Postconditions
For every postcondition of the constructor and of every case of every behaviour, a
Propis generated, which expresses that said postcondition holds after a valid transition.The postconditions are kept separate to allow the user to omit proving any that they do not need, or trust that the SMT solver has validated.
Invariants
The invariants provided in the Act specification are merged into a conjuction in the
invariantsterm.Three other generated terms are of interest:
invariantInit: Given a property P, claims that P holds after a valid constructor execution.invariantStep: Given a property P, claims that if P holds in the prestate of a step transition, then it holdsin the poststate.
invariantReachable: Given a property P and proofs ofinvariantInit PandinvariantStep P, asserts and proves that P is true for any state reachable from an initial state.The above can also be used to prove any invariant, not just those generated from the specification.
Miscellaneous