Concrete syntax for Hoare triples

hoare[ P ==> Q ] { … } is the triple hoareStmt P p Q, where the body is parsed by the statement parser of ProgramSyntax.lean (the same one proc and the module syntax use):

hoare[ §x = 1 ==> §x = 2 ] {
  var u : Nat;
  let one := 1;
  u <- $x + one;
  x <- $u;
}

Like a proc body, the block may open with var declarations and may contain Lean binders (let/have/letI/haveI) in statement position. Both kinds of binder are repeated around P and Q: the vars (as letIs, exactly as in the body) and the binders on the spine of the statement sequence (ProgramSyntax.wrapSpineBinders, which is what proc does for its return value). So a precondition or postcondition may mention the local program variables and the body's lets. A var x : T binds x to its local slot localVarLens "x" T, so §x in a condition is literally the term the body reads and writes; the type comes from the declaration.

P and Q are ordinary GaudiExpr[ ] expressions of type Prop, so program variables are read with the $/§ sigil. The state they are read at is the whole ProgramState (globals and locals); a triple about a procedure is the second form below.

Both forms also print in this surface syntax, and round-trip: the delaborators are at the end of each of the two sections below, and like the ones in ProgramSyntax.lean they step aside under pp.gaudisCrypt false and whenever the term is not of the shape the notation builds.

Concrete syntax for procedure triples

hoare[ M (x, m) : P ==> Q ] is hoareProc P' M.procedure Q', where M is a procedure module (or a bare Procedure) and x, m name its parameters:

hoare[ S.commit (x, m) : §x = §h ==> §res ≠ §h ]

The precondition sees the parameters and the globals, the postcondition res and the globals — hoareProc's own shape, which does not give the postcondition the entry parameters. A property relating the result to an argument is not a hoareProc triple and has to be stated another way (save the argument into a global, or use a relational judgment); EasyCrypt imposes the same restriction.

Everything is read with the sigil, parameters included: §x for a parameter, §y for a global, §res for the result and §params for the whole argument tuple. One spelling for every variable, so a condition can be lifted out of a procedure body unchanged.

The parameter names may be left out — hoare[ S.commit : … ] — in which case they are looked up in the @[gaudiProcParamNames] attribute that moduletype and module record them in. Names written at the triple win over the recorded ones, with a warning if they disagree; an explicit () asserts that the procedure takes none. Without recorded names, they are read off the procedure itself if its parameterNames reduce to a literal list (as for a proc literal); a procedure whose names cannot be found either way (a variable, say) has to have them written.

M is parsed at term:max, so an applied module expression needs parentheses: hoare[ (Module.app X A) (x) : … ]. Without that, M (x, m) would parse as an application and swallow the parameter list.

There is no { … } block in this form: no body is written at the triple, and the procedure's own locals are invisible to hoareProc, so there is nothing for a var to declare. A Lean let/have in front of the triple scopes over both conditions.

How it elaborates

The two conditions are plain lambdas of exactly the shape hoareProc asks for:

hoareProc (sig := ‹sig›)
  (fun args σ =>
    let params : Getter _ ProgramState := Getter.mk fun _ => args
    let x : Getter _ ProgramState := Getter.mk fun _ => (Lens.id.ofst).get args
    let m : Getter _ ProgramState := Getter.mk fun _ => (Lens.id.osnd).get args
    (GaudiExpr[ P ] : Getter Prop ProgramState).get ⟨σ, VariableAssignment.init⟩)
  (Module.Proc.procedure M)
  (fun res σ =>
    let res : Getter _ ProgramState := Getter.mk fun _ => res
    (GaudiExpr[ Q ] : Getter Prop ProgramState).get ⟨σ, VariableAssignment.init⟩)

Points worth knowing:

• GaudiExpr[ ] reads from a ProgramState (that is CurrentState's field type), so the condition is read at ⟨σ, VariableAssignment.init⟩: the globals of the triple, and locals that no condition can mention (there is no var here). Globals resolve through the Evaluatable (Lens T VariableAssignment) T instance. The parameters and the result are not locals of this state but getters that ignore it, so no argument tuple has to be packed into the state and the result never has to masquerade as a variable.
• A parameter's getter is the projection (mkChain (navSteps k n)).get args out of the argument tuple sig.ParamType. It is not the callee's slot localVarLens "x" T: under hoareProc's shape the precondition is about the argument tuple, not about the callee's entry frame (stating it over that frame would change hoareProc's type).
• The parameter binders are plain lets, not letIs: they have to survive elaboration, so that a condition mentioning a parameter prints as §x rather than as the inlined slot getter, and so that the written names stay recoverable from the term. Every name is bound whether a condition uses it or not; the binder idents carry no source position, so an unmentioned one does not trip the unused-variable linter.
• sig is passed explicitly, because ProcedureSignature.ParamType ?sig ≟ A × B does not determine ?sig. This is a term elaborator rather than a macro for that reason: it elaborates M first, and then has sig as an Expr to hand to exprToSyntax — which is also how the binder types args : sig.ParamType and res : sig.ret get written without reconstructing any type syntax.

Why hoare[ and not hoare [

The leading atom is glued to the bracket on purpose. A term-level syntax cannot start with a non-reserved identifier-like atom — Lean's leading-parser table never reaches it, so a production opening with &"hoare" is simply never tried — and the spaced form hoare [ … ] would therefore have to make hoare a reserved keyword. Gluing makes hoare[ a token of its own and leaves the bare word hoare available as an ordinary identifier (a keyword is banned in every position, binders and unfold/attribute arguments included, and a constant so named prints as «hoare»). EasyCrypt spells its triples hoare[ … : pre ==> post ], so this is also the familiar form.

The underlying definition is hoareStmt, not hoare, so reserving the keyword would no longer collide with anything today — the spaced form is available should we want it, at the price of that project-wide reservation.

def GaudisCrypt.«termHoare[_==>_]{_Var_;__}» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

Printing a statement triple

hoareStmt A p B prints as hoare[ P ==> Q ] { … } whenever the body prints as statements. A condition of the shape the macro builds — a GaudiExpr[ ] getter under exactly the let/have binders on the body's spine — prints as the P it was written as. Any other condition c : ProgramState → Prop (one a rewrite or dsimp produced, say) prints as c CurrentState.state, β-reduced, which re-elaborates to c up to η. If c mentions its argument inside a nested GaudiExpr[ ], where CurrentState.state would read the nested state, it prints as let σ := CurrentState.state; c σ instead (ProgramSyntax.getterViaState, which also prints the expression slots of statements that are not of the shape the macros build).

A condition without the spine binders is printed as it is, and the macro wraps it in them again. That is sound when it mentions none of their names, and otherwise the delaborator steps aside.

The vars are recovered the way the proc delaborator recovers them (see "Program variables" in ProgramSyntax.lean), over the body and both conditions together: a slot localVarLens "x" T is one variable wherever it occurs in the three, so §x in a condition and x in the body print under the same name and the same var line.

Procedure triples

def GaudisCrypt.«termHoare[_(_):_==>_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def GaudisCrypt.knownParamNames? (p : Lean.Expr) : Lean.MetaM (Option (Array Lean.Name))

The parameter names of the procedure p that can be found without being written: the ones @[gaudiProcParamNames] records (on M for p = Module.Proc.procedure M), else p.parameterNames if it reduces to a literal list (a proc literal, say).

Equations

• One or more equations did not get rendered due to their size.

Printing a procedure triple

hoareProc A p B prints as hoare[ M (x, y) : P ==> Q ] when both conditions have the shape the elaborator builds: fun args σ => let … ; (GaudiExpr[ P ]).get ⟨σ, ()⟩, with one Getter.mk let per bound name. The shape is checked on the raw term, which is also where the two things a printed triple could otherwise get wrong are ruled out: that the condition is read at this triple's σ and not at some other state in scope, and that it goes through the let-bound getters rather than mentioning args/σ itself (neither has a surface spelling).

The parameter names are always printed, whether they were written at the triple or taken from the callee's @[gaudiProcParamNames] — printing them is faithful either way, and does not depend on the attribute still being there.

From a procedure triple to a statement triple

hoareProcToStmt is hoareProc_as_hoareStmt as a conversion — in the shape of an Isabelle conv (cterm -> thm), Expr → MetaM Simp.Result: the term it rewrites to and the proof of the equation. The two lenses the lemma quantifies over are chosen here: one local variable per parameter of the procedure, under the parameter's name, and one for the result, so that the statement prints as

hoare[ P ==> Q ] { var res : R, x : X, y : Y; res <- call p (§x, §y); }

The signature is read off the term, so the Nonempty instances the slots need are found at the concrete types.

def GaudisCrypt.hoareProcToStmt (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

hoareProc A p B ↦ the hoareStmt about res <- call p (x₁, …, xₙ);, with one local variable per parameter of p (see the section docstring), and the proof of the equation.

The conditions are A/B applied to the reads of the slots, with their lets substituted (the procedure-triple notation binds the parameter names, which would shadow the variables) and the parameter projections reduced, so that the parameter x reads as the variable §x; then put in the shape GaudiExpr[ P ].get by ProgramSyntax.getterViaState.

Equations

• One or more equations did not get rendered due to their size.

def GaudisCrypt.tacticHoare_proc_to_stmt : Lean.ParserDescr

Rewrite a goal hoareProc A p B to the hoareStmt about res <- call p (x₁, …, xₙ);, one local variable per parameter — the conversion hoareProcToStmt applied to the goal.

Equations

• GaudisCrypt.tacticHoare_proc_to_stmt = Lean.ParserDescr.node `GaudisCrypt.tacticHoare_proc_to_stmt 1024 (Lean.ParserDescr.nonReservedSymbol "hoare_proc_to_stmt" false)