| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
arguments since more context variables were used in the definitions than in the placeholder axioms
|
| | |
|
| |
|
|
| |
Partial work towards #218
|
| |
|
|
|
| |
Note that this makes the axiom we added false. It has a very long and
descriptive name to account for this fact.
|
| | |
|
| |
|
|
| |
Not sure if locally adding hypotheses is the best way to do it.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
@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).
```
|
| | |
|
| |
|
|
| |
Maybe it'll result in better output code with fewer zeros?
|
| | |
|
| |
|
|
|
|
|
| |
The new parameterized definitions and proofs are in
WordByWord/Abstract/Dependent/*; the old ones are untouched (and unused)
in WordByWord/Abstract/*. I replaced definitions I didn't know how to
write in the Saturated API with the use of an axiom.
|
| |
|
|
|
|
| |
I didn't want to bother redoing all of the proofs that I'd already done,
so instead I prove the cps'ified version equal to the non-cps version,
and transfer over the proofs that way.
|
| |
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/commit/b4b711cba32a21806c6c0aae53be40c04af60cb3#commitcomment-22521097
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307776611
|
| |
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307772410
|
| |
|
|
|
| |
Some of the proofs are a bit monsterous. It'd be nice to go back and
automate them more sometime.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Also add [small], as per
https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307568416
|
| | |
|
| |
|
|
| |
It's been migrated to Definitions.v and Proofs.v in the same directory
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Transcribe
https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-301334813
Not sure if it's right, but now I'll try proofs.
|
| |
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307212425
|
| | |
|
| | |
|
Jason Gross
Andres Erbsen
jadep