Prove simple bounded add associativity

5 files changed, 88 insertions, 10 deletions

diff --git a/.gitignore b/.gitignore
index 35f903a..0a123ab 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,6 +4,8 @@
 *.vo
 *.vos
 *.vok
+*.aux
+*.glob
 *.cache
 
 .direnv/
diff --git a/src/.BitEQ.aux b/src/.BitEQ.aux
deleted file mode 100644
index b85cf5b..0000000
--- a/src/.BitEQ.aux
+++ /dev/null
@@ -1,2 +0,0 @@
-COQAUX1 0c779ed0297eab017740eaf15e9ad89b /home/ymherklotz/projects/biteq/src/BitEQ.v
-0 0 vo_compile_time "0.140"
diff --git a/src/BitEQ.glob b/src/BitEQ.glob
deleted file mode 100644
index 5adc945..0000000
--- a/src/BitEQ.glob
+++ /dev/null
@@ -1,3 +0,0 @@
-DIGEST 0c779ed0297eab017740eaf15e9ad89b
-Fbiteq.BitEQ
-R15:22 bbv.Word <> <> lib
diff --git a/src/BitEQ.v b/src/BitEQ.v
index 4093a79..35d08aa 100644
--- a/src/BitEQ.v
+++ b/src/BitEQ.v
@@ -1,12 +1,54 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
+Require Import Coq.micromega.Psatz.
 Require Import Coq.Bool.Bool.
 
+Require Import biteq.Lib.
+
 Require Import bbv.Word.
-Import Notations.
 
-#[local] Open Scope nat_scope.
-#[local] Open Scope word_scope.
+#[local] Open Scope Z_scope.
+
+Record bv := Zbv { size: N; val: Z; }.
+
+Definition bvZ (b: bv) := (val b) mod (2 ^ (Z.of_N (size b))).
+
+Definition bvadd (sz: N) (a b: bv) :=
+  Zbv sz (bvZ a + bvZ b).
+
+Compute bvZ (bvadd 4%N (Zbv 3%N 5) (Zbv 3%N 5)).
+
+Lemma pow_2_div : forall p q, 0 <= p <= q -> (2 ^ p | 2 ^ q).
+Proof.
+  intros.
+  exploit Z.le_exists_sub.
+  assert (p <= q) by lia. apply H0.
+  intros. inversion H0. inversion H1. rewrite H2.
+  rewrite Z.pow_add_r; try lia.
+  apply Z.divide_mul_r. apply Z.divide_refl.
+Qed.
+
+Lemma mod_mod_pow_2 :
+  forall a p q,
+    0 <= p <= q -> (a mod 2 ^ q) mod (2 ^ p) = a mod (2 ^ p).
+Proof.
+  intros. rewrite <- Znumtheory.Zmod_div_mod; try lia. now apply pow_2_div.
+Qed.
 
-Definition wucast {sz: nat} (sz': nat) (w: word sz) : word sz' :=
-  ZToWord _ (uwordToZ w).
+Lemma bounded_add_assoc :
+  forall (p q r s v u: N) (a b c: Z),
+    (v <= q)%N -> (v <= u)%N ->
+    bvZ (bvadd v (bvadd u (Zbv p a) (Zbv r b)) (Zbv s c))
+    = bvZ (bvadd v (Zbv p a) (bvadd q (Zbv r b) (Zbv s c))).
+Proof.
+  intros.
+  (* Zplus_mod *)
+  unfold bvadd, bvZ; simpl in *.
+  rewrite Zplus_mod by eauto. rewrite mod_mod_pow_2 by lia. symmetry.
+  rewrite Zplus_mod by eauto.
+  replace (((b mod 2 ^ Z.of_N r + c mod 2 ^ Z.of_N s) mod 2 ^ Z.of_N q) mod 2 ^ Z.of_N v)
+    with ((b mod 2 ^ Z.of_N r + c mod 2 ^ Z.of_N s) mod 2 ^ Z.of_N v)
+    by (symmetry; apply mod_mod_pow_2; lia).
+  rewrite <- Zplus_mod. symmetry.
+  rewrite <- Zplus_mod. now rewrite Z.add_assoc.
+Qed.
diff --git a/src/Lib.v b/src/Lib.v
new file mode 100644
index 0000000..3e955c8
--- /dev/null
+++ b/src/Lib.v
@@ -0,0 +1,39 @@
+Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.
+Proof. auto. Qed.
+
+Ltac exploit x :=
+    refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _ _) _)
+ || refine (modusponens _ _ (x _ _ _) _)
+ || refine (modusponens _ _ (x _ _) _)
+ || refine (modusponens _ _ (x _) _).