aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly
Commit message (Collapse)AuthorAge
* Not quite done with WordUtil lemmas.Gravatar Robert Sloan2016-11-08
|\
* | More of jgross admits, less neg and the cmovsGravatar Rob Sloan2016-11-01
| |
| * Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
| | | | | | | | (cc @andres-erbsen)
* | most of jgross' admitsGravatar Rob Sloan2016-10-31
| | | | | | | | '
| * Silence a warningGravatar Jason Gross2016-10-31
| |
| * Significantly faster wordToN, I hopeGravatar Jason Gross2016-10-31
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change -------------------------------------------------------------------------------------- 3m22.43s | Total | 3m22.13s || +0m00.30s -------------------------------------------------------------------------------------- 0m34.51s | Spec/Ed25519 | 0m34.56s || -0m00.05s 0m28.83s | Experiments/Ed25519 | 0m28.60s || +0m00.22s 0m17.28s | EdDSARepChange | 0m17.25s || +0m00.03s 0m08.66s | [require-in-module,deprecated] src/Assembly/GF25519 | 0m08.66s || +0m00.00s 0m08.46s | Encoding/PointEncoding | 0m08.47s || -0m00.00s 0m08.35s | Specific/GF25519BoundedCommonWord | 0m08.44s || -0m00.08s 0m07.74s | Specific/GF25519Reflective | 0m07.69s || +0m00.04s 0m07.59s | Specific/GF25519Reflective/Reified/Mul | 0m07.65s || -0m00.06s 0m07.35s | Specific/GF25519BoundedCommon | 0m07.39s || -0m00.04s 0m06.88s | Specific/GF25519Reflective/Reified/Freeze | 0m06.86s || +0m00.01s 0m05.80s | Bedrock/Word | 0m05.74s || +0m00.05s 0m05.43s | Specific/SC25519 | 0m05.32s || +0m00.10s 0m04.76s | Reflection/Z/Interpretations | 0m04.65s || +0m00.10s 0m04.27s | Encoding/PointEncodingPre | 0m04.31s || -0m00.04s 0m03.72s | Assembly/GF25519BoundedInstantiation | 0m03.68s || +0m00.04s 0m03.21s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.34s || -0m00.12s 0m02.91s | Specific/GF25519Reflective/Reified/CarryOpp | 0m02.86s || +0m00.05s 0m02.84s | Specific/GF25519Reflective/Reified/CarryAdd | 0m02.87s || -0m00.03s 0m02.70s | Assembly/State | 0m02.67s || +0m00.03s 0m02.00s | Specific/GF25519Reflective/Reified/Unpack | 0m01.96s || +0m00.04s 0m01.97s | Specific/GF25519Reflective/Reified/Sub | 0m01.95s || +0m00.02s 0m01.95s | Specific/GF25519Reflective/Reified/Pack | 0m02.03s || -0m00.07s 0m01.81s | Assembly/Evaluables | 0m01.88s || -0m00.06s 0m01.78s | Specific/GF25519Bounded | 0m01.77s || +0m00.01s 0m01.71s | Specific/GF25519Reflective/Reified/Opp | 0m01.68s || +0m00.03s 0m01.66s | Specific/GF25519Reflective/Reified/Add | 0m01.66s || +0m00.00s 0m01.52s | Assembly/Compile | 0m01.48s || +0m00.04s 0m01.49s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.48s || +0m00.01s 0m01.44s | Assembly/WordizeUtil | 0m01.51s || -0m00.07s 0m01.33s | Assembly/Bounds | 0m01.34s || -0m00.01s 0m01.22s | Assembly/Conversions | 0m01.23s || -0m00.01s 0m01.05s | Util/WordUtil | 0m01.03s || +0m00.02s 0m00.94s | Assembly/LL | 0m00.94s || +0m00.00s 0m00.94s | Assembly/Pipeline | 0m00.90s || +0m00.03s 0m00.87s | Assembly/HL | 0m00.89s || -0m00.02s 0m00.81s | Assembly/PhoasCommon | 0m00.77s || +0m00.04s 0m00.79s | Assembly/QhasmEvalCommon | 0m00.83s || -0m00.03s 0m00.75s | Specific/GF25519Reflective/Reified | 0m00.80s || -0m00.05s 0m00.72s | Specific/GF25519Reflective/Common | 0m00.71s || +0m00.01s 0m00.70s | Encoding/ModularWordEncodingTheorems | 0m00.65s || +0m00.04s 0m00.66s | Spec/EdDSA | 0m00.66s || +0m00.00s 0m00.61s | Spec/ModularWordEncoding | 0m00.58s || +0m00.03s 0m00.61s | Encoding/ModularWordEncodingPre | 0m00.67s || -0m00.06s 0m00.51s | Assembly/Qhasm | 0m00.51s || +0m00.00s 0m00.48s | Assembly/StringConversion | 0m00.50s || -0m00.02s 0m00.47s | Assembly/QhasmUtil | 0m00.40s || +0m00.06s 0m00.36s | Assembly/QhasmCommon | 0m00.31s || +0m00.04s
* Disable extraction in src/Assembly/GF25519.vGravatar Jason Gross2016-10-29
| | | | Hopefully this makes the 8.4 build complete in reasonable time again...
* Disable some printingGravatar Jason Gross2016-10-29
|
* Merge branch 'master' into rsloan-phoasGravatar Jason Gross2016-10-27
|\
* | Fixes for Coq 8.4Gravatar Jason Gross2016-10-27
| |
* | Strip function extensionality, enable printing of sub, mul, opp, freezeGravatar Jason Gross2016-10-27
| |
* | Tactics to manually remove Z.to/of_N and suchGravatar Robert Sloan2016-10-26
| |
* | Refactors to remove intermediate conversionsGravatar Robert Sloan2016-10-26
| |
| * 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.
* | Refactors to remove intermediate conversions in HLConversionsGravatar Robert Sloan2016-10-25
| |
* | Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoasGravatar Robert Sloan2016-10-24
|\ \
* | | Use HL conversions for all data types + Pipeline.v refactorsGravatar Robert Sloan2016-10-24
| | |
| | * Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
| | |
| | * Fix for weaker pattern matching in < 8.4pl4Gravatar Jason Gross2016-10-22
| | |
| | * Fix for weaker pattern matching in < 8.4pl4Gravatar Jason Gross2016-10-22
| | |
| * | More Coq 8.4 fixesGravatar Jason Gross2016-10-22
| | |
| * | Fix 8.4 buildGravatar Jason Gross2016-10-22
| | |
| * | cbn does not exist in 8.4Gravatar Jason Gross2016-10-22
| | |
| * | Fix 8.4 buildGravatar Jason Gross2016-10-22
| | |
| * | Fix build failure in 8.6Gravatar Jason Gross2016-10-22
| | |
| * | Merge branch 'master' into pr/84Gravatar Jason Gross2016-10-22
|/| | | |/
| * Unfold interp stuff in Assembly/GF25519BoundedInstantiationGravatar Jason Gross2016-10-22
| |
| * Interpret LetIn to Let_In for better control of interpGravatar Jason Gross2016-10-22
| |
* | Make lower bounds work by using HL conversionsGravatar Robert Sloan2016-10-21
| |
* | merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
|\ \
* \ \ merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
|\ \ \ | | |/ | |/|
* | | committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
| | |
| * | Instantiate some things with bounded thingsGravatar Jason Gross2016-10-21
| | | | | | | | | | | | With help from Rob, and a bit of type golf.
| | * committing unstable refactors to patch masterGravatar Robert Sloan2016-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
| |
| * Adjust bounds in assemblyGravatar Jason Gross2016-10-20
| |
| * Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
| |
| * Various fixes for Coq 8.4Gravatar Jason Gross2016-10-20
| |
| * Use carry versions of operationsGravatar Jason Gross2016-10-20
| |
| * rfreeze, not rinv; update to saner boundedness requirementsGravatar Jason Gross2016-10-20
| |
| * Start instantiating boundedness thingsGravatar Jason Gross2016-10-19
|/
* Fast bounds-checking machinery but lower-bounds are brokenGravatar Robert Sloan2016-10-18
|
* Converting to bounded machineryGravatar Robert Sloan2016-10-17
|
* More of the Conversions.v correctness proofsGravatar Robert Sloan2016-10-14
|
* Use 64-bit limbs in PipelinesGravatar Robert Sloan2016-10-14
|
* Making sub bounds actually tightGravatar Robert Sloan2016-10-14
|
* Moved to non-extended operations + Extraction + Bounds-checkingGravatar Robert Sloan2016-10-14
|
* Well, here's the program instance. The string conversion is still running.Gravatar Robert Sloan2016-10-13
|
* More minor improvements in Conversions.v and Compile.vGravatar Robert Sloan2016-10-13
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 01:19:42 +0000