Module-based reorganization of Qhasm code

1 files changed, 44 insertions, 0 deletions

diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
new file mode 100644
index 000000000..0528d0738
--- /dev/null
+++ b/src/Assembly/QhasmUtil.v
@@ -0,0 +1,44 @@
+
+Require Import ZArith NArith NPeano.
+Require Export Bedrock.Word.
+
+Definition Label := nat.
+Definition Index (limit: nat) := {x: nat | (x < limit)%nat}.
+Definition Invert := bool.
+
+Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
+Coercion indexToNat : Index >-> nat.
+
+(* Magical Bitwise Manipulations *)
+
+(* Force w to be m bits long, by truncation or zero-extension *)
+Definition trunc {n} (m: nat) (w: word n): word m.
+  destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
+
+  - replace m with (n + (m - n)) by abstract intuition.
+    refine (zext w (m - n)).
+
+  - rewrite <- s; assumption.
+
+  - replace n with (m + (n - m)) in w by abstract intuition.
+    refine (split1 m (n-m) w).
+Defined.
+
+(* Get the index-th m-bit block of w *)
+Definition getIndex {n} (w: word n) (m index: nat): word m.
+  replace n with
+    ((min n (m * index)) + (n - (min n (m * index))))%nat
+    in w by abstract (
+      assert ((min n (m * index)) <= n)%nat
+        by apply Nat.le_min_l;
+      intuition).
+
+  refine
+    (trunc m
+      (split2 (min n (m * index)) (n - min n (m * index)) w)).
+Defined.
+
+(* set the index-th m-bit block of w to s *)
+Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n :=
+  w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat))))
+    ^| (trunc n (combine s (wzero (index * m)%nat))).