| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
@jadephilipoom the remaining context to prove is in
src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v and
src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v:
```coq
Local Notation conditional_subtract_cps := (@drop_high_cps
R_numlimbs).
(*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT},
(T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg],
and drops high bit *)
Axiom conditional_subtract : T (S R_numlimbs) -> T R_numlimbs (*
computes [arg - N] if [R <= arg], and drops high bit *).
Local Lemma small_add : forall n a b, small a -> small b -> small
(@add n a b).
Proof.
intros; apply Saturated.small_add; auto; try lia.
cbv [uweight].
rewrite ?Znat.Nat2Z.inj_succ, ?Z.pow_succ_r by lia.
try nia.
Admitted.
Local Lemma small_add' : forall n a b, small a -> small b -> small
(@add' n a b).
Proof.
intros; apply Saturated.small_add; auto; try lia.
cbv [uweight].
rewrite !Znat.Nat2Z.inj_succ, !Z.pow_succ_r by lia.
try nia.
Admitted.
Axiom conditional_subtract_cps_id : forall v cpsT f,
@conditional_subtract_cps v cpsT f = f (@conditional_subtract _ v).
Axiom small_scmul : forall (n : nat) (a : Z) (v : T n),
small v -> 0 <= a < Z.pos r -> 0 <= eval v < R -> small (scmul a
v).
Axiom eval_conditional_subtract
: forall v : T (S R_numlimbs),
small v ->
0 <= eval v < eval N + Z.pos R ->
eval (conditional_subtract v) = eval v + (if Z.pos R <=? eval v
then - eval N else 0).
Axiom small_conditional_subtract
: forall v : T (S R_numlimbs),
small v ->
0 <= eval v < eval N + Z.pos R ->
small (conditional_subtract v).
```
|
Jason Gross