From b68f013b14d7725579f5b680982c2131dee93f79 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 9 Oct 2016 13:44:43 -0400
Subject: Add some bounded decode/and things

---
 src/BoundedArithmetic/Double/Core.v     | 11 +++++++++++
 src/BoundedArithmetic/InterfaceProofs.v |  3 +++
 2 files changed, 14 insertions(+)

(limited to 'src/BoundedArithmetic')

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 *)
-- 
cgit v1.2.3