aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-08-24 19:46:19 -0700
committerGravatar Jason Gross <jagro@google.com>2016-08-24 19:46:19 -0700
commit34d53cc72df1a3c31838e0cc7e06f0cf8959d628 (patch)
tree33d626d40ca904c7c10fb3b2902334a3bf2d74eb /_CoqProject
parent1098b468da5a573f4d4dd5f23546637d0bbff185 (diff)
Rework bounded proofs
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.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 4f8bf08a3..9ed483860 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,6 +27,7 @@ src/BoundedArithmetic/ArchitectureToZLikeProofs.v
src/BoundedArithmetic/DoubleBounded.v
src/BoundedArithmetic/DoubleBoundedProofs.v
src/BoundedArithmetic/Interface.v
+src/BoundedArithmetic/InterfaceProofs.v
src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
src/CompleteEdwardsCurve/ExtendedCoordinates.v
src/CompleteEdwardsCurve/Pre.v