diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-19 15:37:56 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-10-19 23:16:51 -0400 |
| commit | 3586b26609773f345c788c8db24f85404d41140a (patch) | |
| tree | a860cfa015fbfea121ddfcca3ea4f45f36b6ef26 /_CoqProject | |
| parent | 4e62f74577d2ff56c03b283a6dd43595070ae38a (diff) | |
First pass at bounded version of GF25519
Boundedness is axiomatized as
```coq
Axiom ExprBinOp : Type.
Axiom ExprUnOp : Type.
Axiom interp_bexpr : ExprBinOp -> Specific.GF25519.fe25519 ->
Specific.GF25519.fe25519 -> Specific.GF25519.fe25519.
Axiom interp_uexpr : ExprUnOp -> Specific.GF25519.fe25519 ->
Specific.GF25519.fe25519.
Axiom radd : ExprBinOp.
Axiom rsub : ExprBinOp.
Axiom rmul : ExprBinOp.
Axiom ropp : ExprUnOp.
Axiom rinv : ExprUnOp.
Axiom radd_correct : forall x y, interp_bexpr radd x y = carry_add x y.
Axiom rsub_correct : forall x y, interp_bexpr rsub x y = carry_sub x y.
Axiom rmul_correct : forall x y, interp_bexpr rmul x y = mul x y.
Axiom ropp_correct : forall x, interp_uexpr ropp x = carry_opp x.
Axiom rinv_correct : forall x, interp_uexpr rinv x = inv x.
Axiom check_bbounds : ExprBinOp -> bool.
Axiom check_ubounds : ExprUnOp -> bool.
Axiom radd_bounded : check_bbounds radd = true.
Axiom rsub_bounded : check_bbounds rsub = true.
Axiom rmul_bounded : check_bbounds rmul = true.
Axiom ropp_bounded : check_ubounds ropp = true.
Axiom rinv_bounded : check_ubounds rinv = true.
Axiom bbounds_correct
: forall rexpr, check_bbounds rexpr = true
-> forall x y, is_bounded x = true
-> is_bounded y = true
-> is_bounded (interp_bexpr rexpr x y)
= true.
Axiom ubounds_correct
: forall rexpr, check_ubounds rexpr = true
-> forall x, is_bounded x = true
-> is_bounded (interp_uexpr rexpr x) =
true.
```
Questions:
- Some of this is very general and probably doesn't belong in this file
(e.g., [correct_le_le]). Should it stay, or move elsewhere?
- There's a lot of type munging that could be generalized to arbitrary
heterogenous lists; should it be generalized?
- How do we do [div] on bounded things? Currently, I have
```coq
Axiom div : forall (f g : fe25519), fe25519.
Axiom div_correct : forall a b : fe25519,
ModularBaseSystem.eq (proj1_fe25519 (div a b))
(ModularBaseSystem.div (proj1_fe25519 a)
(proj1_fe25519 b)).
```
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index de628d687..d60bebff6 100644 --- a/_CoqProject +++ b/_CoqProject @@ -124,6 +124,7 @@ src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v +src/Specific/GF25519Bounded.v src/Specific/SC25519.v src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v |