wip

formal-land · Jan 26, 2025 · d1ae316 · d1ae316
1 parent 57c7320
commit d1ae316
Show file tree

Hide file tree

Showing 77 changed files with 3,746 additions and 2,614 deletions.
diff --git a/Garden/Circom/Circomlib/proof/circuits/sha256/xor3.v b/Garden/Circom/Circomlib/proof/circuits/sha256/xor3.v
@@ -0,0 +1,62 @@
+Require Import Garden.Garden.
+Require Import Circom.Circomlib.translation.circuits.sha256.xor3.
+
+Import Run.
+
+Lemma run_Xor3 (P : Z) (a b c out mid : list F.t)
+    (H_length_a : List.length a = 3%nat)
+    (H_length_b : List.length b = 3%nat)
+    (H_length_c : List.length c = 3%nat)
+    (H_bits_a : List.Forall (fun x => x = 0 \/ x = 1) a)
+    (H_bits_b : List.Forall (fun x => x = 0 \/ x = 1) b)
+    (H_bits_c : List.Forall (fun x => x = 0 \/ x = 1) c) :
+  let signals := {|
+    Xor3Signals.a := a;
+    Xor3Signals.b := b;
+    Xor3Signals.c := c;
+    Xor3Signals.out := out;
+    Xor3Signals.mid := mid;
+  |} in
+  {{ Xor3Signals.IsNamed.P, 97 , signals, Scopes.empty ⏩
+    Xor3 3 🔽 BlockUnit.Tt
+  ⏩ Scopes.empty, True, True }}.
+Proof.
+  do 4 (destruct a as [|? a]; cbn in H_length_a; try discriminate).
+  do 4 (destruct b as [|? b]; cbn in H_length_b; try discriminate).
+  do 4 (destruct c as [|? c]; cbn in H_length_c; try discriminate).
+  repeat match goal with
+  | H : List.Forall _ _ |- _ => inversion_clear H
+  end.
+  repeat match goal with
+  | H : _ \/ _ |- _ => destruct H
+  end;
+    subst.
+  { run_deterministic.
+    { eapply Run.PrimitiveGetVarAccessSignal;
+      (* reflexivity.
+      now constructor.
+      cbn.
+      repeat econstructor. *)
+       [
+        reflexivity | now constructor | now repeat econstructor |
+      ].
+      eapply Run.PrimitiveDeclareSignal.
+      cbn.
+    { eapply Run.PrimitiveGetVarAccess.
+      repeat constructor.
+      2: {
+        repeat constructor.
+      }
+      reflexivity.
+    Show.
+
+  }
+  {
+    cbn in H_length_a.
+    discriminate.
+  }
+  2: {
+
+  }
+  run_deterministic.
+Qed.
diff --git a/Garden/Circom/Circomlib/translation/circuits/aliascheck.v b/Garden/Circom/Circomlib/translation/circuits/aliascheck.v
@@ -7,22 +7,27 @@ Module AliasCheckSignals.
     (* Input *)
     in_ : list F.t;
   }.
+
+  Module IsNamed.
+    Inductive P : forall (A : Set), (t -> A) -> string -> Prop :=
+    | in_ : P _ in_ "in".
+  End IsNamed.
 End AliasCheckSignals.
 
 (* Template body *)
 Definition AliasCheck : M.t (BlockUnit.t Empty_set) :=
   M.template_body [] (
     (* Signal Input *)
-    do~ M.declare_signal "in" [[ [ 254 ] ]] in
+    do~ M.declare_signal "in" in
     (* Component *)
     do~ M.declare_component "compConstant" in
-    do~ M.substitute_var "compConstant" [[ M.call_function ~(| "CompConstant", [ PrefixOp.sub ~(| 1 |) ] |) ]] in
+    do~ M.substitute_var "compConstant" [] [[ M.call_function ~(| "CompConstant", [ PrefixOp.sub ~(| 1 |) ] |) ]] in
     (* Var *)
     do~ M.declare_var "i" [[ ([] : list F.t) ]] in
-    do~ M.substitute_var "i" [[ 0 ]] in
+    do~ M.substitute_var "i" [] [[ 0 ]] in
     do~ M.while [[ InfixOp.lesser ~(| M.var (| "i" |), 254 |) ]] (
-      do~ M.substitute_var "compConstant" [[ M.var_access (| "in", [Access.Array (M.var (| "i" |))] |) ]] in
-      do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var (| "i" |), 1 |) ]] in
+      do~ M.substitute_var "compConstant" [Access.Component "in"; Access.Array (M.var (| "i" |))] [[ M.var_access (| "in", [Access.Array (M.var (| "i" |))] |) ]] in
+      do~ M.substitute_var "i" [] [[ InfixOp.add ~(| M.var (| "i" |), 1 |) ]] in
       M.pure BlockUnit.Tt
     ) in
     do~ M.equality_constraint

diff --git a/Garden/Circom/Circomlib/translation/circuits/babyjub.v b/Garden/Circom/Circomlib/translation/circuits/babyjub.v
@@ -25,47 +25,61 @@ Module BabyAddSignals.
     (* Intermediate *)
     tau : F.t;
   }.
+
+  Module IsNamed.
+    Inductive P : forall (A : Set), (t -> A) -> string -> Prop :=
+    | x1 : P _ x1 "x1"
+    | y1 : P _ y1 "y1"
+    | x2 : P _ x2 "x2"
+    | y2 : P _ y2 "y2"
+    | xout : P _ xout "xout"
+    | yout : P _ yout "yout"
+    | beta : P _ beta "beta"
+    | gamma : P _ gamma "gamma"
+    | delta : P _ delta "delta"
+    | tau : P _ tau "tau".
+  End IsNamed.
 End BabyAddSignals.
 
 (* Template body *)
 Definition BabyAdd : M.t (BlockUnit.t Empty_set) :=
   M.template_body [] (
     (* Signal Input *)
-    do~ M.declare_signal "x1" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "x1" in
     (* Signal Input *)
-    do~ M.declare_signal "y1" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "y1" in
     (* Signal Input *)
-    do~ M.declare_signal "x2" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "x2" in
     (* Signal Input *)
-    do~ M.declare_signal "y2" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "y2" in
     (* Signal Output *)
-    do~ M.declare_signal "xout" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "xout" in
     (* Signal Output *)
-    do~ M.declare_signal "yout" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "yout" in
     (* Signal Intermediate *)
-    do~ M.declare_signal "beta" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "beta" in
     (* Signal Intermediate *)
-    do~ M.declare_signal "gamma" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "gamma" in
     (* Signal Intermediate *)
-    do~ M.declare_signal "delta" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "delta" in
     (* Signal Intermediate *)
-    do~ M.declare_signal "tau" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "tau" in
     (* Var *)
     do~ M.declare_var "a" [[ ([] : list F.t) ]] in
-    do~ M.substitute_var "a" [[ 168700 ]] in
+    do~ M.substitute_var "a" [] [[ 168700 ]] in
     (* Var *)
     do~ M.declare_var "d" [[ ([] : list F.t) ]] in
-    do~ M.substitute_var "d" [[ 168696 ]] in
-    do~ M.substitute_var "beta" [[ InfixOp.mul ~(| M.var (| "x1" |), M.var (| "y2" |) |) ]] in
-    do~ M.substitute_var "gamma" [[ InfixOp.mul ~(| M.var (| "y1" |), M.var (| "x2" |) |) ]] in
-    do~ M.substitute_var "delta" [[ InfixOp.mul ~(| InfixOp.add ~(| InfixOp.mul ~(| PrefixOp.sub ~(| M.var (| "a" |) |), M.var (| "x1" |) |), M.var (| "y1" |) |), InfixOp.add ~(| M.var (| "x2" |), M.var (| "y2" |) |) |) ]] in
-    do~ M.substitute_var "tau" [[ InfixOp.mul ~(| M.var (| "beta" |), M.var (| "gamma" |) |) ]] in
-    do~ M.substitute_var "xout" [[ InfixOp.div ~(| InfixOp.add ~(| M.var (| "beta" |), M.var (| "gamma" |) |), InfixOp.add ~(| 1, InfixOp.mul ~(| M.var (| "d" |), M.var (| "tau" |) |) |) |) ]] in
+    do~ M.substitute_var "d" [] [[ 168696 ]] in
+    do~ M.substitute_var "beta" [] [[ InfixOp.mul ~(| M.var (| "x1" |), M.var (| "y2" |) |) ]] in
+    do~ M.substitute_var "gamma" [] [[ InfixOp.mul ~(| M.var (| "y1" |), M.var (| "x2" |) |) ]] in
+    do~ M.substitute_var "delta" [] [[ InfixOp.mul ~(| InfixOp.add ~(| InfixOp.mul ~(| PrefixOp.sub ~(| M.var (| "a" |) |), M.var (| "x1" |) |), M.var (| "y1" |) |), InfixOp.add ~(| M.var (| "x2" |), M.var (| "y2" |) |) |) ]] in
+    do~ M.substitute_var "tau" [] [[ InfixOp.mul ~(| M.var (| "beta" |), M.var (| "gamma" |) |) ]] in
+    do~ M.substitute_var "xout" [] [[ InfixOp.div ~(| InfixOp.add ~(| M.var (| "beta" |), M.var (| "gamma" |) |), InfixOp.add ~(| 1, InfixOp.mul ~(| M.var (| "d" |), M.var (| "tau" |) |) |) |) ]] in
     do~ M.equality_constraint
       [[ InfixOp.mul ~(| InfixOp.add ~(| 1, InfixOp.mul ~(| M.var (| "d" |), M.var (| "tau" |) |) |), M.var (| "xout" |) |) ]]
       [[ InfixOp.add ~(| M.var (| "beta" |), M.var (| "gamma" |) |) ]]
     in
-    do~ M.substitute_var "yout" [[ InfixOp.div ~(| InfixOp.sub ~(| InfixOp.add ~(| M.var (| "delta" |), InfixOp.mul ~(| M.var (| "a" |), M.var (| "beta" |) |) |), M.var (| "gamma" |) |), InfixOp.sub ~(| 1, InfixOp.mul ~(| M.var (| "d" |), M.var (| "tau" |) |) |) |) ]] in
+    do~ M.substitute_var "yout" [] [[ InfixOp.div ~(| InfixOp.sub ~(| InfixOp.add ~(| M.var (| "delta" |), InfixOp.mul ~(| M.var (| "a" |), M.var (| "beta" |) |) |), M.var (| "gamma" |) |), InfixOp.sub ~(| 1, InfixOp.mul ~(| M.var (| "d" |), M.var (| "tau" |) |) |) |) ]] in
     do~ M.equality_constraint
       [[ InfixOp.mul ~(| InfixOp.sub ~(| 1, InfixOp.mul ~(| M.var (| "d" |), M.var (| "tau" |) |) |), M.var (| "yout" |) |) ]]
       [[ InfixOp.sub ~(| InfixOp.add ~(| M.var (| "delta" |), InfixOp.mul ~(| M.var (| "a" |), M.var (| "beta" |) |) |), M.var (| "gamma" |) |) ]]
@@ -92,28 +106,36 @@ Module BabyDblSignals.
     (* Output *)
     yout : F.t;
   }.
+
+  Module IsNamed.
+    Inductive P : forall (A : Set), (t -> A) -> string -> Prop :=
+    | x : P _ x "x"
+    | y : P _ y "y"
+    | xout : P _ xout "xout"
+    | yout : P _ yout "yout".
+  End IsNamed.
 End BabyDblSignals.
 
 (* Template body *)
 Definition BabyDbl : M.t (BlockUnit.t Empty_set) :=
   M.template_body [] (
     (* Signal Input *)
-    do~ M.declare_signal "x" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "x" in
     (* Signal Input *)
-    do~ M.declare_signal "y" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "y" in
     (* Signal Output *)
-    do~ M.declare_signal "xout" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "xout" in
     (* Signal Output *)
-    do~ M.declare_signal "yout" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "yout" in
     (* Component *)
     do~ M.declare_component "adder" in
-    do~ M.substitute_var "adder" [[ M.call_function ~(| "BabyAdd", ([] : list F.t) |) ]] in
-    do~ M.substitute_var "adder" [[ M.var (| "x" |) ]] in
-    do~ M.substitute_var "adder" [[ M.var (| "y" |) ]] in
-    do~ M.substitute_var "adder" [[ M.var (| "x" |) ]] in
-    do~ M.substitute_var "adder" [[ M.var (| "y" |) ]] in
-    do~ M.substitute_var "xout" [[ M.var_access (| "adder", [Access.Component "xout"] |) ]] in
-    do~ M.substitute_var "yout" [[ M.var_access (| "adder", [Access.Component "yout"] |) ]] in
+    do~ M.substitute_var "adder" [] [[ M.call_function ~(| "BabyAdd", ([] : list F.t) |) ]] in
+    do~ M.substitute_var "adder" [Access.Component "x1"] [[ M.var (| "x" |) ]] in
+    do~ M.substitute_var "adder" [Access.Component "y1"] [[ M.var (| "y" |) ]] in
+    do~ M.substitute_var "adder" [Access.Component "x2"] [[ M.var (| "x" |) ]] in
+    do~ M.substitute_var "adder" [Access.Component "y2"] [[ M.var (| "y" |) ]] in
+    do~ M.substitute_var "xout" [] [[ M.var_access (| "adder", [Access.Component "xout"] |) ]] in
+    do~ M.substitute_var "yout" [] [[ M.var_access (| "adder", [Access.Component "yout"] |) ]] in
     M.pure BlockUnit.Tt
   ).
 
@@ -135,27 +157,35 @@ Module BabyCheckSignals.
     (* Intermediate *)
     y2 : F.t;
   }.
+
+  Module IsNamed.
+    Inductive P : forall (A : Set), (t -> A) -> string -> Prop :=
+    | x : P _ x "x"
+    | y : P _ y "y"
+    | x2 : P _ x2 "x2"
+    | y2 : P _ y2 "y2".
+  End IsNamed.
 End BabyCheckSignals.
 
 (* Template body *)
 Definition BabyCheck : M.t (BlockUnit.t Empty_set) :=
   M.template_body [] (
     (* Signal Input *)
-    do~ M.declare_signal "x" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "x" in
     (* Signal Input *)
-    do~ M.declare_signal "y" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "y" in
     (* Signal Intermediate *)
-    do~ M.declare_signal "x2" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "x2" in
     (* Signal Intermediate *)
-    do~ M.declare_signal "y2" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "y2" in
     (* Var *)
     do~ M.declare_var "a" [[ ([] : list F.t) ]] in
-    do~ M.substitute_var "a" [[ 168700 ]] in
+    do~ M.substitute_var "a" [] [[ 168700 ]] in
     (* Var *)
     do~ M.declare_var "d" [[ ([] : list F.t) ]] in
-    do~ M.substitute_var "d" [[ 168696 ]] in
-    do~ M.substitute_var "x2" [[ InfixOp.mul ~(| M.var (| "x" |), M.var (| "x" |) |) ]] in
-    do~ M.substitute_var "y2" [[ InfixOp.mul ~(| M.var (| "y" |), M.var (| "y" |) |) ]] in
+    do~ M.substitute_var "d" [] [[ 168696 ]] in
+    do~ M.substitute_var "x2" [] [[ InfixOp.mul ~(| M.var (| "x" |), M.var (| "x" |) |) ]] in
+    do~ M.substitute_var "y2" [] [[ InfixOp.mul ~(| M.var (| "y" |), M.var (| "y" |) |) ]] in
     do~ M.equality_constraint
       [[ InfixOp.add ~(| InfixOp.mul ~(| M.var (| "a" |), M.var (| "x2" |) |), M.var (| "y2" |) |) ]]
       [[ InfixOp.add ~(| 1, InfixOp.mul ~(| InfixOp.mul ~(| M.var (| "d" |), M.var (| "x2" |) |), M.var (| "y2" |) |) |) ]]
@@ -179,39 +209,46 @@ Module BabyPbkSignals.
     (* Output *)
     Ay : F.t;
   }.
+
+  Module IsNamed.
+    Inductive P : forall (A : Set), (t -> A) -> string -> Prop :=
+    | in_ : P _ in_ "in"
+    | Ax : P _ Ax "Ax"
+    | Ay : P _ Ay "Ay".
+  End IsNamed.
 End BabyPbkSignals.
 
 (* Template body *)
 Definition BabyPbk : M.t (BlockUnit.t Empty_set) :=
   M.template_body [] (
     (* Signal Input *)
-    do~ M.declare_signal "in" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "in" in
     (* Signal Output *)
-    do~ M.declare_signal "Ax" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "Ax" in
     (* Signal Output *)
-    do~ M.declare_signal "Ay" [[ ([] : list F.t) ]] in
+    do~ M.declare_signal "Ay" in
     (* Var *)
     do~ M.declare_var "BASE8" [[ [ 2 ] ]] in
-    do~ M.substitute_var "BASE8" [[ array_with_repeat (0) (2) ]] in
-    do~ M.substitute_var "BASE8" [[ [ 5299619240641551281634865583518297030282874472190772894086521144482721001553; 16950150798460657717958625567821834550301663161624707787222815936182638968203 ] ]] in
+    do~ M.substitute_var "BASE8" [] [[ array_with_repeat (0) (2) ]] in
+    do~ M.substitute_var "BASE8" [] [[ [ 5299619240641551281634865583518297030282874472190772894086521144482721001553; 16950150798460657717958625567821834550301663161624707787222815936182638968203 ] ]] in
     (* Component *)
     do~ M.declare_component "pvkBits" in
-    do~ M.substitute_var "pvkBits" [[ M.call_function ~(| "Num2Bits", [ 253 ] |) ]] in
-    do~ M.substitute_var "pvkBits" [[ M.var (| "in" |) ]] in
+    do~ M.substitute_var "pvkBits" [] [[ M.call_function ~(| "Num2Bits", [ 253 ] |) ]] in
+    do~ M.substitute_var "pvkBits" [Access.Component "in"] [[ M.var (| "in" |) ]] in
     (* Component *)
     do~ M.declare_component "mulFix" in
-    do~ M.substitute_var "mulFix" [[ M.call_function ~(| "EscalarMulFix", [ 253; M.var (| "BASE8" |) ] |) ]] in
+    do~ M.substitute_var "mulFix" [] [[ M.call_function ~(| "EscalarMulFix", [ 253; M.var (| "BASE8" |) ] |) ]] in
     (* Var *)
     do~ M.declare_var "i" [[ ([] : list F.t) ]] in
-    do~ M.substitute_var "i" [[ 0 ]] in
-    do~ M.substitute_var "i" [[ 0 ]] in
+    do~ M.substitute_var "i" [] [[ 0 ]] in
+    do~ M.substitute_var "i" [] [[ 0 ]] in
     do~ M.while [[ InfixOp.lesser ~(| M.var (| "i" |), 253 |) ]] (
-      do~ M.substitute_var "mulFix" [[ M.var_access (| "pvkBits", [Access.Component "out"; Access.Array (M.var (| "i" |))] |) ]] in
-      do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var (| "i" |), 1 |) ]] in
+      do~ M.substitute_var "mulFix" [Access.Component "e"; Access.Array (M.var (| "i" |))] [[ M.var_access (| "pvkBits", [Access.Component "out"; Access.Array (M.var (| "i" |))] |) ]] in
+      do~ M.substitute_var "i" [] [[ InfixOp.add ~(| M.var (| "i" |), 1 |) ]] in
       M.pure BlockUnit.Tt
     ) in
-    do~ M.substitute_var "Ax" [[ M.var_access (| "mulFix", [Access.Component "out"; Access.Array (0)] |) ]] in
-    do~ M.substitute_var "Ay" [[ M.var_access (| "mulFix", [Access.Component "out"; Access.Array (1)] |) ]] in
+    do~ M.substitute_var "Ax" [] [[ M.var_access (| "mulFix", [Access.Component "out"; Access.Array (0)] |) ]] in
+    do~ M.substitute_var "Ay" [] [[ M.var_access (| "mulFix", [Access.Component "out"; Access.Array (1)] |) ]] in
     M.pure BlockUnit.Tt
   ).