Remove names from the ECDSA proof that do not resolve to anything, and

are unnecessary to the proof.Now that we are being more carefule about naming, these produce errors.
GaloisInc · Oct 30, 2020 · 3d47c3d · 3d47c3d
1 parent 07c4690
commit 3d47c3d
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/examples/ecdsa/ecdsa.saw b/examples/ecdsa/ecdsa.saw
@@ -579,7 +579,7 @@ let ec_full_add_spec ss = do {
     unfolding ["p384_ec_full_add"];
     simplify ss;
     unint_z3 [ "p384_field_add", "p384_field_sub", "p384_field_mul"
-             , "p384_full_add", "p384_mod_half", "p384_ec_double"
+             , "p384_mod_half", "p384_ec_double"
              ];
   };
 };
@@ -598,7 +598,7 @@ let ec_full_sub_spec ss = do {
     simplify ss;
     unint_z3 [ "p384_ec_full_add", "p384_ec_double", "p384_field_add"
              , "p384_field_sub", "p384_field_mul"
-             , "p384_full_add", "p384_mod_half"
+             , "p384_mod_half"
              ];
   };
 };
@@ -811,7 +811,7 @@ let ec_twin_mul_spec ss = do {
     beta_reduce_goal;
     simplify ss;
     unint_z3 [ "p384_ec_twin_mul_init", "p384_ec_twin_mul_aux1"
-             , "p384_ec_twin_mul_aux2", "p384_ec_twin_mul_aux_f"
+             , "p384_ec_twin_mul_aux2"
              ];
   };
 };