Skip to content

Commit

Permalink
Adapt ecdsa-crucible.saw to PR #910 "structured-names".
Browse files Browse the repository at this point in the history
SAW now performs name resolution on each argument to `unint_z3`
and other uninterpreted-function tactics; some unused names that
do not resolve to anything needed to be removed from the ecdsa
proof.
  • Loading branch information
Brian Huffman committed Nov 25, 2020
1 parent 27d6f2d commit ab51ebd
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions examples/ecdsa/ecdsa-crucible.saw
Original file line number Diff line number Diff line change
Expand Up @@ -1374,7 +1374,7 @@ ec_full_add_ov <- method "ec_full_add"
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"
];
};

Expand Down Expand Up @@ -1422,7 +1422,7 @@ ec_full_sub_ov <- method "ec_full_sub"
simplify ec_full_sub_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"
];
};

Expand Down Expand Up @@ -1724,7 +1724,7 @@ ec_twin_mul_ov <- method "ec_twin_mul"
simplify ss;
// TODO: see if some rules from twin_mul_init_ss can help.
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"
];
};

Expand Down

0 comments on commit ab51ebd

Please sign in to comment.