aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
...
* Add reification of various operationsGravatar Jason Gross2016-10-30
| | | | | We split the reification up into separate files, one operation per file, so that we can run all the reification in parallel when building.
* Add initial work on reifying GF25519 stuffGravatar Jason Gross2016-10-30
|
* Add InterpWfGravatar Jason Gross2016-10-28
|
* Add InterpWfRelGravatar Jason Gross2016-10-28
|
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
|
* Merge pull request #84 from mit-plv/rsloan-phoasGravatar Jason Gross2016-10-27
|\ | | | | Patching master with most of my Conversion refactors
* | Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
| | | | | | | | That is, for add, sub, mul, opp, freeze, ge_modulus, pack, and unpack.
* | Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
| | | | | | | | This way we will have a faster build of reification things
* | Add WfRelReflectiveGravatar Jason Gross2016-10-27
| | | | | | | | Not sure if it's needed, but it was pretty easy to write...
* | Add WfReflectiveGenGravatar Jason Gross2016-10-27
| | | | | | | | Prep for WfRelReflective
* | Add Wf proofs about MapInterpGravatar Jason Gross2016-10-27
| |
| * Merge branch 'master' into rsloan-phoasGravatar 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.
| * Fix 8.4 buildGravatar Jason Gross2016-10-22
| |
| * Merge branch 'master' into pr/84Gravatar Jason Gross2016-10-22
| |\ | |/ |/|
* | Fix src/Experiments/Ed25519.v for Coq 8.4Gravatar Jason Gross2016-10-22
| | | | | | | | Using very dubious module hackery.
| * merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
| |\ | |/ |/|
| * committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
| |
* | Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
| |
* | Merge branch 'master' into instantiation-rsloan-phoasGravatar Jason Gross2016-10-20
|\ \
| * | 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)). ```
* | | Start instantiating boundedness thingsGravatar Jason Gross2016-10-19
| |/ |/|
| * Rename and clean up exponent codeGravatar Jason Gross2016-10-17
| |
| * Initial work on exponent field as ZGravatar Jason Gross2016-10-17
| |
| * Add Z as ZBoundedGravatar Jason Gross2016-10-16
| |
* | Making sub bounds actually tightGravatar Robert Sloan2016-10-14
| |
* | Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
| |
| * Add src/BoundedArithmetic/Eta.vGravatar Jason Gross2016-10-13
| |
| * remove EncodingLemmas from _CoqProject (file deleted by Andres in commit ↵Gravatar jadep2016-10-12
| | | | | | | | 9379415c)
| * Add Ed25519 to _CoqProjectGravatar Jason Gross2016-10-12
| |
| * Add some admitted x86->ZLike proofsGravatar Jason Gross2016-10-10
| |
| * Update _CoqProjectGravatar Jason Gross2016-10-10
| |
| * Add shl,shr,shrd to repeated doublingGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------------------------- 0m03.99s | Total | 0m03.08s || +0m00.90s --------------------------------------------------------------------------------------------------------- 0m01.14s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.02s || +0m00.11s 0m00.52s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.53s || -0m00.01s 0m00.51s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.51s || +0m00.00s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | N/A || +0m00.47s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.54s || -0m00.08s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | N/A || +0m00.46s 0m00.44s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.49s || -0m00.04s
| * Add proofs for doubling shl,shr,shrdGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------------------ 0m14.81s | Total | 0m00.00s || +0m14.81s ------------------------------------------------------------------------------------------------ 0m08.87s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | N/A || +0m08.86s 0m02.82s | BoundedArithmetic/Double/Proofs/ShiftLeft | N/A || +0m02.81s 0m02.72s | BoundedArithmetic/Double/Proofs/ShiftRight | N/A || +0m02.72s 0m00.40s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | N/A || +0m00.40s
| * Some work on x86 and bounded repeated thingsGravatar Jason Gross2016-10-09
| |
| * 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
| * Add a variant of [map] on reflective things that changes the interp functionGravatar Jason Gross2016-10-07
| |
* | Merge _CoqProjectGravatar Rob Sloan2016-10-06
|\ \
| | * Moved PointEncoding out of SpecGravatar jadep2016-10-06
| | |
| | * Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
| | |
| | * Add some more instructionsGravatar Jason Gross2016-10-04
| |/ |/|
* | Wrote proofs necessary to fill in all point-encoding related context ↵Gravatar jadep2016-10-03
| | | | | | | | variables in EdDSARepChange.v
* | Spec: add ed25519Gravatar Andres Erbsen2016-10-03
| |
| * Complete example + GF25519 outline in Pipeline.vGravatar Robert Sloan2016-10-02
| |
* | Small example of bounds-calculation with dependent types (#61)Gravatar Jason Gross2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | This might properly belong in Experiments rather than TestCase. It demos the ability to transform from one kind of constants to another kind, and to plug bounds calculation functions into [var] to get bounds. There's not currently any sort of correctness theorem, and I'm not entirely sure what one would look like. Probably something that says that if you map a function over the syntax tree and then interpret, you could instead have first interpreted and then applied the function. I'm hopeful that this will provide a template for integrating this version of the syntax with rsloan-phoas.
* | montgomery-curveGravatar Andres Erbsen2016-09-28
| |
* | Merge pull request #69 from JasonGross/scalable-scalarsGravatar Jason Gross2016-09-26
|\ \ | | | | | | Scalable Scalars, Dead Code Removal, Register Assignment
* | | add Montgomery x-coordinate Diffie-Hellman and Curve25519Gravatar Andres Erbsen2016-09-26
| | |
| | * Fix merge with masterGravatar Robert Sloan2016-09-24
| | |\ | |_|/ |/| |
| | * Large-scale refactoring of src/AssemblyGravatar Robert Sloan2016-09-24
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 17:47:04 +0000