circom: translate all the circomlib examples

formal-land · Jan 16, 2025 · 5f240a3 · 5f240a3
1 parent 1fc0c06
commit 5f240a3
Show file tree

Hide file tree

Showing 102 changed files with 3,001 additions and 16 deletions.
diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
@@ -38,19 +38,12 @@ jobs:
             cd ../..
           endGroup
           startGroup "Translate Circom library"
-            cd third-party/circomlib/test/circuits
-            # For each Circom circuit
-            for circuit in *.circom; do
-              # Translate the circuit to JSON
-              circom $circuit
-            done
-            cd ../../../..
-            # For each JSON circuit
-            for circuit in third-party/circomlib/circuits/*.json; do
-              # Translate the JSON circuit to Coq
-              echo "Translating $circuit"
-              python scripts/coq_of_circom.py $circuit > Garden/Circom/Example/$(basename $circuit .json).v
-            done
+            cd third-party/circomlib
+            # Translate each Circom circuit to JSON
+            find . -name '*.circom' -execdir circom {} \;
+            cd ../..
+            # Translate the JSON to Coq
+            python scripts/coq_of_circom_ci.py
           endGroup
           startGroup "Check that the diff is empty (excluding submodules)"
             git -c color.ui=always diff --exit-code --ignore-submodules=dirty

diff --git a/Garden/Circom/Example/aliascheck.v → ...en/Circom/Circomlib/circuits/aliascheck.v b/Garden/Circom/Example/aliascheck.v → ...en/Circom/Circomlib/circuits/aliascheck.v
diff --git a/Garden/Circom/Example/babyjub.v → Garden/Circom/Circomlib/circuits/babyjub.v b/Garden/Circom/Example/babyjub.v → Garden/Circom/Circomlib/circuits/babyjub.v
diff --git a/Garden/Circom/Example/binsub.v → Garden/Circom/Circomlib/circuits/binsub.v b/Garden/Circom/Example/binsub.v → Garden/Circom/Circomlib/circuits/binsub.v
diff --git a/Garden/Circom/Example/binsum.v → Garden/Circom/Circomlib/circuits/binsum.v b/Garden/Circom/Example/binsum.v → Garden/Circom/Circomlib/circuits/binsum.v
diff --git a/Garden/Circom/Example/bitify.v → Garden/Circom/Circomlib/circuits/bitify.v b/Garden/Circom/Example/bitify.v → Garden/Circom/Circomlib/circuits/bitify.v
diff --git a/Garden/Circom/Example/comparators.v → ...n/Circom/Circomlib/circuits/comparators.v b/Garden/Circom/Example/comparators.v → ...n/Circom/Circomlib/circuits/comparators.v
diff --git a/Garden/Circom/Example/compconstant.v → .../Circom/Circomlib/circuits/compconstant.v b/Garden/Circom/Example/compconstant.v → .../Circom/Circomlib/circuits/compconstant.v
diff --git a/Garden/Circom/Example/eddsa.v → Garden/Circom/Circomlib/circuits/eddsa.v b/Garden/Circom/Example/eddsa.v → Garden/Circom/Circomlib/circuits/eddsa.v
diff --git a/Garden/Circom/Example/eddsamimc.v → Garden/Circom/Circomlib/circuits/eddsamimc.v b/Garden/Circom/Example/eddsamimc.v → Garden/Circom/Circomlib/circuits/eddsamimc.v
diff --git a/Garden/Circom/Example/eddsaposeidon.v → ...Circom/Circomlib/circuits/eddsaposeidon.v b/Garden/Circom/Example/eddsaposeidon.v → ...Circom/Circomlib/circuits/eddsaposeidon.v
diff --git a/Garden/Circom/Example/escalarmul.v → ...en/Circom/Circomlib/circuits/escalarmul.v b/Garden/Circom/Example/escalarmul.v → ...en/Circom/Circomlib/circuits/escalarmul.v
diff --git a/Garden/Circom/Example/escalarmulany.v → ...Circom/Circomlib/circuits/escalarmulany.v b/Garden/Circom/Example/escalarmulany.v → ...Circom/Circomlib/circuits/escalarmulany.v
diff --git a/Garden/Circom/Example/escalarmulfix.v → ...Circom/Circomlib/circuits/escalarmulfix.v b/Garden/Circom/Example/escalarmulfix.v → ...Circom/Circomlib/circuits/escalarmulfix.v
diff --git a/Garden/Circom/Example/escalarmulw4table.v → ...om/Circomlib/circuits/escalarmulw4table.v b/Garden/Circom/Example/escalarmulw4table.v → ...om/Circomlib/circuits/escalarmulw4table.v
diff --git a/Garden/Circom/Example/gates.v → Garden/Circom/Circomlib/circuits/gates.v b/Garden/Circom/Example/gates.v → Garden/Circom/Circomlib/circuits/gates.v
diff --git a/Garden/Circom/Example/mimc.v → Garden/Circom/Circomlib/circuits/mimc.v b/Garden/Circom/Example/mimc.v → Garden/Circom/Circomlib/circuits/mimc.v
diff --git a/Garden/Circom/Example/mimcsponge.v → ...en/Circom/Circomlib/circuits/mimcsponge.v b/Garden/Circom/Example/mimcsponge.v → ...en/Circom/Circomlib/circuits/mimcsponge.v
diff --git a/Garden/Circom/Example/montgomery.v → ...en/Circom/Circomlib/circuits/montgomery.v b/Garden/Circom/Example/montgomery.v → ...en/Circom/Circomlib/circuits/montgomery.v
diff --git a/Garden/Circom/Example/mux1.v → Garden/Circom/Circomlib/circuits/mux1.v b/Garden/Circom/Example/mux1.v → Garden/Circom/Circomlib/circuits/mux1.v
diff --git a/Garden/Circom/Example/mux2.v → Garden/Circom/Circomlib/circuits/mux2.v b/Garden/Circom/Example/mux2.v → Garden/Circom/Circomlib/circuits/mux2.v
diff --git a/Garden/Circom/Example/mux3.v → Garden/Circom/Circomlib/circuits/mux3.v b/Garden/Circom/Example/mux3.v → Garden/Circom/Circomlib/circuits/mux3.v
diff --git a/Garden/Circom/Example/mux4.v → Garden/Circom/Circomlib/circuits/mux4.v b/Garden/Circom/Example/mux4.v → Garden/Circom/Circomlib/circuits/mux4.v
diff --git a/Garden/Circom/Example/pedersen.v → Garden/Circom/Circomlib/circuits/pedersen.v b/Garden/Circom/Example/pedersen.v → Garden/Circom/Circomlib/circuits/pedersen.v
diff --git a/Garden/Circom/Example/pedersen_old.v → .../Circom/Circomlib/circuits/pedersen_old.v b/Garden/Circom/Example/pedersen_old.v → .../Circom/Circomlib/circuits/pedersen_old.v
diff --git a/Garden/Circom/Example/pointbits.v → Garden/Circom/Circomlib/circuits/pointbits.v b/Garden/Circom/Example/pointbits.v → Garden/Circom/Circomlib/circuits/pointbits.v
diff --git a/Garden/Circom/Example/poseidon.v → Garden/Circom/Circomlib/circuits/poseidon.v b/Garden/Circom/Example/poseidon.v → Garden/Circom/Circomlib/circuits/poseidon.v
diff --git a/Garden/Circom/Example/poseidon_constants.v → ...m/Circomlib/circuits/poseidon_constants.v b/Garden/Circom/Example/poseidon_constants.v → ...m/Circomlib/circuits/poseidon_constants.v
diff --git a/Garden/Circom/Circomlib/circuits/sha256/ch.v b/Garden/Circom/Circomlib/circuits/sha256/ch.v
@@ -0,0 +1,33 @@
+
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module Ch_tSignals.
+  Record t : Set := {
+    a : list F.t;
+    b : list F.t;
+    c : list F.t;
+    out : list F.t;
+  }.
+End Ch_tSignals.
+
+(* Template body *)
+Definition Ch_t (n : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "a" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "b" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "c" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Var *)
+  do~ M.declare_var "k" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), M.var ~(| "n" |) |) ]] (
+    do~ M.substitute_var "out" [[ InfixOp.add ~(| InfixOp.mul ~(| M.var_access ~(| "a", [Access.Array (M.var ~(| "k" |))] |), InfixOp.sub ~(| M.var_access ~(| "b", [Access.Array (M.var ~(| "k" |))] |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |) |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.
diff --git a/Garden/Circom/Circomlib/circuits/sha256/constants.v b/Garden/Circom/Circomlib/circuits/sha256/constants.v
@@ -0,0 +1,53 @@
+
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module HSignals.
+  Record t : Set := {
+    out : list F.t;
+  }.
+End HSignals.
+
+(* Template body *)
+Definition H (x : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ 32 ] ]] in
+  (* Var *)
+  do~ M.declare_var "c" [[ [ 8 ] ]] in
+  do~ M.substitute_var "c" [[ array_with_repeat (0) (8) ]] in
+  do~ M.substitute_var "c" [[ [ 1779033703; 3144134277; 1013904242; 2773480762; 1359893119; 2600822924; 528734635; 1541459225 ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), 32 |) ]] (
+    do~ M.substitute_var "out" [[ InfixOp.bitAnd ~(| InfixOp.shiftR ~(| M.var_access ~(| "c", [Access.Array (M.var ~(| "x" |))] |), M.var ~(| "i" |) |), 1 |) ]] in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.
+
+(* Template signals *)
+Module KSignals.
+  Record t : Set := {
+    out : list F.t;
+  }.
+End KSignals.
+
+(* Template body *)
+Definition K (x : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ 32 ] ]] in
+  (* Var *)
+  do~ M.declare_var "c" [[ [ 64 ] ]] in
+  do~ M.substitute_var "c" [[ array_with_repeat (0) (64) ]] in
+  do~ M.substitute_var "c" [[ [ 1116352408; 1899447441; 3049323471; 3921009573; 961987163; 1508970993; 2453635748; 2870763221; 3624381080; 310598401; 607225278; 1426881987; 1925078388; 2162078206; 2614888103; 3248222580; 3835390401; 4022224774; 264347078; 604807628; 770255983; 1249150122; 1555081692; 1996064986; 2554220882; 2821834349; 2952996808; 3210313671; 3336571891; 3584528711; 113926993; 338241895; 666307205; 773529912; 1294757372; 1396182291; 1695183700; 1986661051; 2177026350; 2456956037; 2730485921; 2820302411; 3259730800; 3345764771; 3516065817; 3600352804; 4094571909; 275423344; 430227734; 506948616; 659060556; 883997877; 958139571; 1322822218; 1537002063; 1747873779; 1955562222; 2024104815; 2227730452; 2361852424; 2428436474; 2756734187; 3204031479; 3329325298 ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), 32 |) ]] (
+    do~ M.substitute_var "out" [[ InfixOp.bitAnd ~(| InfixOp.shiftR ~(| M.var_access ~(| "c", [Access.Array (M.var ~(| "x" |))] |), M.var ~(| "i" |) |), 1 |) ]] in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.
diff --git a/Garden/Circom/Circomlib/circuits/sha256/maj.v b/Garden/Circom/Circomlib/circuits/sha256/maj.v
@@ -0,0 +1,37 @@
+
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module Maj_tSignals.
+  Record t : Set := {
+    a : list F.t;
+    b : list F.t;
+    c : list F.t;
+    out : list F.t;
+    mid : list F.t;
+  }.
+End Maj_tSignals.
+
+(* Template body *)
+Definition Maj_t (n : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "a" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "b" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "c" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Intermediate *)
+  do~ M.declare_signal "mid" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Var *)
+  do~ M.declare_var "k" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), M.var ~(| "n" |) |) ]] (
+    do~ M.substitute_var "mid" [[ InfixOp.mul ~(| M.var_access ~(| "b", [Access.Array (M.var ~(| "k" |))] |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |) ]] in
+    do~ M.substitute_var "out" [[ InfixOp.add ~(| InfixOp.mul ~(| M.var_access ~(| "a", [Access.Array (M.var ~(| "k" |))] |), InfixOp.sub ~(| InfixOp.add ~(| M.var_access ~(| "b", [Access.Array (M.var ~(| "k" |))] |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |), InfixOp.mul ~(| 2, M.var_access ~(| "mid", [Access.Array (M.var ~(| "k" |))] |) |) |) |), M.var_access ~(| "mid", [Access.Array (M.var ~(| "k" |))] |) |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.
diff --git a/Garden/Circom/Circomlib/circuits/sha256/rotate.v b/Garden/Circom/Circomlib/circuits/sha256/rotate.v
@@ -0,0 +1,27 @@
+
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module RotRSignals.
+  Record t : Set := {
+    in_ : list F.t;
+    out : list F.t;
+  }.
+End RotRSignals.
+
+(* Template body *)
+Definition RotR (n r : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "in" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), M.var ~(| "n" |) |) ]] (
+    do~ M.substitute_var "out" [[ M.var_access ~(| "in", [Access.Array (InfixOp.mod_ ~(| InfixOp.add ~(| M.var ~(| "i" |), M.var ~(| "r" |) |), M.var ~(| "n" |) |))] |) ]] in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.
diff --git a/Garden/Circom/Circomlib/circuits/sha256/sha256.v b/Garden/Circom/Circomlib/circuits/sha256/sha256.v
@@ -0,0 +1,129 @@
+
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module Sha256Signals.
+  Record t : Set := {
+    in_ : list F.t;
+    out : list F.t;
+    paddedIn : list F.t;
+  }.
+End Sha256Signals.
+
+(* Template body *)
+Definition Sha256 (nBits : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "in" [[ [ M.var ~(| "nBits" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ 256 ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "k" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "nBlocks" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "nBlocks" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "bitsLastBlock" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "bitsLastBlock" [[ 0 ]] in
+  do~ M.substitute_var "nBlocks" [[ InfixOp.add ~(| InfixOp.intDiv ~(| InfixOp.add ~(| M.var ~(| "nBits" |), 64 |), 512 |), 1 |) ]] in
+  (* Signal Intermediate *)
+  do~ M.declare_signal "paddedIn" [[ [ InfixOp.mul ~(| M.var ~(| "nBlocks" |), 512 |) ] ]] in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), M.var ~(| "nBits" |) |) ]] (
+    do~ M.substitute_var "paddedIn" [[ M.var_access ~(| "in", [Access.Array (M.var ~(| "k" |))] |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  do~ M.substitute_var "paddedIn" [[ 1 ]] in
+  do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "nBits" |), 1 |) ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), InfixOp.sub ~(| InfixOp.mul ~(| M.var ~(| "nBlocks" |), 512 |), 64 |) |) ]] (
+    do~ M.substitute_var "paddedIn" [[ 0 ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), 64 |) ]] (
+    do~ M.substitute_var "paddedIn" [[ InfixOp.bitAnd ~(| InfixOp.shiftR ~(| M.var ~(| "nBits" |), M.var ~(| "k" |) |), 1 |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  (* Component *)
+  do~ M.declare_component "ha0" in
+  do~ M.substitute_var "ha0" [[ M.call_function ~(| "H", [ 0 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "hb0" in
+  do~ M.substitute_var "hb0" [[ M.call_function ~(| "H", [ 1 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "hc0" in
+  do~ M.substitute_var "hc0" [[ M.call_function ~(| "H", [ 2 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "hd0" in
+  do~ M.substitute_var "hd0" [[ M.call_function ~(| "H", [ 3 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "he0" in
+  do~ M.substitute_var "he0" [[ M.call_function ~(| "H", [ 4 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "hf0" in
+  do~ M.substitute_var "hf0" [[ M.call_function ~(| "H", [ 5 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "hg0" in
+  do~ M.substitute_var "hg0" [[ M.call_function ~(| "H", [ 6 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "hh0" in
+  do~ M.substitute_var "hh0" [[ M.call_function ~(| "H", [ 7 ] |) ]] in
+  (* Component *)
+  do~ M.declare_component "sha256compression" in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), M.var ~(| "nBlocks" |) |) ]] (
+    do~ M.substitute_var "sha256compression" [[ M.call_function ~(| "Sha256compression", ([] : list F.t) |) ]] in
+    do~ M.if_ [[ InfixOp.eq ~(| M.var ~(| "i" |), 0 |) ]] (* then *) (
+      do~ M.substitute_var "k" [[ 0 ]] in
+      do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), 32 |) ]] (
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "ha0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "hb0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "hc0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "hd0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "he0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "hf0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "hg0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "hh0", [Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+        do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+        M.pure BlockUnit.Tt
+      ) in
+      M.pure BlockUnit.Tt
+    ) (* else *) (
+      do~ M.substitute_var "k" [[ 0 ]] in
+      do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), 32 |) ]] (
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 0 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 1 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 2 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 3 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 4 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 5 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 6 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "i" |), 1 |)); Access.Component "out"; Access.Array (InfixOp.sub ~(| InfixOp.add ~(| InfixOp.mul ~(| 32, 7 |), 31 |), M.var ~(| "k" |) |))] |) ]] in
+        do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+        M.pure BlockUnit.Tt
+      ) in
+      M.pure BlockUnit.Tt
+    ) in
+    do~ M.substitute_var "k" [[ 0 ]] in
+    do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), 512 |) ]] (
+      do~ M.substitute_var "sha256compression" [[ M.var_access ~(| "paddedIn", [Access.Array (InfixOp.add ~(| InfixOp.mul ~(| M.var ~(| "i" |), 512 |), M.var ~(| "k" |) |))] |) ]] in
+      do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+      M.pure BlockUnit.Tt
+    ) in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), 256 |) ]] (
+    do~ M.substitute_var "out" [[ M.var_access ~(| "sha256compression", [Access.Array (InfixOp.sub ~(| M.var ~(| "nBlocks" |), 1 |)); Access.Component "out"; Access.Array (M.var ~(| "k" |))] |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.