Concrete syntax for expressions

Surface syntax for the expressions of the imperative probabilistic language; see syntax-ideas.md for design notes.

Expressions — GaudiExpr[ e ]

Wraps a Lean expression e as a program expression. Inside, the $ sigil reads program variables:

• $x — the value of program variable / lens x;
• $(e) — the value of an arbitrary lens-valued term e.

e.g. GaudiExpr[ $a + $b * 2 ]. Every expression position in a statement is already an GaudiExpr, so $ may be used directly there (see ProgramSyntax.lean).

§x is a second spelling of $x, with the same meaning. It exists because it can be printed: $x parses as a Lean antiquotation node, and antiquotation nodes cannot be pretty-printed ($a + 1 fails to format), so §x is what the delaborators emit.

Ambient current state + variable evaluation

An expression of value type T living in a statement with local-state S is a Getter T (State × S). Inside the body we make the current state available via the typeclass CurrentState S, so a program variable x (a lens/getter) can be read as a plain value with eval x. eval accepts both global variables (into State) and full-current-state variables (into State × S); dispatch is on the concrete type of the argument (see Evaluatable).

class GaudisCrypt.CurrentState [ProgramSpec] (S : outParam Type) : Type u_1

The ambient current state State × S. The local-state type S is an outParam: [CurrentState S] resolves by reading off the ambient state's type, so S need not be known up front — this is what lets a global variable, whose type says nothing about S, still be evaluated.

• state : ProcedureState S

class GaudisCrypt.Evaluatable [ProgramSpec] (S X : Type) (T : outParam Type) : Type u_1

Anything that can be read to a value T in the ambient CurrentState S: program variables (lenses/getters into State, or into the full ProcedureState S), and anything users later add instances for. Dispatch is on the concrete type X of the argument, so resolution is never stuck on a metavariable.

• eval : ProcedureState S → X → T

def GaudisCrypt.eval [ProgramSpec] {S X T : Type} [Evaluatable S X T] [cs : CurrentState S] (x : X) : T

User-facing variable read, with S implicit (inferred from the variable's container in the full case, from the ambient CurrentState in the global case). Pass (S := …) to force a particular state.

Equations

• §x = GaudisCrypt.Evaluatable.eval GaudisCrypt.CurrentState.state x

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableGetterState [ProgramSpec] {S T : Type} : Evaluatable S (Getter T State) T

The four container shapes, dispatched directly on the argument type. (No Lens → Getter forwarder: it would overlap these, so we spell out all four.)

Equations

• GaudisCrypt.instEvaluatableGetterState = { eval := fun (cs : GaudisCrypt.ProcedureState S) (x : GaudisCrypt.Getter T GaudisCrypt.State) => x.get cs.global }

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableGetterProcedureState [ProgramSpec] {S T : Type} : Evaluatable S (Getter T (ProcedureState S)) T

Equations

• GaudisCrypt.instEvaluatableGetterProcedureState = { eval := fun (cs : GaudisCrypt.ProcedureState S) (x : GaudisCrypt.Getter T (GaudisCrypt.ProcedureState S)) => x.get cs }

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableLensState [ProgramSpec] {S T : Type} : Evaluatable S (Lens T State) T

Equations

• GaudisCrypt.instEvaluatableLensState = { eval := fun (cs : GaudisCrypt.ProcedureState S) (x : GaudisCrypt.Lens T GaudisCrypt.State) => x.get cs.global }

@[implicit_reducible]

instance GaudisCrypt.instEvaluatableLensProcedureState [ProgramSpec] {S T : Type} : Evaluatable S (Lens T (ProcedureState S)) T

Equations

• GaudisCrypt.instEvaluatableLensProcedureState = { eval := fun (cs : GaudisCrypt.ProcedureState S) (x : GaudisCrypt.Lens T (GaudisCrypt.ProcedureState S)) => x.get cs }

Reduction lemmas (so denotations compute)

simp reduces all four cases (global/full × getter/lens) to a plain .get read. Making S a real parameter (rather than a cs.L projection) is what lets the full-state lemmas match under simp.

@[simp]

theorem GaudisCrypt.eval_getter_global [ProgramSpec] {S T : Type} [cs : CurrentState S] (x : Getter T State) : §x = x.get CurrentState.state.global

@[simp]

theorem GaudisCrypt.eval_getter_full [ProgramSpec] {S T : Type} [cs : CurrentState S] (x : Getter T (ProcedureState S)) : §x = x.get CurrentState.state

@[simp]

theorem GaudisCrypt.eval_lens_global [ProgramSpec] {S T : Type} [cs : CurrentState S] (x : Lens T State) : §x = x.get CurrentState.state.global

@[simp]

theorem GaudisCrypt.eval_lens_full [ProgramSpec] {S T : Type} [cs : CurrentState S] (x : Lens T (ProcedureState S)) : §x = x.get CurrentState.state

Sigil syntax for expressions

The $ sigil is parsed by Lean as a (pseudo) antiquotation node; we intercept those nodes inside the GaudiExpr[ ] macro and rewrite $e to eval e.

$x ↦ eval x (variable reference) $(e) ↦ eval e (arbitrary lens-valued term as a variable) GaudiExpr[ e ] wraps an expression body e into a Getter _ (State × S), making the ambient CurrentState available inside e.

def GaudisCrypt.«termGaudiExpr[_]» : Lean.ParserDescr

Equations

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

The printable sigil §

$x is an antiquotation node, which Lean's formatter cannot print (it fails inside infix operators, so $a + 1 would be unprintable). §x means exactly the same — it expands to eval x just like $x does — but is an ordinary piece of syntax, so it both parses and prints. The eval unexpander turns every variable read back into it.

def GaudisCrypt.«term§__» : Lean.ParserDescr

§x — the value of program variable / lens x in the ambient CurrentState; the printable spelling of $x.

Equations

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

def GaudisCrypt.unexpandEval : Lean.PrettyPrinter.Unexpander

Equations

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