Tests for ProgramSyntax

Experiments for programs

axiom GaudisCrypt.ProgTest.a : Lens ℕ VariableAssignment

axiom GaudisCrypt.ProgTest.b : Lens ℕ VariableAssignment

axiom GaudisCrypt.ProgTest.c : Lens Bool VariableAssignment

axiom GaudisCrypt.ProgTest.d : Lens ℕ VariableAssignment

axiom GaudisCrypt.ProgTest.a_b_disjoint : a.Disjoint b

axiom GaudisCrypt.ProgTest.a_d_disjoint : a.Disjoint d

axiom GaudisCrypt.ProgTest.b_d_disjoint : b.Disjoint d

noncomputable def GaudisCrypt.ProgTest.prog_assign : Stmt

Equations

• GaudisCrypt.ProgTest.prog_assign = GaudiProg[ GaudisCrypt.ProgTest.a <- §GaudisCrypt.ProgTest.a + 1; GaudisCrypt.ProgTest.b <- §GaudisCrypt.ProgTest.a + §GaudisCrypt.ProgTest.b; ]

noncomputable def GaudisCrypt.ProgTest.prog_if : Stmt

Equations

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

noncomputable def GaudisCrypt.ProgTest.prog_while : Stmt

Equations

• GaudisCrypt.ProgTest.prog_while = GaudiProg[ while (§GaudisCrypt.ProgTest.a == 0) { GaudisCrypt.ProgTest.a <- §GaudisCrypt.ProgTest.a + 1; } ]

noncomputable def GaudisCrypt.ProgTest.prog_sample : Stmt

Equations

• GaudisCrypt.ProgTest.prog_sample = GaudiProg[ GaudisCrypt.ProgTest.c <$ GaudisCrypt.SubProbability.uniform; ]

noncomputable def GaudisCrypt.ProgTest.split : Stmt

Equations

• GaudisCrypt.ProgTest.split = GaudiProg[ GaudisCrypt.ProgTest.a, GaudisCrypt.ProgTest.b <- (1, 2); ]

noncomputable def GaudisCrypt.ProgTest.split2 : Stmt

Equations

• GaudisCrypt.ProgTest.split2 = GaudiProg[ GaudisCrypt.ProgTest.a, GaudisCrypt.ProgTest.b <- (1, 2); ]

noncomputable def GaudisCrypt.ProgTest.split3 : Stmt

Equations

• GaudisCrypt.ProgTest.split3 = GaudiProg[ (GaudisCrypt.ProgTest.a, GaudisCrypt.ProgTest.b), GaudisCrypt.ProgTest.d <- ((1, 3), 2); ]

noncomputable def GaudisCrypt.ProgTest.proc_inc : proctype (ℕ) -> ℕ

Equations

• GaudisCrypt.ProgTest.proc_inc = proc (x : ℕ) : ℕ { skip; return §x + 1 }

noncomputable def GaudisCrypt.ProgTest.proc_sum : proctype (ℕ, ℕ) -> ℕ

Equations

• GaudisCrypt.ProgTest.proc_sum = proc (x : ℕ, y : ℕ) : ℕ { var u : ℕ; u <- §x + §y; return §u }

noncomputable def GaudisCrypt.ProgTest.proc_loop : proctype () -> ℕ

Equations

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

noncomputable def GaudisCrypt.ProgTest.prog_call : Stmt

Equations

• GaudisCrypt.ProgTest.prog_call = GaudiProg[ GaudisCrypt.ProgTest.a <- call GaudisCrypt.ProgTest.proc_inc (§GaudisCrypt.ProgTest.a); ]

noncomputable def GaudisCrypt.ProgTest.prog_call2 : Stmt

Equations

• GaudisCrypt.ProgTest.prog_call2 = GaudiProg[ GaudisCrypt.ProgTest.a <- call GaudisCrypt.ProgTest.proc_sum (§GaudisCrypt.ProgTest.a, §GaudisCrypt.ProgTest.b); ]

noncomputable def GaudisCrypt.ProgTest.prog_call_void : Stmt

Equations

• GaudisCrypt.ProgTest.prog_call_void = GaudiProg[ call GaudisCrypt.ProgTest.proc_inc (§GaudisCrypt.ProgTest.a); ]

noncomputable def GaudisCrypt.ProgTest.proc_with_hole : proctype (ℕ) → ℕ uses ((ℕ) → ℕ)

Equations

• GaudisCrypt.ProgTest.proc_with_hole = proc (x : ℕ) uses (A : (ℕ) → ℕ) : ℕ { var y : ℕ; y <- call A (§x); return §y }

noncomputable def GaudisCrypt.ProgTest.proc_two_holes : proctype (ℕ) → ℕ uses ((ℕ) → Bool, (Bool) → ℕ)

Equations

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

axiom GaudisCrypt.ProgTest.procAxiomatized : proctype (ℕ, ℕ) → Bool

Printing and round-tripping

#roundtrip t prints t with the delaborators of ProgramSyntax.lean, parses the printed text again and checks that what comes back is definitionally equal to t. The printed text is logged and pinned by the #guard_msgs docstrings — a delaborator that quietly gave up (so that Lean printed the raw constructor term) would still round-trip, but would not print the surface syntax, and the docstring catches that.

def GaudisCrypt.ProgTest.roundtrip (e : Lean.Expr) : Lean.Elab.TermElabM String

Print e, parse the printed text, elaborate it at e's type, and check the result is defeq to e. Returns the printed text. (Also used by the flattening tests, on what they produce.)

Equations

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

def GaudisCrypt.ProgTest.«command#roundtrip_» : Lean.ParserDescr

#roundtrip t: print t, parse the printed text, elaborate it, and check the result is defeq to t. Logs the printed text.

Equations

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

Program variables

A parameter or var stands for its slot localVarLens "x" T in the locals; printing turns the slots back into names where it can.

Statements the macros did not build

A statement built by hand or left behind by a rewrite prints as well, as long as its l-values are lenses.

Rejected declarations