aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
* 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
|
* 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
|
* 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
| |
| * Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
| |
| * Add dead code eliminationGravatar Jason Gross2016-09-22
| |
| * Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
|/ | | | | | | | | | | | | | The register assigner will return [None] if you give it an invalid assignment (too short, attempting to eliminate live code, attempting to merge registers that can't be merged). No correctness proofs yet, nor any sort of automatic register assignment. I'm planning to write a dead-code-eliminator register assigner next. It should also be moderately straight-forward to write a default register allocator, or perhaps a register post-allocator, that takes a manual register allocation, and renumbers variables in a greedy way. (This would let you pre-specify that some registers should be merged, but leave the rest of the assignment up to the algorithm.)
* Revert "Update _CoqProject"Gravatar Jason Gross2016-09-22
| | | | This reverts commit 1628cb14799db7af9eb13e49ae89f50d8f527301.
* move eddsa rep changeGravatar Andres Erbsen2016-09-22
|
* Update _CoqProjectGravatar Jason Gross2016-09-22
|
* Add some util files for reflective let bindingsGravatar Jason Gross2016-09-21
|
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
|
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
| | | | Experiments/SpecEd25519 will come back soon
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
|
* Add generalized version of Wf parameterized on relGravatar Jason Gross2016-09-15
| | | | | | This should allow a nice elegant abstract way of doing bounds analysis. It's possible that wf should be redefined in terms of rel_wf.
* Move FancyMachine from Experiments to SpecificGravatar Jason Gross2016-09-08
| | | | | | | | | | Quoting Andres: > I am leaning towards putting this in Specifc instead of Experiments -- it > seems like complete result on its own, these files are unlikely to be reused > for something else, and I don't think we are expecting to need to remove it > any time soon. Currently, `Specific` code does not quantify over anything (no > context variables), but this seems secondary. We could make versions of this > with the curve constants plugged in, though.
* Add Barrett and Montgomery for the 256-bit machineGravatar Jason Gross2016-09-07
| | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------ 0m12.69s | Total | 0m00.00s || +0m12.69s ------------------------------------------------------------------------ 0m06.96s | Experiments/FancyMachineMontgomery256 | N/A || +0m06.96s 0m03.07s | Experiments/FancyMachineBarrett256 | N/A || +0m03.06s 0m02.67s | Experiments/FancyMachine256 | N/A || +0m02.67s
* Add Common Subexpression EliminationGravatar Jason Gross2016-09-06
|
* Add correctness of interpretation of linearize and inline_constGravatar Jason Gross2016-09-05
|
* Add LinearizeWfGravatar Jason Gross2016-09-05
| | | | The proof of wf-preservation for inline_const isn't finished yet, though...
* Fix order of binders, and add WfProofsGravatar Jason Gross2016-09-05
|
* Fix _CoqProjectGravatar Jason Gross2016-09-05
|
* Remove ReifyDirectGravatar Jason Gross2016-09-05
| | | | It's probably not going to be used
* A helper lemma for [Wf]Gravatar Jason Gross2016-09-05
| | | | | | | | | This method allows a proof term that's linear in the term being proven well-founded, rather than exponential in it. By factoring out all of the reasoning about expressions, we can incur overhead equal to (the number of constants) + (the number of let-bindings) + (the number of variables used), all without mentioning the term itself; [vm_compute] can do the appropriate reduction for us.
* PHOAS syntaxGravatar Jason Gross2016-09-05
| | | | | | | We also have linearization of function application / lets, constant-inlining, and reification. This closes #58.
* Add a file about pointed PropsGravatar Jason Gross2016-09-05
|
* Rename congrunce_option to inversion_option, add [inversion_prod]Gravatar Jason Gross2016-08-31
|
* Integrate suggestions from AndresGravatar Jason Gross2016-08-25
|
* Rework bounded proofsGravatar Jason Gross2016-08-24
| | | | | | | | | | Now the rewrite strategy no longer relies on projections of anything other than [decode], and the conversion to ZLike is simpler. Modulo some annoyingly delicate arithmetic around things like [2^n * 2^n = 2^(2*n)] and whether to factor [(decode (fst x) + decode (snd x) >> n) >> b] as [decode x >> n] or as [shrd (fst x) (snd x) n], the proofs bascially go by pulling/pushing decodes.
* Merge remote-tracking branch 'upstream/master' into bounded-interfaceGravatar Jason Gross2016-08-24
|\
| * Removed now-obsolete ModularBaseSystemField.v; field lemmas for ↵Gravatar jadep2016-08-24
| | | | | | | | ModularBaseSystem are now in ModularBaseSystemProofs.v and Specific/
* | Update _CoqProjectGravatar Jason Gross2016-08-23
| |
* | Hook up the bounded interface, finish proofsGravatar Jason Gross2016-08-23
| |
* | Initial work on an architecture interface for ℤ/nℤGravatar Jason Gross2016-08-23
|/ | | | | This provides a cleaner interface for the bottom level implementation, as well as an implementation of multiplying 128x128 -> 256.
* Specify a type of bounded integers for mod arithGravatar Jason Gross2016-08-09
| | | | Also use it to implement Montgomery reduction and Barrett reduction.
* Define Montgomery reduction / multiplication on Z (#42)Gravatar Jason Gross2016-08-05
| | | | | | This is partly done for my own benefit, to internalize how Montgomery multiplication works, and partly done as a template for word-based Montgomery multiplication when the carrying does not take advantage of the fact that we are using a pseudomersenne prime.
* Implement Barrett Reduction following HAC 14.42 (#45)Gravatar Jason Gross2016-08-04
| | | | | | From http://cacr.uwaterloo.ca/hac/about/chap14.pdf This should take care of most of #43, at least the specification on Z part of it.
* Add a generalized version of Barrett Reduction (#44)Gravatar Jason Gross2016-08-04
| | | | | | | | | In this version, we split up the integer division so that we are less likely to overflow in intermediate computations. This is still not the version in HAC 14.42; that version also does early reduction modulo b^(k+1). This is work towards #43
* Add ZUtil lemmas, and Util.BoolGravatar Jason Gross2016-08-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m43.58s | Total | 1m44.69s || -0m01.10s ---------------------------------------------------------------------------------- 0m32.94s | Specific/GF25519 | 0m33.18s || -0m00.24s 0m15.34s | ModularArithmetic/ModularBaseSystemProofs | 0m15.35s || -0m00.00s 0m11.42s | Experiments/SpecEd25519 | 0m11.46s || -0m00.04s 0m07.12s | Specific/GF1305 | 0m07.38s || -0m00.25s 0m04.04s | ModularArithmetic/Pow2BaseProofs | 0m04.09s || -0m00.04s 0m03.82s | ModularArithmetic/Tutorial | 0m03.79s || +0m00.02s 0m03.81s | BaseSystemProofs | 0m03.71s || +0m00.10s 0m03.16s | ModularArithmetic/ModularBaseSystemOpt | 0m03.23s || -0m00.06s 0m02.76s | Util/ZUtil | 0m02.79s || -0m00.03s 0m01.63s | ModularArithmetic/PrimeFieldTheorems | 0m01.65s || -0m00.02s 0m01.58s | Encoding/PointEncodingPre | 0m01.51s || +0m00.07s 0m01.57s | ModularArithmetic/ModularArithmeticTheorems | 0m01.59s || -0m00.02s 0m01.33s | BaseSystem | 0m01.50s || -0m00.16s 0m01.09s | ModularArithmetic/ExtendedBaseVector | 0m01.13s || -0m00.03s 0m00.95s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.97s || -0m00.02s 0m00.93s | ModularArithmetic/BarrettReduction/Z | 0m00.98s || -0m00.04s 0m00.91s | Util/NumTheoryUtil | 0m01.19s || -0m00.27s 0m00.91s | ModularArithmetic/ModularBaseSystemField | 0m00.91s || +0m00.00s 0m00.81s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.81s || +0m00.00s 0m00.74s | Experiments/SpecificCurve25519 | 0m00.70s || +0m00.04s 0m00.65s | Encoding/ModularWordEncodingTheorems | 0m00.72s || -0m00.06s 0m00.65s | Encoding/ModularWordEncodingPre | 0m00.62s || +0m00.03s 0m00.64s | Testbit | 0m00.66s || -0m00.02s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.63s || +0m00.00s 0m00.63s | Spec/ModularWordEncoding | 0m00.63s || +0m00.00s 0m00.60s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.03s 0m00.59s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || -0m00.02s 0m00.57s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.61s || -0m00.04s 0m00.56s | ModularArithmetic/Pre | 0m00.48s || +0m00.08s 0m00.41s | ModularArithmetic/Pow2Base | 0m00.42s || -0m00.01s 0m00.38s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.43s || -0m00.04s 0m00.38s | Spec/ModularArithmetic | 0m00.39s || -0m00.01s 0m00.04s | Util/Bool | N/A || +0m00.04s
* Add HProp, IsomorphismGravatar Jason Gross2016-07-29
|
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
|
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I do hereby revoke the privilege of [intuition] to grab random hints from random databases. This privilege is reserved for [debug_intuition], which comes with a warning about not being used in production code. This tactic is useful in conjunction with `Print Hint *`, to discover what hint databases the hints were grabbed from. (Suggestions for renaming [debug_intuition] welcome.) Any file using [intuition] must [Require Export Crypto.Util.FixCoqMistakes.]. It's possible we could lift this restriction by compiling [FixCoqMistakes] separately, and passing along `-require FixCoqMistakes` to Coq. Should we do this? After | File Name | Before || Change ------------------------------------------------------------------------------------ 3m29.54s | Total | 4m33.13s || -1m03.59s ------------------------------------------------------------------------------------ 0m03.75s | BaseSystemProofs | 0m43.84s || -0m40.09s 0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.48s || +0m08.09s 0m03.04s | Util/ListUtil | 0m11.18s || -0m08.14s 0m01.62s | ModularArithmetic/PrimeFieldTheorems | 0m09.53s || -0m07.90s 0m00.87s | Util/NumTheoryUtil | 0m07.61s || -0m06.74s 0m01.61s | Encoding/PointEncodingPre | 0m06.93s || -0m05.31s 0m51.95s | Specific/GF25519 | 0m47.52s || +0m04.42s 0m12.30s | Experiments/SpecEd25519 | 0m11.29s || +0m01.01s 0m09.22s | Specific/GF1305 | 0m08.17s || +0m01.05s 0m03.48s | CompleteEdwardsCurve/Pre | 0m04.77s || -0m01.28s 0m02.70s | Assembly/State | 0m04.09s || -0m01.38s 0m01.55s | ModularArithmetic/ModularArithmeticTheorems | 0m02.93s || -0m01.38s 0m01.16s | Assembly/Pseudize | 0m02.34s || -0m01.17s 0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s 0m06.02s | Algebra | 0m06.67s || -0m00.65s 0m05.90s | Experiments/GenericFieldPow | 0m06.68s || -0m00.77s 0m04.65s | WeierstrassCurve/Pre | 0m05.27s || -0m00.61s 0m03.93s | ModularArithmetic/Pow2BaseProofs | 0m03.94s || -0m00.00s 0m03.70s | ModularArithmetic/Tutorial | 0m03.85s || -0m00.14s 0m02.83s | ModularArithmetic/ModularBaseSystemOpt | 0m02.84s || -0m00.00s 0m02.74s | Experiments/EdDSARefinement | 0m01.80s || +0m00.94s 0m02.35s | Util/ZUtil | 0m02.51s || -0m00.15s 0m01.86s | Assembly/Wordize | 0m02.32s || -0m00.45s 0m01.23s | ModularArithmetic/ExtendedBaseVector | 0m01.20s || +0m00.03s 0m01.21s | BaseSystem | 0m01.63s || -0m00.41s 0m01.03s | Experiments/SpecificCurve25519 | 0m00.98s || +0m00.05s 0m01.01s | ModularArithmetic/ModularBaseSystemProofs | 0m01.11s || -0m00.10s 0m00.95s | ModularArithmetic/BarrettReduction/Z | 0m01.38s || -0m00.42s 0m00.92s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.81s || -0m00.89s 0m00.85s | ModularArithmetic/ModularBaseSystemField | 0m00.86s || -0m00.01s 0m00.82s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.79s || +0m00.02s 0m00.80s | Assembly/QhasmEvalCommon | 0m00.93s || -0m00.13s 0m00.73s | Spec/EdDSA | 0m00.59s || +0m00.14s 0m00.72s | Util/Tuple | 0m00.71s || +0m00.01s 0m00.70s | Util/IterAssocOp | 0m00.72s || -0m00.02s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.71s || -0m00.03s 0m00.66s | Assembly/Pipeline | 0m00.64s || +0m00.02s 0m00.65s | Testbit | 0m00.65s || +0m00.00s 0m00.65s | Assembly/PseudoConversion | 0m00.65s || +0m00.00s 0m00.64s | Util/AdditionChainExponentiation | 0m00.63s || +0m00.01s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || -0m00.01s 0m00.63s | Assembly/Pseudo | 0m00.65s || -0m00.02s 0m00.62s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.05s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.57s || +0m00.04s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.69s || -0m00.08s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.59s || +0m00.01s 0m00.56s | Assembly/StringConversion | 0m00.56s || +0m00.00s 0m00.54s | Spec/ModularWordEncoding | 0m00.61s || -0m00.06s 0m00.54s | Assembly/QhasmUtil | 0m00.46s || +0m00.08s 0m00.52s | Assembly/Qhasm | 0m00.53s || -0m00.01s 0m00.48s | Assembly/AlmostQhasm | 0m00.52s || -0m00.04s 0m00.48s | ModularArithmetic/Pre | 0m00.48s || +0m00.00s 0m00.46s | Assembly/Vectorize | 0m00.72s || -0m00.25s 0m00.45s | Spec/WeierstrassCurve | 0m00.44s || +0m00.01s 0m00.44s | Assembly/AlmostConversion | 0m00.44s || +0m00.00s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.51s || -0m00.08s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.03s 0m00.41s | Spec/CompleteEdwardsCurve | 0m00.43s || -0m00.02s 0m00.34s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s 0m00.03s | Util/FixCoqMistakes | N/A || +0m00.03s 0m00.02s | Util/Notations | 0m00.04s || -0m00.02s 0m00.02s | Util/Tactics | 0m00.02s || +0m00.00s
* re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵Gravatar jadep2016-07-21
| | | | organization of reasoning.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 14:17:04 +0000