diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 14:31:18 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 14:32:48 -0700 |
| commit | d12f190a2ef6f129583f1fd69411638e237d731e (patch) | |
| tree | e2acde80fc0723047756b5a0f9dafb1a3f0d4600 /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | ffc5e19d56b808e61fac1d94a9dfddc7b86cfa5d (diff) | |
Express carry_simple in terms of carry_gen
Also make much of the remaining code outside of Pow2BaseProofs
independent of the precise definition of carry_simple. (We use [Local
Opaque] to enforce this modularity.
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 7c7004dce..d7e6f1c65 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -3,6 +3,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem. Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil. @@ -118,9 +119,10 @@ Section Carries. cbv [carry]. rewrite <- pull_app_if_sumbool. cbv beta delta - [carry carry_and_reduce Pow2Base.carry_simple Pow2Base.add_to_nth + [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_and_reduce_single Pow2Base.carry_simple Z.pow2_mod Z.ones Z.pred PseudoMersenneBaseParams.limb_widths]. + rewrite !add_to_nth_set_nth. change @Pow2Base.base_from_limb_widths with @base_from_limb_widths_opt. change @nth_default with @nth_default_opt in *. change @set_nth with @set_nth_opt in *. |