Merge pull request #879 from GaloisInc/fix-ecdsa

Fix ecdsa example proofs.
GaloisInc · Oct 28, 2020 · d12eb10 · d12eb10
2 parents 66a2d40 + 94e1558
commit d12eb10
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 19 deletions.
diff --git a/examples/ecdsa/ecdsa-crucible.saw b/examples/ecdsa/ecdsa-crucible.saw
@@ -32,21 +32,6 @@ let {{
 
   jget a (i : [32]) = a @ i
 
-  p384_mod_div (p,x,y) = egcd(p,0,y,x)
-    where
-      mh = p384_field::p384_mod_half
-      ms = p384_field::p384_mod_sub
-      /* In code below, a is always odd. */
-      egcd(a,ra,b,rb) =
-        if b == 0 then
-          ra
-        else if (b && 1) == 0 then /* b is even. */
-          egcd(a, ra, b >> 1, mh(p, rb))
-        else if a < b then
-          egcd(a, ra, (b - a) >> 1, mh(p, ms(p, rb, ra)))
-        else
-          egcd(b, rb, (a - b) >> 1, mh(p, ms(p, ra, rb)))
-
   field_prime = 0xffffffffffffffffffffffffffffffffffffffffffffffff #
                 0xfffffffffffffffeffffffff0000000000000000ffffffff
 
@@ -563,7 +548,7 @@ p384_curve_field_sq_simp <- do {
 };
 p384_curve_field_div_simp <- do {
   let {{ thm x y = ecc::p384_curve.point_ops.group_field.div (x,y) ==
-                   p384_mod_div (p384_field::p384_group_size, x, y) }};
+                   p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }};
   let t = unfold_term ["thm"] {{ thm }};
   let t = rewrite ss0 t;
   //print_term t;
@@ -594,7 +579,7 @@ p384_curve_is_val_simp <- do {
   prove_print z3 t;
 };
 p384_curve_norm_simp <- do {
-  let {{ thm x = ecc::p384_curve.point_ops.group_field.norm x ==
+  let {{ thm x = ecc::p384_curve.point_ops.group_field.normalize x ==
                  (if x < p384_field::p384_group_size
                   then x
                   else x - p384_field::p384_group_size) }};
@@ -997,7 +982,7 @@ mod_div_ov <- method_skip "mod_div"
     (pp, p) <- ecdsa_arr384 "p";
     jvm_execute_func [this, pra, px, py, pp];
     //ecdsa_uses_temps this;
-    ecdsa_assign_arr384 pra {{ p384_mod_div (p, x, y) }};
+    ecdsa_assign_arr384 pra {{ p384_field::p384_mod_div (p, x, y) }};
   }
   abc;
 

diff --git a/examples/ecdsa/ecdsa.saw b/examples/ecdsa/ecdsa.saw
@@ -1123,7 +1123,6 @@ let main = do {
     , "and"
     , "or"
     , "not"
-    , "bitvector"
     ] ss4;
 
   p384_point_ops_add_simp <- do {
-Original file line number
+Diff line change
@@ Expand Up / @@ -1123,7 +1123,6 @@ let main = do { @@
         , "and"
         , "or"
         , "not"
-        , "bitvector"
         ] ss4;
       p384_point_ops_add_simp <- do {
@@ Expand Down @@