The file tests/proofs/dexter/dexter.md will contain two/three modules, two for declaring the configuration and the serialization/deserialization rules, and one with the claims.
We need a README-based kprove harness for calling prover on the claims module, but uses the serialization/deserialization/configuration modules the main module.
Note that calling kprove on markdown files currently does not work, we need to address this first, but it shouldn't take too long to do for Radu.
The file
tests/proofs/dexter/dexter.mdwill contain two/three modules, two for declaring the configuration and the serialization/deserialization rules, and one with the claims.We need a README-based kprove harness for calling prover on the claims module, but uses the serialization/deserialization/configuration modules the main module.
Note that calling kprove on markdown files currently does not work, we need to address this first, but it shouldn't take too long to do for Radu.