Make Assembly modules 8.5-compatible

8 files changed, 98 insertions, 63 deletions

diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 58215cdf2..ba76f3585 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -25,4 +25,6 @@ Module PipelineExample.
   Program Definition asdf: Program Unary32 := ($0 :+: $0)%p.
 
   Definition exStr := Pipeline.toString asdf.
+
+  (* Eval vm_compute in exStr. *)
 End PipelineExample.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index 48e642151..5d0b2afa4 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -1,6 +1,6 @@
-Require Import QhasmUtil QhasmCommon QhasmEvalCommon QhasmUtil State.
-Require Import Language.
-Require Import List Compare_dec.
+Require Import QhasmCommon QhasmUtil State.
+Require Import Language QhasmEvalCommon.
+Require Import List Compare_dec PeanoNat Omega.
 
 Module Pseudo <: Language.
   Import EvalUtil ListState.
@@ -117,8 +117,8 @@ Module Pseudo <: Language.
     intros; destruct (le_dec n 0).
 
     - exists 0; abstract intuition.
-    - exists (x mod n); abstract (
-        pose proof (mod_bound_pos x n); omega).
+    - exists (x mod n)%nat; abstract (
+        pose proof (Nat.mod_bound_pos x n); omega).
   Defined.
 
   Notation "% A" := (PVar _ (Some false) (indexize A))
@@ -133,19 +133,19 @@ Module Pseudo <: Language.
   Notation "# A" := (PConst _ (natToWord _ A))
     (at level 20, right associativity) : pseudo_notations.
 
-  Notation "A :+: B" := (PBin _ Add (PComb _ _ _ A B))
+  Notation "A :+: B" := (PBin _ IAdd (PComb _ _ _ A B))
     (at level 60, right associativity) : pseudo_notations.
 
   Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B))
     (at level 60, right associativity) : pseudo_notations.
 
-  Notation "A :-: B" := (PBin _ Sub (PComb _ _ _ A B))
+  Notation "A :-: B" := (PBin _ ISub (PComb _ _ _ A B))
     (at level 60, right associativity) : pseudo_notations.
 
-  Notation "A :&: B" := (PBin _ And (PComb _ _ _ A B))
+  Notation "A :&: B" := (PBin _ IAnd (PComb _ _ _ A B))
     (at level 45, right associativity) : pseudo_notations.
 
-  Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B))
+  Notation "A :^: B" := (PBin _ IXor (PComb _ _ _ A B))
     (at level 45, right associativity) : pseudo_notations.
 
   Notation "A :>>: B" := (PShift _ Shr (indexize B) A)
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 35f8e1e30..9c3fda2a0 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -174,7 +174,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
             Some (ASeq
             (AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
             (AWhile (CConst _ TLt (reg' a) (const' (natToWord _ e)))
-                (ASeq fp (AOp (IOpConst Add (reg' a) (const' (natToWord _ 1)))))),
+                (ASeq fp (AOp (IOpConst IAdd (reg' a) (const' (natToWord _ 1)))))),
             fr, madd a rM M', F')
 
         | _ => None
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index ccec401d2..908d16037 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -57,9 +57,11 @@ Inductive Assignment : Type :=
 (* Operations *)
 
 Inductive IntOp :=
-  | Add: IntOp  | Sub: IntOp
-  | Xor: IntOp  | And: IntOp
-  | Or: IntOp.
+  | IAdd: IntOp
+  | ISub: IntOp
+  | IXor: IntOp
+  | IAnd: IntOp
+  | IOr: IntOp.
 
 Inductive CarryOp := | AddWithCarry: CarryOp.
 
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index dbd46b1b4..4c64d8681 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -19,9 +19,13 @@ Module EvalUtil.
     | TGe => orb (eqBit) (gtBit)
     end.
 
-  Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool :=
-    match io with
-    | Add =>
+  Definition evalIntOp {b} (io: IntOp) (x y: word b) :=
+    match io return (word b) * option bool with
+    | ISub => (wminus x y, None)
+    | IXor => (wxor x y, None)
+    | IAnd => (wand x y, None)
+    | IOr => (wor x y, None)
+    | IAdd =>
       let v := (wordToN x + wordToN y)%N in
       let c := (overflows b (&x + &y)%N)%w in
 
@@ -29,11 +33,6 @@ Module EvalUtil.
       | right _ => fun _ => (NToWord b v, Some false)
       | left _ => fun _ => (NToWord b v, Some true)
       end eq_refl
-
-    | Sub => (wminus x y, None)
-    | Xor => (wxor x y, None)
-    | And => (wand x y, None)
-    | Or => (wor x y, None)
     end.
 
   Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool :=
@@ -125,22 +124,54 @@ Module EvalUtil.
         then left _ else right _ else right _ else right _
 
     | _ => fun _ => right _
-    end (eq_refl (a, b))); abstract (
-      inversion_clear _H;
+    end (eq_refl (a, b))); 
+      try destruct v, v'; subst;
       unfold regName, stackName, constValueN, memName, memLength in *;
-      intuition; try inversion H;
-      destruct v, v'; subst;
-      try assert (w = w0) by (apply width_eq); do 3 first [
-          contradict _H0; inversion H1
-        | rewrite <- (natToWord_wordToNat w0);
-          rewrite <- (natToWord_wordToNat w2);
-          assert (w = w1) by (apply width_eq); subst;
-          rewrite _H0
-        | apply (inj_pair2_eq_dec _ Nat.eq_dec) in H3
-        | inversion H; subst; intuition
-        | destruct i, i'; simpl in _H2; subst;
-          replace l with l0 by apply proof_irrelevance
-        | intuition ]).
+      repeat progress (try apply f_equal; subst; match goal with
+        (* Makeshift intuition *)
+      | [ |- ?x = ?x ] => reflexivity
+      | [ H: ?x <> ?x |- _ ] => destruct H
+      | [ |- ?x = ?y ] => apply proof_irrelevance
+
+        (* Destruct the widths *)
+      | [ w0: Width ?x, w1: Width ?x |- _ ] =>
+        let H := fresh in
+        assert (w0 = w1) as H by (apply width_eq);
+          rewrite H in *;
+          clear w0 H
+
+        (* Invert <> *)
+      | [ |- regM _ _ <> _ ] => let H := fresh in (intro H; inversion H)
+      | [ |- memM _ _ _ <> _ ] => let H := fresh in (intro H; inversion H)
+      | [ |- stackM _ _ <> _ ] => let H := fresh in (intro H; inversion H)
+      | [ |- constM _ _ <> _ ] => let H := fresh in (intro H; inversion H)
+
+        (* Invert common structures *)
+      | [ H: regName _ = regName _ |- _ ] => inversion_clear H
+      | [ H: (_, _) = _ |- _ ] => inversion_clear H
+      | [ H: ?x = _ |- _ ] => is_var x; rewrite H in *; clear H
+
+        (* Destruct sigmas, exist, existT *)
+      | [ H: proj1_sig ?a = proj1_sig ?b |- _ ] =>
+        let l0 := fresh in let l1 := fresh in
+        destruct a, b; simpl in H; subst
+      | [ H: proj1_sig ?a <> proj1_sig ?b |- _ ] =>
+        let l0 := fresh in let l1 := fresh in
+        destruct a, b; simpl in H; subst
+      | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => 
+        apply (inj_pair2_eq_dec _ Nat.eq_dec) in H;
+            subst; intuition
+      | [ H: exist _ _ _ = exist _ _ _ |- _ ] => 
+        inversion H; subst; intuition
+
+        (* Single specialized wordToNat proof *)
+      | [ H: wordToNat ?a = wordToNat ?b |- ?a = ?b] =>
+        rewrite <- (natToWord_wordToNat a);
+        rewrite <- (natToWord_wordToNat b);
+        rewrite H; reflexivity
+
+      | _ => idtac
+      end).
   Defined.
 
   Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}.
@@ -148,9 +179,9 @@ Module EvalUtil.
       by abstract (destruct (a <? b)%nat; intuition);
       destruct H.
 
-    - left; abstract (apply Nat.ltb_lt in e; intuition).
+    - left; abstract (apply Nat.ltb_lt; intuition).
 
-    - right; abstract (rewrite Nat.ltb_lt in n; intuition).
+    - right; abstract (rewrite Nat.ltb_lt in *; intuition).
   Defined.
 
   Fixpoint stackNames {n} (lst: list (Mapping n)): list nat :=
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index f49d48573..1c5c6b807 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -48,7 +48,7 @@ Section Util.
       | _ => fun _ => left _
       end eq_refl); abstract (
         unfold c in *; unfold N.lt, N.ge;
-        rewrite _H in *; intuition; try inversion H).
+        rewrite e in *; intuition; try inversion H).
   Defined.
 
   Definition break {n} (m: nat) (x: word n): word m * word (n - m).
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 20bb532ad..8602c7f96 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -4,7 +4,7 @@ Require Export Bedrock.Word.
 Require Import ZArith NArith NPeano Ndec.
 Require Import Compare_dec Omega.
 Require Import OrderedType Coq.Structures.OrderedTypeEx.
-Require Import FMapAVL FMapList JMeq.
+Require Import FMapPositive FMapFullAVL JMeq.
 
 Require Import QhasmUtil QhasmCommon.
 
@@ -127,22 +127,22 @@ Module Triple_as_OT <: UsualOrderedType.
       inversion H0; subst; omega.
   Qed.
 
-  Definition compare x y : Compare lt eq x y.
-    destruct (Nat_as_OT.compare (get0 x) (get0 y)).
+  Ltac compare_tmp x y :=
+    abstract (
+      unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *;
+      destruct (Nat.eq_dec (get0 x) (get0 y));
+      destruct (Nat.eq_dec (get1 x) (get1 y));
+      simpl; intuition).
 
-    Ltac compare_tmp x y :=
-      abstract (
-        unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *;
-        destruct (Nat.eq_dec (get0 x) (get0 y));
-        destruct (Nat.eq_dec (get1 x) (get1 y));
-        simpl; intuition).
+  Ltac compare_eq x y :=
+    abstract (
+      unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq, get0, get1 in *;
+      destruct x as [x x2], y as [y y2];
+      destruct x as [x0 x1], y as [y0 y1];
+      simpl in *; subst; intuition).
 
-    Ltac compare_eq x y :=
-      abstract (
-        unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq, get0, get1 in *;
-        destruct x as [x x2], y as [y y2];
-        destruct x as [x0 x1], y as [y0 y1];
-        simpl in *; subst; intuition).
+  Definition compare x y : Compare lt eq x y.
+    destruct (Nat_as_OT.compare (get0 x) (get0 y)).
 
     - apply LT; compare_tmp x y.
     - destruct (Nat_as_OT.compare (get1 x) (get1 y)).
@@ -177,9 +177,9 @@ End Triple_as_OT.
 Module StateCommon.
   Export ListNotations.
 
-  Module NatM := FMapAVL.Make(Nat_as_OT).
-  Module PairM := FMapAVL.Make(Pair_as_OT).
-  Module TripleM := FMapAVL.Make(Triple_as_OT).
+  Module NatM := FMapFullAVL.Make(Nat_as_OT).
+  Module PairM := FMapFullAVL.Make(Pair_as_OT).
+  Module TripleM := FMapFullAVL.Make(Triple_as_OT).
 
   Definition NatNMap: Type := NatM.t N.
   Definition PairNMap: Type := PairM.t N.
@@ -326,4 +326,4 @@ Module FullState.
     | Some c' => setCarry c' state
     | _ => state
     end.
-End FullState.
\ No newline at end of file
+End FullState.
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index c365c5824..66a83cfa3 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -103,11 +103,11 @@ Module StringConversion <: Conversion Qhasm QhasmString.
 
     Coercion intOpToString (b: IntOp): string :=
       match b with
-      | Add => "+"
-      | Sub => "-"
-      | Xor => "^"
-      | And => "&"
-      | Or => "|"
+      | IAdd => "+"
+      | ISub => "-"
+      | IXor => "^"
+      | IAnd => "&"
+      | IOr => "|"
       end.
 
     Coercion dualOpToString (b: DualOp): string :=