diff options
author | 2017-06-29 13:37:20 -0400 | |
---|---|---|
committer | 2017-06-29 13:37:20 -0400 | |
commit | 8eec11bfb6d97a3cbb21e74f26c469157c58e2d8 (patch) | |
tree | 0d6599457da7deb807db1fec1caf90200a58727b /src | |
parent | ff89c5cc3fb7240c1e87d4234ab8b84859fc23ea (diff) |
Fix unfolding to not unfold sub_with_get_borrow in P256
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/MontgomeryP256_128.v | 17 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD64/MontgomeryP256.v | 8 |
2 files changed, 16 insertions, 9 deletions
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v index 086a454e8..323be5533 100644 --- a/src/Specific/MontgomeryP256_128.v +++ b/src/Specific/MontgomeryP256_128.v @@ -34,7 +34,7 @@ Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. (* cbv [ r wt sz p256 @@ -42,9 +42,10 @@ Proof. CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' CPSUtil.flat_map_cps CPSUtil.fold_right_cps CPSUtil.map_cps CPSUtil.Tuple.left_append_cps CPSUtil.firstn_cps CPSUtil.combine_cps CPSUtil.on_tuple_cps CPSUtil.update_nth_cps CPSUtil.from_list_default_cps CPSUtil.from_list_default'_cps fst snd length List.seq List.hd List.app - redc redc_cps redc_loop_cps redc_body_cps + redc pre_redc_cps redc_cps redc_loop_cps redc_body_cps Positional.to_associational_cps Saturated.divmod_cps + Saturated.conditional_sub_cps Saturated.scmul_cps Saturated.uweight Saturated.Columns.mul_cps @@ -52,13 +53,19 @@ Proof. (*Z.of_nat Pos.of_succ_nat Nat.pred Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*) Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps + CPSUtil.Tuple.map2_cps Saturated.Columns.from_associational_cps Saturated.Associational.multerm_cps + Saturated.Positional.sat_add_cps + Saturated.Positional.sat_sub_cps + Saturated.Positional.chain_op_cps + Saturated.Positional.chain_op'_cps Saturated.Columns.compact_cps Saturated.Columns.compact_step_cps Saturated.Columns.compact_digit_cps Saturated.drop_high_cps Saturated.add_cps + Saturated.add_S1_cps Saturated.Columns.add_cps Saturated.Columns.cons_to_nth_cps Nat.pred @@ -138,7 +145,7 @@ Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. @@ -149,7 +156,7 @@ Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. @@ -160,7 +167,7 @@ Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v index d90a63bfb..ae5a3cb43 100644 --- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v +++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v @@ -34,7 +34,7 @@ Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. (* cbv [ r wt sz p256 @@ -139,7 +139,7 @@ Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. @@ -150,7 +150,7 @@ Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. @@ -161,7 +161,7 @@ Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. |