aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Collapse)AuthorAge
* Simplify proof of proj1_fe25519_encodeGravatar Jason Gross2016-10-27
|
* Add lemmas about GF25519BoundedCommon.{encode,decode}Gravatar Jason Gross2016-10-27
|
* Switch to bounded ZGravatar Jason Gross2016-10-25
| | | | | We don't have working word code yet, because the reification code currently does spurious word->N->Z->N->word conversions everywhere. So we use Z instead.
* Adjust bound on final word in wire_digits to 31Gravatar Jason Gross2016-10-24
|
* Fix bounds on wire_digitsGravatar Jason Gross2016-10-24
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/86#issuecomment-255839706
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
|
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
|
* Finish twedprm_ERep proofGravatar Jason Gross2016-10-23
| | | | (cc @andres-erbsen)
* Make some things instancesGravatar Jason Gross2016-10-23
|
* Generalize field_from_redundant_representationGravatar Jason Gross2016-10-23
| | | | Note that the old version did not need phi', but the new version does
* Add decode to GF25519BoundedCommonGravatar Jason Gross2016-10-22
|
* Make [vm_compute] on Bounded word reasonableGravatar Jason Gross2016-10-22
| | | | We no longer store the type of proofs of [<=] in the term itself; this makes it amenable to vm_compute
* Fix divergence in src/Specific/GF25519Bounded.vGravatar Jason Gross2016-10-22
| | | | Not sure how I missed this...
* Unfold interp stuff in Assembly/GF25519BoundedInstantiationGravatar Jason Gross2016-10-22
|
* Add bounded sqrtGravatar Jason Gross2016-10-22
|
* final touches/fixes for freeze restructuringGravatar jadep2016-10-22
|
* add arguments that I forgotGravatar jadep2016-10-22
|
* Modified [freeze] to be more reifyableGravatar jadep2016-10-22
|
* pow, not pow_opt, in Specific/GF25519Gravatar Jason Gross2016-10-21
|
* Add word64eqb_ZeqbGravatar Jason Gross2016-10-21
|
* Sane fieldwisebGravatar Jason Gross2016-10-21
|
* Make eqb sane (help from Jade)Gravatar Jason Gross2016-10-21
|
* Remove axioms from src/Specific/GF25519Bounded.v, plug assemblyGravatar Jason Gross2016-10-21
|
* A bit of initial setup on correct_and_bounded proofs in ↵Gravatar Jason Gross2016-10-20
| | | | GF25519BoundedInstantiation
* Plug bounded into assembly stuffGravatar Jason Gross2016-10-20
|
* Remove code that should have been removedGravatar Jason Gross2016-10-20
|
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
|
* Add todoGravatar Jason Gross2016-10-20
|
* Switch from bounded Z to bounded wordGravatar Jason Gross2016-10-20
|
* More specific bounded requirements, implement invGravatar Jason Gross2016-10-19
|
* First pass at bounded version of GF25519Gravatar Jason Gross2016-10-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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)). ```
* Removed the lingering TODO and print statement that @JasonGross helpfully ↵Gravatar jadep2016-10-19
| | | | pointed out
* Fill in admits for field with carry_add, carry_opp, and carry_subGravatar jadep2016-10-19
|
* Define carry_opp in terms of carry_subGravatar Jason Gross2016-10-19
|
* Add opt versions of add, sub, oppGravatar Jason Gross2016-10-19
|
* Fix out of memory error for 8.5,8.5pl1Gravatar Jason Gross2016-10-19
|
* Fix for Coq 8.4 evar propogationGravatar Jason Gross2016-10-18
|
* Fix missing importsGravatar Jason Gross2016-10-17
|
* Remove broken importsGravatar Jason Gross2016-10-17
|
* Rename and clean up exponent codeGravatar Jason Gross2016-10-17
|
* Remove admits with the help of AndresGravatar Jason Gross2016-10-17
|
* Fill in more proofsGravatar Jason Gross2016-10-17
|
* Initial work on exponent field as ZGravatar Jason Gross2016-10-17
|
* Clean up ge_modulus definition in SpecificGravatar jadep2016-10-12
|
* Added top-level modulus comparison operation so field-element decoding can ↵Gravatar jadep2016-10-12
| | | | return None if input is greater than modulus
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
| | | | | | | | | | | | | | | | | | | | | | | | Some help from jadep on BitwiseOr. After | File Name | Before || Change -------------------------------------------------------------------------------------- 0m39.26s | Total | 0m36.03s || +0m03.23s -------------------------------------------------------------------------------------- N/A | BoundedArithmetic/DoubleBoundedProofs | 0m21.20s || -0m21.19s 0m07.47s | BoundedArithmetic/Double/Proofs/Multiply | N/A || +0m07.46s 0m06.70s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | N/A || +0m06.70s 0m05.14s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | N/A || +0m05.13s 0m02.75s | BoundedArithmetic/Double/Proofs/Decode | N/A || +0m02.75s 0m08.06s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.05s || +0m00.00s 0m02.01s | Specific/FancyMachine256/Barrett | 0m02.13s || -0m00.12s 0m02.00s | Specific/FancyMachine256/Montgomery | 0m02.06s || -0m00.06s 0m01.75s | Specific/FancyMachine256/Core | 0m01.66s || +0m00.09s 0m00.90s | BoundedArithmetic/Double/Proofs/LoadImmediate | N/A || +0m00.90s 0m00.88s | BoundedArithmetic/Double/Proofs/BitwiseOr | N/A || +0m00.88s 0m00.58s | BoundedArithmetic/Double/Proofs/SelectConditional | N/A || +0m00.57s 0m00.53s | BoundedArithmetic/ArchitectureToZLike | 0m00.47s || +0m00.06s 0m00.49s | BoundedArithmetic/Double/Core | N/A || +0m00.49s N/A | BoundedArithmetic/DoubleBounded | 0m00.46s || -0m00.46s
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
|
* Add bitwise and, remove mkl from fancyGravatar Jason Gross2016-10-03
|
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
|
* Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
| | | | | By being careful about building the expressions in the first place, we no longer need it, and can rely on dead code elimination.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 05:47:11 +0000