rem/enriching-properties

[mccleeary-galois]

Adding additional notation to properties and new command to be able to check those properties with the options specified.

[weaversa]

May I suggest using doc comments to separate out REPL commands (like how Rust does doc tests -- https://doc.rust-lang.org/rustdoc/write-documentation/documentation-tests.html)?

/**
 * This property checks that ...
 *
 * ```
 * :check t0
 * ``` 
 */
property t0 = True

/**
 * This property demonstrates ... about the following polymorphic property.
 *
 * ```
 * :prove t1 `{a=1}
 * :prove t1 `{a=2}
 * ```
 */
t1 : {a} (1 <= a, a <= 2) => [a] -> Bit
property t1 x = True

What's nice about this is that the doc comments can exist on more than just propertys, and can demonstrate how functions are to be used, for example, sign then verify.

[eddywestbrook]

@weaversa One of the issues with the code fences approach that we were trying to talk about with you and @WeeknightMVP the other day is that listing REPL commands doesn't really associate any structure to the assurance case. Instead, we are trying to structure the assurance case for properties so you can e.g. write queries over all properties that are checked but not proved, or all properties that are proved with Z3 and not yices (if your system doesn't have yices installed), etc.