feat(core): finish run_from_shifts proof

formal-land · Jan 23, 2025 · 5a0b79f · 5a0b79f
1 parent f17d44c
commit 5a0b79f
Showing 1 changed file with 30 additions and 41 deletions.
diff --git a/Garden/01/Keccak.v b/Garden/01/Keccak.v
@@ -557,23 +557,23 @@ Module Keccak.
               let y_nat := Z.to_nat y_z in
               let x_nat := Z.to_nat x_z in
               let q_nat := Z.to_nat q_z in
-              let shifts_0 := nth_or_default 0%Z shifts (q_nat + (Z.to_nat QUARTERS) * (x_nat + (Z.to_nat DIM) * y_nat)) in
-              let shifts_1 := nth_or_default 0%Z shifts (1 + q_nat + (Z.to_nat QUARTERS) * (x_nat + (Z.to_nat DIM) * y_nat)) in
-              let shifts_2 := nth_or_default 0%Z shifts (2 + q_nat + (Z.to_nat QUARTERS) * (x_nat + (Z.to_nat DIM) * y_nat)) in
-              let shifts_3 := nth_or_default 0%Z shifts (3 + q_nat + (Z.to_nat QUARTERS) * (x_nat + (Z.to_nat DIM) * y_nat)) in
+              let shifts_0 := simulation_grid_400 shifts 0 y_nat x_nat q_nat in
+              let shifts_1 := simulation_grid_400 shifts 1 y_nat x_nat q_nat in
+              let shifts_2 := simulation_grid_400 shifts 2 y_nat x_nat q_nat in
+              let shifts_3 := simulation_grid_400 shifts 3 y_nat x_nat q_nat in 
               shifts_0 + 2 ^ 1 * shifts_1 + 2 ^ 2 * shifts_2 + 2 ^ 3 * shifts_3
-          | _, _, _ => 0
+              | _, _, _ => 0
           end
       end
     else if Z.of_nat (List.length shifts) =? 80 then
       match x, q with
       | Some x_z, Some q_z =>
           let x_nat := Z.to_nat x_z in
           let q_nat := Z.to_nat q_z in
-          let shifts_0 := nth_or_default 0%Z shifts (q_nat + (Z.to_nat QUARTERS) * x_nat) in
-          let shifts_1 := nth_or_default 0%Z shifts (1 + q_nat + (Z.to_nat QUARTERS) * x_nat) in
-          let shifts_2 := nth_or_default 0%Z shifts (2 + q_nat + (Z.to_nat QUARTERS) * x_nat) in
-          let shifts_3 := nth_or_default 0%Z shifts (3 + q_nat + (Z.to_nat QUARTERS) * x_nat) in
+          let shifts_0 := simulation_grid_80 shifts 0 x_nat q_nat in
+          let shifts_1 := simulation_grid_80 shifts 1 x_nat q_nat in
+          let shifts_2 := simulation_grid_80 shifts 2 x_nat q_nat in
+          let shifts_3 := simulation_grid_80 shifts 3 x_nat q_nat in
           shifts_0 + 2 ^ 1 * shifts_1 + 2 ^ 2 * shifts_2 + 2 ^ 3 * shifts_3
       | _, _ => 0
       end
@@ -596,43 +596,32 @@ Module Keccak.
         lia.
       }
       {
-        destruct y. destruct x. destruct q.
-        { unfold nth_or_default.
-          replace 0 with (Variable_.eval Variable_.Zero) by reflexivity.
-          repeat rewrite (List.map_nth Variable_.eval).
-          repeat set (List.nth _ _ _).
-          with_strategy opaque [Z.add Z.mul var_two_pow] cbn.
-          rewrite !var_two_pow_correct.
-          rewrite !run_grid_400.
-          unfold simulation_grid_400.
-          unfold nth_or_default.
-          replace 0 with (Variable_.eval Variable_.Zero) by reflexivity.
-          repeat rewrite (List.map_nth Variable_.eval).
-          repeat set (List.nth _ _ _).
-          with_strategy opaque [Z.add Z.mul var_two_pow] cbn.
-          repeat f_equal.
-          { admit. }
-          all: lia.
-        }
-        all: trivial.
+        destruct y, x, q; trivial.
+        rewrite <- !run_grid_400.
+        with_strategy opaque [Z.add Z.mul var_two_pow] cbn.
+        rewrite !var_two_pow_correct.
+        lia.
       }
     }
     { destruct (Z.of_nat (Datatypes.length shifts) =? 80) eqn:Heq80.
-      { destruct x, q.
-        { unfold nth_or_default.
-          replace 0 with (Variable_.eval Variable_.Zero) by reflexivity.
-          repeat rewrite (List.map_nth Variable_.eval).
-          repeat set (List.nth _ _ _).
-          with_strategy opaque [Z.add Z.mul var_two_pow] cbn.
-          rewrite !var_two_pow_correct.
-          rewrite !grid_80_is_valid.
-          { admit. }
-          all: trivial.
-          all: lia.  }
+      { destruct x. 
+        { destruct q.
+          { unfold nth_or_default.
+            replace 0 with (Variable_.eval Variable_.Zero) by reflexivity.
+            repeat rewrite (List.map_nth Variable_.eval).
+            repeat set (List.nth _ _ _). 
+            with_strategy opaque [Z.add Z.mul var_two_pow] cbn.
+            rewrite !var_two_pow_correct.
+            rewrite <- !run_grid_80.
+            lia.
+          }
+          { trivial. }
+        }
+        { trivial. }
       }
-      trivial.
+      { reflexivity. }
     }
-  Admitted.
+  Qed.
 
   (*
   fn constrain_theta(&mut self, step: Steps) -> Vec<Vec<Vec<Self::Variable>>> {