Add some bounded decode/and things

2 files changed, 14 insertions, 0 deletions

diff --git a/src/BoundedArithmetic/Double/Core.v b/src/BoundedArithmetic/Double/Core.v
index aa87e756e..011c610ec 100644
--- a/src/BoundedArithmetic/Double/Core.v
+++ b/src/BoundedArithmetic/Double/Core.v
@@ -95,6 +95,17 @@ Section tuple2.
       := { or := bitwise_or_double }.
   End bitwise_or.
 
+  Section bitwise_and.
+    Context {W}
+            {and : bitwise_and W}.
+
+    Definition bitwise_and_double (x : tuple W 2) (y : tuple W 2) : tuple W 2
+      := (and (fst x) (fst y), and (snd x) (snd y)).
+
+    Global Instance and_double : bitwise_and (tuple W 2)
+      := { and := bitwise_and_double }.
+  End bitwise_and.
+
   Section spread_left.
     Context (n : Z) {W}
             {ldi : load_immediate W}
diff --git a/src/BoundedArithmetic/InterfaceProofs.v b/src/BoundedArithmetic/InterfaceProofs.v
index 8256fc23f..25cd09e85 100644
--- a/src/BoundedArithmetic/InterfaceProofs.v
+++ b/src/BoundedArithmetic/InterfaceProofs.v
@@ -12,6 +12,9 @@ Local Open Scope Z_scope.
 Import BoundedRewriteNotations.
 Local Notation bit b := (if b then 1 else 0).
 
+Lemma decoder_eta {n W} (decode : decoder n W) : decode = {| Interface.decode := decode |}.
+Proof. destruct decode; reflexivity. Defined.
+
 Section InstructionGallery.
   Context (n : Z) (* bit-width of width of [W] *)
           {W : Type} (* bounded type, [W] for word *)