Tests for ModuleSyntax

def Experiment.TestModule [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

Equations

• Experiment.TestModule = GaudisCrypt.Module Experiment.TestModule.typeRep

@[reducible]

noncomputable def Experiment.TestModule.mk [GaudisCrypt.ProgramSpec] (s : Structure) : TestModule

Equations

• Experiment.TestModule.mk s = GaudisCrypt.Module.pair' s.main s.aux

noncomputable def Experiment.TestModule.structure [GaudisCrypt.ProgramSpec] (m : TestModule) : Structure

Equations

• m.structure = { main := m.main, aux := m.aux }

noncomputable def Experiment.TestModule.main [GaudisCrypt.ProgramSpec] (m : TestModule) : procmod (String, ℕ) → Bool

Equations

• m.main = GaudisCrypt.Module.fst' m

noncomputable def Experiment.TestModule.main.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities TestModule (procmod (String, ℕ) → Bool) main

Equations

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

@[simp]

theorem Experiment.TestModule.mk_destruct [GaudisCrypt.ProgramSpec] (s : Structure) : (mk s).structure = s

noncomputable def Experiment.TestModule.aux [GaudisCrypt.ProgramSpec] (m : TestModule) : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

Equations

• m.aux = GaudisCrypt.Module.snd' m

def Experiment.TestModule.typeRep : GaudisCrypt.ModuleTypeRep

Equations

• Experiment.TestModule.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig (String, ℕ) → Bool)).prod ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

@[implicit_reducible]

instance Experiment.instIsModuleTestModule [GaudisCrypt.ProgramSpec] : GaudisCrypt.IsModule TestModule

Equations

• Experiment.instIsModuleTestModule = { moduleTypeRep := Experiment.TestModule.typeRep, isModule := ⋯ }

structure Experiment.TestModule.Structure [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

• main : procmod (String, ℕ) → Bool
• aux : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

@[simp]

theorem Experiment.TestModule.destruct_mk [GaudisCrypt.ProgramSpec] (m : TestModule) : mk m.structure = m

noncomputable def Experiment.TestModule.aux.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities TestModule (GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)) aux

Equations

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

@[implicit_reducible]

instance Experiment.instIsModuleOneField [GaudisCrypt.ProgramSpec] : GaudisCrypt.IsModule OneField

Equations

• Experiment.instIsModuleOneField = { moduleTypeRep := Experiment.OneField.typeRep, isModule := ⋯ }

structure Experiment.OneField.Structure [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

• only : procmod (ℕ) → Bool

@[reducible]

noncomputable def Experiment.OneField.mk [GaudisCrypt.ProgramSpec] (s : Structure) : OneField

Equations

• Experiment.OneField.mk s = s.only

def Experiment.OneField [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

Equations

• Experiment.OneField = GaudisCrypt.Module Experiment.OneField.typeRep

def Experiment.OneField.typeRep : GaudisCrypt.ModuleTypeRep

Equations

• Experiment.OneField.typeRep = GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → Bool)

noncomputable def Experiment.OneField.only.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities OneField (procmod (ℕ) → Bool) only

Equations

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

@[simp]

theorem Experiment.OneField.mk_destruct [GaudisCrypt.ProgramSpec] (s : Structure) : (mk s).structure = s

noncomputable def Experiment.OneField.only [GaudisCrypt.ProgramSpec] (m : OneField) : procmod (ℕ) → Bool

Equations

• m.only = m

@[simp]

theorem Experiment.OneField.destruct_mk [GaudisCrypt.ProgramSpec] (m : OneField) : mk m.structure = m

noncomputable def Experiment.OneField.structure [GaudisCrypt.ProgramSpec] (m : OneField) : Structure

Equations

• m.structure = { only := m.only }

noncomputable def Experiment.UnicodeArrowField.g [GaudisCrypt.ProgramSpec] (m : UnicodeArrowField) : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)

Equations

• m.g = GaudisCrypt.Module.snd' m

noncomputable def Experiment.UnicodeArrowField.g.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities UnicodeArrowField (GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)) g

Equations

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

@[simp]

theorem Experiment.UnicodeArrowField.destruct_mk [GaudisCrypt.ProgramSpec] (m : UnicodeArrowField) : mk m.structure = m

def Experiment.UnicodeArrowField [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

Equations

• Experiment.UnicodeArrowField = GaudisCrypt.Module Experiment.UnicodeArrowField.typeRep

@[implicit_reducible]

instance Experiment.instIsModuleUnicodeArrowField [GaudisCrypt.ProgramSpec] : GaudisCrypt.IsModule UnicodeArrowField

Equations

• Experiment.instIsModuleUnicodeArrowField = { moduleTypeRep := Experiment.UnicodeArrowField.typeRep, isModule := ⋯ }

@[reducible]

noncomputable def Experiment.UnicodeArrowField.mk [GaudisCrypt.ProgramSpec] (s : Structure) : UnicodeArrowField

Equations

• Experiment.UnicodeArrowField.mk s = GaudisCrypt.Module.pair' s.f s.g

noncomputable def Experiment.UnicodeArrowField.f [GaudisCrypt.ProgramSpec] (m : UnicodeArrowField) : procmod (ℕ) → Bool

Equations

• m.f = GaudisCrypt.Module.fst' m

structure Experiment.UnicodeArrowField.Structure [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

• f : procmod (ℕ) → Bool
• g : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)

noncomputable def Experiment.UnicodeArrowField.structure [GaudisCrypt.ProgramSpec] (m : UnicodeArrowField) : Structure

Equations

• m.structure = { f := m.f, g := m.g }

@[simp]

theorem Experiment.UnicodeArrowField.mk_destruct [GaudisCrypt.ProgramSpec] (s : Structure) : (mk s).structure = s

noncomputable def Experiment.UnicodeArrowField.f.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities UnicodeArrowField (procmod (ℕ) → Bool) f

Equations

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

def Experiment.UnicodeArrowField.typeRep : GaudisCrypt.ModuleTypeRep

Equations

• Experiment.UnicodeArrowField.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → Bool)).prod ((GaudisCrypt.ModuleTypeRep.proc (procsig (Bool) → ℕ)).arr GaudisCrypt.ModuleTypeRep.unit)

axiom Experiment.testMain [GaudisCrypt.ProgramSpec] : procmod (String, ℕ) → Bool

axiom Experiment.testAux [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc (procsig (ℕ) → String)).arr GaudisCrypt.ModuleTypeRep.unit)

noncomputable def Experiment.myMod [GaudisCrypt.ProgramSpec] : TestModule

Equations

• Experiment.myMod = Experiment.TestModule.mk { main := Experiment.testMain, aux := Experiment.testAux }

theorem Experiment.test [GaudisCrypt.ProgramSpec] : myMod.main = testMain

def Experiment.M2.typeRep : GaudisCrypt.ModuleTypeRep

Equations

• Experiment.M2.typeRep = (GaudisCrypt.ModuleTypeRep.proc (procsig () → Unit)).prod (GaudisCrypt.ModuleTypeRep.proc (procsig () → Unit))

noncomputable def Experiment.M2.g.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities M2 (procmod () → Unit) g

Equations

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

noncomputable def Experiment.M2.h.utilities [GaudisCrypt.ProgramSpec] : GaudisCrypt.ModuleTypeUtilities M2 (procmod () → Unit) h

Equations

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

@[reducible]

noncomputable def Experiment.M2.mk [GaudisCrypt.ProgramSpec] (s : Structure) : M2

Equations

• Experiment.M2.mk s = GaudisCrypt.Module.pair' s.g s.h

noncomputable def Experiment.M2.g [GaudisCrypt.ProgramSpec] (m : M2) : procmod () → Unit

Equations

• m.g = GaudisCrypt.Module.fst' m

@[simp]

theorem Experiment.M2.destruct_mk [GaudisCrypt.ProgramSpec] (m : M2) : mk m.structure = m

def Experiment.M2 [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

Equations

• Experiment.M2 = GaudisCrypt.Module Experiment.M2.typeRep

noncomputable def Experiment.M2.h [GaudisCrypt.ProgramSpec] (m : M2) : procmod () → Unit

Equations

• m.h = GaudisCrypt.Module.snd' m

@[implicit_reducible]

instance Experiment.instIsModuleM2 [GaudisCrypt.ProgramSpec] : GaudisCrypt.IsModule M2

Equations

• Experiment.instIsModuleM2 = { moduleTypeRep := Experiment.M2.typeRep, isModule := ⋯ }

noncomputable def Experiment.M2.structure [GaudisCrypt.ProgramSpec] (m : M2) : Structure

Equations

• m.structure = { g := m.g, h := m.h }

@[simp]

theorem Experiment.M2.mk_destruct [GaudisCrypt.ProgramSpec] (s : Structure) : (mk s).structure = s

structure Experiment.M2.Structure [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

• g : procmod () → Unit
• h : procmod () → Unit

noncomputable def Experiment.X [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) TestModule) M2

Equations

• Experiment.X = ((Experiment.X.g.expression.app (GaudisCrypt.ModuleExpression.var 0).fst).pair Experiment.X.h.expression).abs.toModule ⋯

@[simp]

theorem Experiment.X.h.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

noncomputable def Experiment.X.g.procedure [GaudisCrypt.ProgramSpec] : proctype () → Unit uses (() → Unit)

Equations

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

@[simp]

theorem Experiment.X.h.apply_simp [GaudisCrypt.ProgramSpec] : h = GaudisCrypt.Module.proc procedure

@[simp]

theorem Experiment.X.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : (GaudisCrypt.HoleSigs.empty.append (procsig () → Unit)).Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { call (args GaudisCrypt.HoleIndex.zero) (); call (args GaudisCrypt.HoleIndex.zero) (); call (GaudisCrypt.Module.procedure myMod.main) ("hello", 5); return () }

noncomputable def Experiment.X.h [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.X.h = GaudisCrypt.Module.proc Experiment.X.h.procedure

noncomputable def Experiment.X.g [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (procmod () → Unit)

Equations

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

noncomputable def Experiment.X.h.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.X.h.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.X.g.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app g A = GaudisCrypt.Module.proc (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.nil) (GaudisCrypt.Module.app A myMod).procedure)

@[simp]

theorem Experiment.X.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) : GaudisCrypt.Module.app X (GaudisCrypt.Module.pair A B) = M2.mk { g := GaudisCrypt.Module.app g A, h := h }

noncomputable def Experiment.Y.g [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Arr TestModule (procmod () → Unit))

Equations

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

noncomputable def Experiment.Y [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) TestModule) M2

Equations

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

noncomputable def Experiment.Y.h [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.Y.h = GaudisCrypt.Module.proc Experiment.Y.h.procedure

@[simp]

theorem Experiment.Y.g.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) : GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) B = GaudisCrypt.Module.proc (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.nil) (GaudisCrypt.Module.procedure B.main)) (GaudisCrypt.Module.app A myMod).procedure)

noncomputable def Experiment.Y.h.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.Y.h.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.Y.g.procedure [GaudisCrypt.ProgramSpec] : proctype () → Unit uses ((String, ℕ) → Bool, () → Unit)

Equations

• Experiment.Y.g.procedure = proc () uses (_hole0 : (String, ℕ) → Bool, _hole1 : () → Unit) : Unit { call _hole0 ("hi", 3); call _hole1 (); return () }

@[simp]

theorem Experiment.Y.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) : GaudisCrypt.Module.app Y (GaudisCrypt.Module.pair A B) = M2.mk { g := GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) B, h := h }

@[simp]

theorem Experiment.Y.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : ((GaudisCrypt.HoleSigs.empty.append (procsig (String, ℕ) → Bool)).append (procsig () → Unit)).Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { call (args GaudisCrypt.HoleIndex.zero.succ) ("hi", 3); call (args GaudisCrypt.HoleIndex.zero) (); return () }

@[simp]

theorem Experiment.Y.h.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.Y.h.apply_simp [GaudisCrypt.ProgramSpec] : h = GaudisCrypt.Module.proc procedure

theorem Experiment.M2.mk_g [GaudisCrypt.ProgramSpec] {s : Structure} : (mk s).g = s.g

def Experiment.M3 [GaudisCrypt.ProgramSpec] : Type (max 1 u_1)

Equations

• Experiment.M3 = Experiment.M2

@[simp]

theorem Experiment.NoParams.g.apply_simp [GaudisCrypt.ProgramSpec] : g = GaudisCrypt.Module.proc procedure

noncomputable def Experiment.NoParams.g [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.NoParams.g = GaudisCrypt.Module.proc Experiment.NoParams.g.procedure

@[simp]

theorem Experiment.NoParams.h.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.NoParams.h.apply_simp [GaudisCrypt.ProgramSpec] : h = GaudisCrypt.Module.proc procedure

@[simp]

theorem Experiment.NoParams.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

noncomputable def Experiment.NoParams.g.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.NoParams.g.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.NoParams [GaudisCrypt.ProgramSpec] : M2

Equations

• Experiment.NoParams = Experiment.M2.mk { g := Experiment.NoParams.g, h := Experiment.NoParams.h }

noncomputable def Experiment.NoParams.h.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.NoParams.h.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.NoParams.h [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.NoParams.h = GaudisCrypt.Module.proc Experiment.NoParams.h.procedure

@[simp]

theorem Experiment.EmptyParams.apply_simp [GaudisCrypt.ProgramSpec] (t : GaudisCrypt.Module.Unit) : GaudisCrypt.Module.app EmptyParams t = M2.mk { g := g, h := h }

noncomputable def Experiment.EmptyParams.h [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.EmptyParams.h = GaudisCrypt.Module.proc Experiment.EmptyParams.h.procedure

@[simp]

theorem Experiment.EmptyParams.h.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

noncomputable def Experiment.EmptyParams [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr GaudisCrypt.Module.Unit M2

Equations

• Experiment.EmptyParams = (Experiment.EmptyParams.g.expression.pair Experiment.EmptyParams.h.expression).abs.toModule ⋯

noncomputable def Experiment.EmptyParams.g.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.EmptyParams.g.procedure = proc () : Unit { skip; return () }

noncomputable def Experiment.EmptyParams.g [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.EmptyParams.g = GaudisCrypt.Module.proc Experiment.EmptyParams.g.procedure

@[simp]

theorem Experiment.EmptyParams.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.EmptyParams.h.apply_simp [GaudisCrypt.ProgramSpec] : h = GaudisCrypt.Module.proc procedure

noncomputable def Experiment.EmptyParams.h.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.EmptyParams.h.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.EmptyParams.g.apply_simp [GaudisCrypt.ProgramSpec] : g = GaudisCrypt.Module.proc procedure

@[simp]

theorem Experiment.NoType.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app NoType A = GaudisCrypt.Module.pair (GaudisCrypt.Module.app g A) h

noncomputable def Experiment.NoType.g.procedure [GaudisCrypt.ProgramSpec] : proctype () → Unit uses (() → Unit)

Equations

• Experiment.NoType.g.procedure = proc () uses (_hole0 : () → Unit) : Unit { call _hole0 (); return () }

@[simp]

theorem Experiment.NoType.g.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app g A = GaudisCrypt.Module.proc (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.nil) (GaudisCrypt.Module.app A myMod).procedure)

noncomputable def Experiment.NoType [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Prod (procmod () → Unit) (procmod () → Bool))

Equations

• Experiment.NoType = ((Experiment.NoType.g.expression.app (GaudisCrypt.ModuleExpression.var 0)).pair Experiment.NoType.h.expression).abs.toModule ⋯

noncomputable def Experiment.NoType.h [GaudisCrypt.ProgramSpec] : procmod () → Bool

Equations

• Experiment.NoType.h = GaudisCrypt.Module.proc Experiment.NoType.h.procedure

noncomputable def Experiment.NoType.h.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Bool

Equations

• Experiment.NoType.h.procedure = proc () : Bool { skip; return true }

noncomputable def Experiment.NoType.g [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (procmod () → Unit)

Equations

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

@[simp]

theorem Experiment.NoType.h.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Bool { skip; return true }

@[simp]

theorem Experiment.NoType.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : (GaudisCrypt.HoleSigs.empty.append (procsig () → Unit)).Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { call (args GaudisCrypt.HoleIndex.zero) (); return () }

@[simp]

theorem Experiment.NoType.h.apply_simp [GaudisCrypt.ProgramSpec] : h = GaudisCrypt.Module.proc procedure

noncomputable def Experiment.Deep.h.procedure [GaudisCrypt.ProgramSpec] : proctype () → Unit uses ((String, ℕ) → Bool)

Equations

• Experiment.Deep.h.procedure = proc () uses (_hole0 : (String, ℕ) → Bool) : Unit { call _hole0 ("hi", 3); return () }

noncomputable def Experiment.Deep.h [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)

Equations

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

noncomputable def Experiment.Deep [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Prod (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Prod TestModule (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)))) M2

Equations

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

@[simp]

theorem Experiment.Deep.g.apply_simp [GaudisCrypt.ProgramSpec] (A C : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) C = GaudisCrypt.Module.proc (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.nil) (GaudisCrypt.Module.app C myMod).procedure) (GaudisCrypt.Module.app A myMod).procedure)

@[simp]

theorem Experiment.Deep.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : ((GaudisCrypt.HoleSigs.empty.append (procsig () → Unit)).append (procsig () → Unit)).Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { call (args GaudisCrypt.HoleIndex.zero.succ) (); call (args GaudisCrypt.HoleIndex.zero) (); return () }

@[simp]

theorem Experiment.Deep.h.apply_simp [GaudisCrypt.ProgramSpec] (B : TestModule) : GaudisCrypt.Module.app h B = GaudisCrypt.Module.proc (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.push (fun {sig : GaudisCrypt.ProcedureSignature} => GaudisCrypt.HoleSigs.Instantiation.nil) (GaudisCrypt.Module.procedure B.main))

noncomputable def Experiment.Deep.g.procedure [GaudisCrypt.ProgramSpec] : proctype () → Unit uses (() → Unit, () → Unit)

Equations

• Experiment.Deep.g.procedure = proc () uses (_hole0 : () → Unit, _hole1 : () → Unit) : Unit { call _hole0 (); call _hole1 (); return () }

noncomputable def Experiment.Deep.g [GaudisCrypt.ProgramSpec] : GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (GaudisCrypt.Module.Arr (GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (procmod () → Unit))

Equations

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

@[simp]

theorem Experiment.Deep.h.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : (GaudisCrypt.HoleSigs.empty.append (procsig (String, ℕ) → Bool)).Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { call (args GaudisCrypt.HoleIndex.zero) ("hi", 3); return () }

@[simp]

theorem Experiment.Deep.apply_simp [GaudisCrypt.ProgramSpec] (A : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) (B : TestModule) (C : GaudisCrypt.Module.Arr TestModule (procmod () → Unit)) : GaudisCrypt.Module.app Deep (GaudisCrypt.Module.pair A (GaudisCrypt.Module.pair B C)) = M2.mk { g := GaudisCrypt.Module.app (GaudisCrypt.Module.app g A) C, h := GaudisCrypt.Module.app h B }

noncomputable def Experiment.NoTypeNoParams.g.procedure [GaudisCrypt.ProgramSpec] : proctype () -> Unit

Equations

• Experiment.NoTypeNoParams.g.procedure = proc () : Unit { skip; return () }

@[simp]

theorem Experiment.NoTypeNoParams.g.procedure.apply_simp [GaudisCrypt.ProgramSpec] (args : GaudisCrypt.HoleSigs.empty.Instantiation) : (procedure.instantiate fun {sig : GaudisCrypt.ProcedureSignature} => args) = proc () : Unit { skip; return () }

noncomputable def Experiment.NoTypeNoParams.g [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.NoTypeNoParams.g = GaudisCrypt.Module.proc Experiment.NoTypeNoParams.g.procedure

@[simp]

theorem Experiment.NoTypeNoParams.g.apply_simp [GaudisCrypt.ProgramSpec] : g = GaudisCrypt.Module.proc procedure

noncomputable def Experiment.NoTypeNoParams [GaudisCrypt.ProgramSpec] : procmod () → Unit

Equations

• Experiment.NoTypeNoParams = Experiment.NoTypeNoParams.g