Reorganization of wordize.v

first pseudo conversion lemma

Decent machinery for automatic pseudo-conversion

Decent machinery for automatic pseudo-conversion

Decent machinery for automatic pseudo-conversion

1 files changed, 19 insertions, 20 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 566d7b892..e7e9b0c7d 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,10 +1,8 @@
-Require Export QhasmCommon QhasmUtil State.
-Require Export ZArith Sumbool.
-Require Export Bedrock.Word.
+Require Import QhasmCommon QhasmUtil State.
+Require Import ZArith Sumbool.
+Require Import Bedrock.Word.
 Require Import Logic.Eqdep_dec ProofIrrelevance.
 
-Import Util.
-
 Module EvalUtil.
   Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
     let c := (N.compare (wordToN a) (wordToN b)) in
@@ -25,11 +23,11 @@ Module EvalUtil.
     match io with
     | Add =>
       let v := (wordToN x + wordToN y)%N in
-      let c := (N.compare v (Npow2 b)) in
+      let c := (overflows b (&x + &y)%N)%w in
 
       match c as c' return c' = c -> _ with
-      | Lt => fun _ => (NToWord b v, Some false)
-      | _ => fun _ => (NToWord b v, Some true)
+      | right _ => fun _ => (NToWord b v, Some false)
+      | left _ => fun _ => (NToWord b v, Some true)
       end eq_refl
 
     | Sub => (wminus x y, None)
@@ -41,22 +39,23 @@ Module EvalUtil.
   Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool :=
     match io with
     | AddWidthCarry =>
-      let v := (wordToN x + wordToN y + (if c then 1%N else 0%N))%N in
-      let c := (N.compare v (Npow2 b)) in
+      let c' := (overflows b (&x + &y + (if c then 1 else 0))%N)%w in
+      let v := addWithCarry x y c in
 
-      match c as c' return c' = c -> _ with
-      | Lt => fun _ => (NToWord b v, false)
-      | _ => fun _ => (NToWord b v, true)
+      match c' as c'' return c' = c'' -> _ with
+      | right _ => fun _ => (v, false)
+      | left _ => fun _ => (v, true)
       end eq_refl
     end.
 
-  Definition evalDualOp {b} (duo: DualOp) (x y: word b) :=
-    match duo with
-    | Mult =>
-      let v := (wordToN x * wordToN y)%N in
-      let wres := NToWord (b + b) v in
-      (split1 b b wres, split2 b b wres)
-    end.
+  Definition highBits {n} (m: nat) (x: word n) := snd (break m x).
+
+  Definition evalDualOp {n} (duo: DualOp) (x y: word n): word n * word n.
+    refine match duo with
+    | Mult => (x ^* y,
+        @extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y)))
+    end; abstract omega.
+  Defined.
 
   Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
     match ro with