Tests for ProgramSyntax

Experiments for programs

axiom GaudisCrypt.ProgTest.a [ProgramSpec] : Lens ℕ State

axiom GaudisCrypt.ProgTest.b [ProgramSpec] : Lens ℕ State

axiom GaudisCrypt.ProgTest.c [ProgramSpec] : Lens Bool State

axiom GaudisCrypt.ProgTest.d [ProgramSpec] : Lens ℕ State

axiom GaudisCrypt.ProgTest.a_b_disjoint [ProgramSpec] : disjoint a b

axiom GaudisCrypt.ProgTest.a_d_disjoint [ProgramSpec] : disjoint a d

axiom GaudisCrypt.ProgTest.b_d_disjoint [ProgramSpec] : disjoint b d

noncomputable def GaudisCrypt.ProgTest.prog_assign [ProgramSpec] : Stmt Unit

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 [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.prog_while [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.prog_sample [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.split [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.split2 [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.split3 [ProgramSpec] : Stmt Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

noncomputable def GaudisCrypt.ProgTest.prog_call [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.prog_call2 [ProgramSpec] : Stmt Unit

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 [ProgramSpec] : Stmt Unit

Equations

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

noncomputable def GaudisCrypt.ProgTest.proc_with_hole [ProgramSpec] : 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 [ProgramSpec] : proctype (ℕ) → ℕ uses ((ℕ) → Bool, (Bool) → ℕ)

Equations

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

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.«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.