diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-25 00:36:00 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-25 00:36:00 -0400 |
| commit | 027764b7854cc8f1a089d7a962b71a00ec291032 (patch) | |
| tree | dfeba94ff3251222ae4ba05e545949de13743453 /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | ec33e34bb2928cbaee1895417e19d744497fdf3b (diff) | |
Changed definition of [sub] to require proof that the modulus multiple actually is a multiple of the modulus. This allows for proving the Proper properties of [sub] based on its correctness proof alone, which has the modulus multiple correctness as a precondition.
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 31fab7cd8..28ff29081 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -428,7 +428,7 @@ Section Subtraction. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient}. Local Notation digits := (tuple Z (length limb_widths)). - Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff us vs }. + Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff coeff_mod us vs }. Proof. eexists. cbv [BaseSystem.add ModularBaseSystem.sub BaseSystem.sub]. @@ -439,10 +439,10 @@ Section Subtraction. := Eval cbv [proj1_sig sub_opt_sig] in proj1_sig (sub_opt_sig us vs). Definition sub_opt_correct us vs - : sub_opt us vs = sub coeff us vs + : sub_opt us vs = sub coeff coeff_mod us vs := proj2_sig (sub_opt_sig us vs). - Definition opp_opt_sig (us : digits) : { b : digits | b = opp coeff us }. + Definition opp_opt_sig (us : digits) : { b : digits | b = opp coeff coeff_mod us }. Proof. eexists. cbv [opp]. @@ -454,7 +454,7 @@ Section Subtraction. := Eval cbv [proj1_sig opp_opt_sig] in proj1_sig (opp_opt_sig us). Definition opp_opt_correct us - : opp_opt us = opp coeff us + : opp_opt us = opp coeff coeff_mod us := proj2_sig (opp_opt_sig us). End Subtraction. |