| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This closes #209.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
The new parameterized definitions and proofs are in
WordByWord/Abstract/Dependent/*; the old ones are untouched (and unused)
in WordByWord/Abstract/*. I replaced definitions I didn't know how to
write in the Saturated API with the use of an axiom.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964
and
https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747
Revert "update ocq2C sed script"
This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e.
Revert "make display"
This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e.
Revert "Make use of CArrayNotations"
This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb.
Revert "Fix CArrayNotations"
This reverts commit d0d0fbd4499296a2164e209466227892671556f0.
Revert "Revert "Revert "Add CArrayNotations"""
This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c.
|
|
|
|
| |
This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90.
|
|
|
|
|
|
|
| |
This reverts commit 44359b29d99ab52154dcfdf2b2b16bca7dbaf339.
It triggers [bug #5469](https://coq.inria.fr/bugs/show_bug.cgi?id=5469),
which is present in 8.6, but not v8.6 (nor 8.6.1, once it comes out).
|
|
|
| |
This closes #182.
|
| |
|
|
|
|
|
|
| |
This allows fiat-crypto to continue working with trunk, after the merge
of https://github.com/coq/coq/pull/220. We will remove this when we
migrate to requiring 8.6.1 or 8.7 (neither of which is released yet).
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Now it can handle ops that return (Tbase TZ)
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Currently the refinement is commented out.
Also, we drop the proof of equality early (and probably won't use it in
the first place); there's no way we can carry around such a proof in
reflective-land, so we'll need to add an arithmetical-equality
semi-decider to reflective-land that can prove the relevant equalities
(or we'll need to leave them over as side-conditions). I expeect this
may make things significantly easier on @jadephilipoom.
|
| |
|
| |
|
|
|
|
| |
It's been migrated to Definitions.v and Proofs.v in the same directory
|
| |
|
| |
|
|
|
|
| |
Partial progress with @andres-erbsen
|
| |
|
|
|
|
| |
Written via pair-programming with Andres.
|
|
|
|
|
|
|
|
|
|
|
| |
This closes #171.
It's unfortunately a bit fragile, and takes a really long time (about
60s) to prove correct, because Coq is bad at deep dependent pattern
matching.
We enable a-normal form for the freeze test, because the rewriter only
works when the arguments to adc are var or const.
|
| |
|
| |
|
| |
|