aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rw-r--r--_CoqProject11
-rw-r--r--src/Assembly/AlmostConversion.v64
-rw-r--r--src/Assembly/AlmostQhasm.v77
-rw-r--r--src/Assembly/BoundedWord.v421
-rw-r--r--src/Assembly/Conversion.v17
-rw-r--r--src/Assembly/Language.v8
-rw-r--r--src/Assembly/MultiBoundedWord.v252
-rw-r--r--src/Assembly/Output.ml14
-rw-r--r--src/Assembly/Pipeline.v28
-rw-r--r--src/Assembly/Pseudize.v217
-rw-r--r--src/Assembly/Pseudo.v182
-rw-r--r--src/Assembly/PseudoConversion.v238
-rw-r--r--src/Assembly/Qhasm.v87
-rw-r--r--src/Assembly/QhasmCommon.v129
-rw-r--r--src/Assembly/QhasmEvalCommon.v267
-rw-r--r--src/Assembly/QhasmUtil.v73
-rw-r--r--src/Assembly/State.v329
-rw-r--r--src/Assembly/StringConversion.v386
-rw-r--r--src/Assembly/Vectorize.v75
-rw-r--r--src/Assembly/Wordize.v507
-rw-r--r--src/Galois/GaloisField.v259
22 files changed, 3642 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 8726df21c..9028c237e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,7 @@
bedrock
fiat
*~
+*#
*.vo
*.d
*.glob
diff --git a/_CoqProject b/_CoqProject
index 9c4cdd3cf..567860b25 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,3 +44,14 @@ src/Util/Tactics.v
src/Util/Tuple.v
src/Util/WordUtil.v
src/Util/ZUtil.v
+src/Assembly/QhasmCommon.v
+src/Assembly/QhasmUtil.v
+src/Assembly/State.v
+src/Assembly/QhasmEvalCommon.v
+src/Assembly/Pseudo.v
+src/Assembly/AlmostQhasm.v
+src/Assembly/Qhasm.v
+src/Assembly/PseudoConversion.v
+src/Assembly/AlmostConversion.v
+src/Assembly/StringConversion.v
+src/Assembly/Pipeline.v
diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v
new file mode 100644
index 000000000..878aa37bf
--- /dev/null
+++ b/src/Assembly/AlmostConversion.v
@@ -0,0 +1,64 @@
+
+Require Import NArith.
+Require Export Qhasm AlmostQhasm Conversion.
+
+Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
+ Import QhasmCommon AlmostQhasm Qhasm.
+ Import ListNotations.
+
+ Fixpoint almostToQhasm' (prog: AlmostProgram) (lblStart: N): list QhasmStatement :=
+ let label0 := (lblStart * 2)%N in
+ let label1 := (label0 + 1)%N in
+
+ match prog with
+ | ASkip => []
+ | ASeq a b => (almostToQhasm' a label0) ++ (almostToQhasm' b label1)
+ | AAssign a => [ QAssign a ]
+ | AOp a => [ QOp a ]
+ | ACond c a b =>
+ let start := N.shiftl 2 label0 in
+ let finish := (start + 1)%N in
+ [QCond c (N.to_nat start)] ++
+ (almostToQhasm' b (start + 2)) ++
+ [QCond CTrue (N.to_nat finish)] ++
+ [QLabel (N.to_nat start)] ++
+ (almostToQhasm' a (start + 3)) ++
+ [QLabel (N.to_nat finish)]
+ | AWhile c a =>
+ let start := N.to_nat (N.shiftl 1 label0) in
+ let test := S start in
+ [ QCond CTrue test ;
+ QLabel start ] ++
+ (almostToQhasm' a label1) ++
+ [ QLabel test;
+ QCond c start ]
+ | ADef lbl f x =>
+ let start' := N.shiftl 1 label0 in
+ let start'' := (1 + start')%N in
+
+ [ QLabel lbl ] ++
+ (almostToQhasm' f start') ++
+ [ QRet ] ++
+ (almostToQhasm' x start'')
+
+ | ACall lbl => [QCall lbl]
+ end.
+
+ Transparent Qhasm.Program AlmostQhasm.Program.
+
+ Definition convertProgram x y (prog: AlmostQhasm.Program x):
+ option (Qhasm.Program y) :=
+ Some (almostToQhasm' prog 0%N).
+
+ Definition convertState x y (st: Qhasm.State y):
+ option (AlmostQhasm.State x) :=
+ Some st.
+
+ Lemma convert_spec: forall pa pb a a' b b' prog prog',
+ convertProgram pa pb prog = Some prog' ->
+ convertState pa pb a = Some a' ->
+ convertState pa pb b = Some b' ->
+ Qhasm.evaluatesTo pb prog' a b <-> AlmostQhasm.evaluatesTo pa prog a' b'.
+ Admitted.
+
+End AlmostConversion.
diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
new file mode 100644
index 000000000..f3ed925c7
--- /dev/null
+++ b/src/Assembly/AlmostQhasm.v
@@ -0,0 +1,77 @@
+Require Import QhasmCommon QhasmEvalCommon.
+Require Import Language.
+Require Import List.
+
+Module AlmostQhasm <: Language.
+ Import QhasmEval.
+
+ (* Program Types *)
+ Definition Params := unit.
+ Definition State := fun (_: Params) => State.
+
+ Inductive AlmostProgram: Set :=
+ | ASkip: AlmostProgram
+ | ASeq: AlmostProgram -> AlmostProgram -> AlmostProgram
+ | AAssign: Assignment -> AlmostProgram
+ | AOp: Operation -> AlmostProgram
+ | ACond: Conditional -> AlmostProgram -> AlmostProgram -> AlmostProgram
+ | AWhile: Conditional -> AlmostProgram -> AlmostProgram
+ | ADef: Label -> AlmostProgram -> AlmostProgram -> AlmostProgram
+ | ACall: Label -> AlmostProgram.
+
+ Hint Constructors AlmostProgram.
+
+ Definition Program := fun (_: Params) => AlmostProgram.
+
+ Fixpoint inline (l: nat) (f prog: AlmostProgram) :=
+ match prog with
+ | ASeq a b => ASeq (inline l f a) (inline l f b)
+ | ACond c a b => ACond c (inline l f a) (inline l f b)
+ | AWhile c a => AWhile c (inline l f a)
+ | ADef l' f' p' =>
+ if (Nat.eq_dec l l')
+ then prog
+ else ADef l' (inline l f f') (inline l f p')
+ | ACall l' =>
+ if (Nat.eq_dec l l')
+ then f
+ else prog
+ | _ => prog
+ end.
+
+ Inductive AlmostEval {x: Params}: Program x -> State x -> State x -> Prop :=
+ | AESkip: forall s, AlmostEval ASkip s s
+ | AESeq: forall p p' s s' s'',
+ AlmostEval p s s'
+ -> AlmostEval p' s' s''
+ -> AlmostEval (ASeq p p') s s''
+ | AEAssign a: forall s s',
+ evalAssignment a s = Some s'
+ -> AlmostEval (AAssign a) s s'
+ | AEOp: forall s s' a,
+ evalOperation a s = Some s'
+ -> AlmostEval (AOp a) s s'
+ | AECondFalse: forall c a b s s',
+ evalCond c s = Some false
+ -> AlmostEval b s s'
+ -> AlmostEval (ACond c a b) s s'
+ | AECondTrue: forall c a b s s',
+ evalCond c s = Some true
+ -> AlmostEval a s s'
+ -> AlmostEval (ACond c a b) s s'
+ | AEWhileRun: forall c a s s' s'',
+ evalCond c s = Some true
+ -> AlmostEval a s s'
+ -> AlmostEval (AWhile c a) s' s''
+ -> AlmostEval (AWhile c a) s s''
+ | AEWhileSkip: forall c a s,
+ evalCond c s = Some false
+ -> AlmostEval (AWhile c a) s s
+ | AEFun: forall l f p s s',
+ AlmostEval (inline l f p) s s'
+ -> AlmostEval (ADef l f p) s s'.
+
+ Definition evaluatesTo := @AlmostEval.
+
+ (* world peace *)
+End AlmostQhasm.
diff --git a/src/Assembly/BoundedWord.v b/src/Assembly/BoundedWord.v
new file mode 100644
index 000000000..3c5684793
--- /dev/null
+++ b/src/Assembly/BoundedWord.v
@@ -0,0 +1,421 @@
+
+Require Import Bedrock.Word Bedrock.Nomega.
+Require Import NArith PArith Ndigits Compare_dec Arith.
+Require Import ProofIrrelevance.
+Require Import Ring.
+Require Import Wordize.
+
+Section BoundedWord.
+
+ Local Open Scope wordize_scope.
+
+ Context {n: nat}.
+
+ (* Word Operations *)
+
+ Definition shiftr (w: word n) (bits: nat): word n.
+ destruct (le_dec bits n).
+
+ - replace n with (bits + (n - bits)) in * by (abstract intuition).
+ refine (zext (split1 bits (n - bits) w) (n - bits)).
+
+ - exact (wzero n).
+ Defined.
+
+ Lemma shiftr_spec: forall (w : word n) (bits: nat),
+ wordToN (shiftr w bits) = N.shiftr (wordToN w) (N.of_nat bits).
+ intros; unfold shiftr; destruct (le_dec bits n).
+
+ - admit.
+
+ - replace (wordToN (wzero n)) with 0%N by admit.
+ unfold N.shiftr.
+ induction bits.
+
+ + replace (N.of_nat 0) with 0%N by intuition.
+ assert (n = 0) by intuition; clear n0; subst.
+ replace w with WO; intuition.
+
+ + induction bits; admit.
+ Qed.
+
+ Definition mask (m: nat) (w: word n): word n.
+ destruct (le_dec m n).
+
+ - replace n with (m + (n - m)) in * by (abstract intuition).
+ refine (w ^& (zext (wones m) (n - m))).
+
+ - exact w.
+ Defined.
+
+ (* Definitions of Inequality and simple bounds. *)
+
+ Lemma le_ge : forall n m, (n <= m -> m >= n)%nat.
+ Proof.
+ intros; omega.
+ Qed.
+
+ Lemma ge_le : forall n m, (n >= m -> m <= n)%nat.
+ Proof.
+ intros; omega.
+ Qed.
+
+ Ltac ge_to_le :=
+ try apply N.ge_le;
+ repeat match goal with
+ | [ H : _ |- _ ] => apply N.le_ge in H
+ end.
+
+ Ltac ge_to_le_nat :=
+ try apply le_ge;
+ repeat match goal with
+ | [ H : _ |- _ ] => apply ge_le in H
+ end.
+
+ Ltac preomega := unfold wordLeN; intros; ge_to_le; pre_nomega.
+
+ Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N.
+
+ Theorem word_size_bound : forall (w: word n),
+ w <= Npow2 n - 1.
+ Proof.
+ intros; unfold wordLeN; rewrite wordToN_nat.
+
+ assert (B := wordToNat_bound w);
+ rewrite <- Npow2_nat in B;
+ apply nat_compare_lt in B.
+
+ unfold N.le; intuition;
+ rewrite N2Nat.inj_compare in H;
+ rewrite Nat2N.id in H.
+
+ apply nat_compare_lt in B.
+ apply nat_compare_gt in H.
+
+ replace (N.to_nat (Npow2 n)) with (S (N.to_nat (Npow2 n - 1))) in * by admit.
+ intuition.
+ Qed.
+
+ Theorem constant_bound_N : forall k,
+ NToWord n k <= k.
+ Proof.
+ preomega.
+ rewrite NToWord_nat.
+ destruct (le_lt_dec (pow2 n) (N.to_nat k)).
+
+ specialize (wordToNat_bound (natToWord n (N.to_nat k))); nomega.
+
+ rewrite wordToNat_natToWord_idempotent; nomega.
+ Qed.
+
+ Theorem constant_bound_nat : forall k,
+ natToWord n k <= N.of_nat k.
+ Proof.
+ preomega.
+ destruct (le_lt_dec (pow2 n) k).
+
+ specialize (wordToNat_bound (natToWord n k)); nomega.
+
+ rewrite wordToNat_natToWord_idempotent; nomega.
+ Qed.
+
+ Lemma let_bound : forall (x: word n) (f: word n -> word n) xb fb, x <= xb
+ -> (forall x', x' <= xb -> f x' <= fb)
+ -> (let k := x in f k) <= fb.
+ eauto.
+ Qed.
+
+ Theorem wplus_bound : forall (w1 w2 : word n) b1 b2,
+ w1 <= b1
+ -> w2 <= b2
+ -> w1 ^+ w2 <= b1 + b2.
+ Proof.
+ preomega.
+ destruct (le_lt_dec (pow2 n) (N.to_nat b1 + N.to_nat b2)).
+
+ specialize (wordToNat_bound (w1 ^+ w2)); nomega.
+
+ rewrite wplus_alt.
+ unfold wplusN, wordBinN.
+ rewrite wordToNat_natToWord_idempotent; nomega.
+ Qed.
+
+ Theorem wmult_bound : forall (w1 w2 : word n) b1 b2,
+ w1 <= b1
+ -> w2 <= b2
+ -> w1 ^* w2 <= b1 * b2.
+ Proof.
+ preomega.
+ destruct (le_lt_dec (pow2 n) (N.to_nat b1 * N.to_nat b2)).
+
+ specialize (wordToNat_bound (w1 ^* w2)); nomega.
+
+ rewrite wmult_alt.
+ unfold wmultN, wordBinN.
+ rewrite wordToNat_natToWord_idempotent.
+ ge_to_le_nat.
+
+ apply Mult.mult_le_compat; nomega.
+ pre_nomega.
+ apply Lt.le_lt_trans with (N.to_nat b1 * N.to_nat b2); auto.
+ apply Mult.mult_le_compat; nomega.
+ Qed.
+
+ Theorem shiftr_bound : forall (w : word n) b bits,
+ w <= b
+ -> shiftr w bits <= N.shiftr b (N.of_nat bits).
+ Proof.
+ admit.
+ Qed.
+
+ Theorem mask_bound : forall (w : word n) m,
+ mask m w <= Npow2 m - 1.
+ Proof.
+ admit.
+ Qed.
+
+ Theorem mask_update_bound : forall (w : word n) b m,
+ w <= b
+ -> mask m w <= (N.min b (Npow2 m - 1)).
+ Proof.
+ admit.
+ Qed.
+
+
+ Ltac word_bound :=
+ repeat (
+ eassumption
+ || apply wplus_bound
+ || apply wmult_bound
+ || apply mask_update_bound
+ || apply mask_bound
+ || apply shiftr_bound
+ || apply constant_bound_N
+ || apply constant_bound_nat
+ || apply word_size_bound
+ ).
+
+ Notation "$" := (natToWord _).
+
+ Lemma example1 : forall (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
+ w1 <= b1
+ -> w2 <= b2
+ -> w3 <= b3
+ -> w4 <= b4
+ -> { b | w1 ^+ (w2 ^* w3) ^* w4 <= b }.
+ Proof.
+ eexists.
+ word_bound.
+ Defined.
+
+ (* Eval simpl in fun (w1 w2 w3 w4 : word n) (b1 b2 b3 b4 : N)
+ (H1 : w1 <= b1) (H2 : w2 <= b2) (H3 : w3 <= b3) (H4 : w4 <= b4) =>
+ projT1 (example1 H1 H2 H3 H4). *)
+
+ Lemma example2 : forall (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
+ w1 <= b1
+ -> w2 <= b2
+ -> w3 <= b3
+ -> w4 <= b4
+ -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }.
+ Proof.
+ eexists.
+ word_bound.
+ Defined.
+
+ (*Eval simpl in fun (w1 w2 w3 w4 : word n) (b1 b2 b3 b4 : N)
+ (H1 : w1 <= b1) (H2 : w2 <= b2) (H3 : w3 <= b3) (H4 : w4 <= b4) =>
+ projT1 (example2 H1 H2 H3 H4). *)
+
+ Lemma example3 : forall (w1 w2 w3 w4 : word n),
+ w1 <= Npow2 3
+ -> w2 <= Npow2 4
+ -> w3 <= Npow2 8
+ -> w4 <= Npow2 16
+ -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }.
+ Proof.
+ eexists.
+ word_bound.
+ Defined.
+
+ (* Eval simpl in fun (w1 w2 w3 w4 : word n)
+ (H1 : w1 <= _) (H2 : w2 <= _) (H3 : w3 <= _) (H4 : w4 <= _) =>
+ projT1 (example3 H1 H2 H3 H4). *)
+
+End BoundedWord.
+
+Section MulmodExamples.
+
+ Notation "A <= B" := (wordLeN A B) (at level 70).
+ Notation "$" := (natToWord _).
+
+ Lemma mask_wand : forall (n: nat) (x: word n) m b,
+ mask (N.to_nat m) x <= b
+ -> x ^& (@NToWord n (N.ones m)) <= b.
+ Proof.
+ Admitted.
+
+ Ltac word_bound_step :=
+ idtac; match goal with
+ | [ H: ?x <= _ |- ?x <= _] => eexact H
+ | [|- (let x := ?y in @?z x) <= ?b ] => refine (@let_bound _ y z _ b _ _); [ | intros ? ? ]
+ | [|- (let x := ?y in (?a <= ?b)) ] => change ((let x := y in a) <= b)
+ | [|- (let x := ?y in (?a <= @?b x)) ] => change ((let x := y in a) <= b y); cbv beta
+ | [|- mask _ _ <= _] => apply mask_bound
+ | [|- _ ^+ _ <= _] => apply wplus_bound
+ | [|- _ ^* _ <= _] => apply wmult_bound
+ | [|- shiftr _ _ <= _] => apply shiftr_bound
+ | [|- $ _ <= _] => apply constant_bound_nat
+ | [|- NToWord _ _ <= _] => apply constant_bound_N
+ | [|- _ <= Npow2 _ - 1] => apply word_size_bound
+ | [|- _ ^& (@NToWord _ (N.ones _)) <= _] => apply mask_wand
+ end.
+
+ Ltac simpl_hyps :=
+ match goal with
+ | [ H: ?x <= _ |- context[?x]] =>
+ unfold Npow, Pos.pow, Npow2, N.shiftr in H;
+ simpl in H
+ | [ H: _ |- _ ] => clear H
+ | _ => idtac
+ end.
+
+ Ltac word_bound := repeat (word_bound_step; simpl_hyps).
+
+ Ltac word_bound_danger :=
+ word_bound; try eassumption; try apply word_size_bound.
+
+ Lemma example_and : forall x : word 32,
+ wand x (NToWord 32 (N.ones 10)) <= 1023.
+ intros.
+ replace (wand x (NToWord 32 (N.ones 10))) with (mask 10 x) by admit.
+ word_bound.
+ Qed.
+
+ Lemma example_shiftr : forall x : word 32, shiftr x 30 <= 3.
+ intros.
+ replace 3%N with (N.shiftr (Npow2 32 - 1) (N.of_nat 30)) by (simpl; intuition).
+ word_bound.
+ Qed.
+
+ Lemma example_shiftr2 : forall x : word 32, x <= 1023 -> shiftr x 5 <= 31.
+ intros.
+ replace 31%N with (N.shiftr 1023%N 5%N) by (simpl; intuition).
+ word_bound.
+ Qed.
+
+ Variable f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : word 32.
+ Variable g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : word 32.
+ Hypothesis Hf0 : f0 <= 2^26.
+ Hypothesis Hf1 : f1 <= 2^25.
+ Hypothesis Hf2 : f2 <= 2^26.
+ Hypothesis Hf3 : f3 <= 2^25.
+ Hypothesis Hf4 : f4 <= 2^26.
+ Hypothesis Hf5 : f5 <= 2^25.
+ Hypothesis Hf6 : f6 <= 2^26.
+ Hypothesis Hf7 : f7 <= 2^25.
+ Hypothesis Hf8 : f8 <= 2^26.
+ Hypothesis Hf9 : f9 <= 2^25.
+ Hypothesis Hg0 : g0 <= 2^26.
+ Hypothesis Hg1 : g1 <= 2^25.
+ Hypothesis Hg2 : g2 <= 2^26.
+ Hypothesis Hg3 : g3 <= 2^25.
+ Hypothesis Hg4 : g4 <= 2^26.
+ Hypothesis Hg5 : g5 <= 2^25.
+ Hypothesis Hg6 : g6 <= 2^26.
+ Hypothesis Hg7 : g7 <= 2^25.
+
+ Hypothesis Hg8 : g8 <= 2^26.
+ Hypothesis Hg9 : g9 <= 2^25.
+
+ Lemma example_mulmod_s_ppt : { b | f0 ^* g0 <= b}.
+ eexists.
+ word_bound.
+ Defined.
+
+ Lemma example_mulmod_s_pp : { b | f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2) <= b}.
+ eexists.
+ word_bound.
+ Defined.
+
+ Lemma example_mulmod_s_pp_shiftr :
+ { b | shiftr (f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) 26 <= b}.
+ eexists.
+ word_bound.
+ Defined.
+
+ Lemma example_mulmod_u_fg1 : { b |
+ (let y : word 32 := (* the type declarations on the let-s make type inference not take forever *)
+ (f0 ^* g0 ^+
+ $19 ^*
+ (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+
+ f1 ^* g9 ^* $2)) in
+ let y0 : word 32 :=
+ (shiftr y 26 ^+
+ (f1 ^* g0 ^+ f0 ^* g1 ^+
+ $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9))) in
+ let y1 : word 32 :=
+ (shiftr y0 25 ^+
+ (f2 ^* g0 ^+ f1 ^* g1 ^* $2 ^+ f0 ^* g2 ^+
+ $19 ^* (f9 ^* g3 ^* $2 ^+ f8 ^* g4 ^+ f7 ^* g5 ^* $2 ^+ f6 ^* g6 ^+ f5 ^* g7 ^* $2 ^+ f4 ^* g8 ^+ f3 ^* g9 ^* $2))) in
+ let y2 : word 32 :=
+ (shiftr y1 26 ^+
+ (f3 ^* g0 ^+ f2 ^* g1 ^+ f1 ^* g2 ^+ f0 ^* g3 ^+
+ $19 ^* (f9 ^* g4 ^+ f8 ^* g5 ^+ f7 ^* g6 ^+ f6 ^* g7 ^+ f5 ^* g8 ^+ f4 ^* g9))) in
+ let y3 : word 32 :=
+ (shiftr y2 25 ^+
+ (f4 ^* g0 ^+ f3 ^* g1 ^* $2 ^+ f2 ^* g2 ^+ f1 ^* g3 ^* $2 ^+ f0 ^* g4 ^+
+ $19 ^* (f9 ^* g5 ^* $2 ^+ f8 ^* g6 ^+ f7 ^* g7 ^* $2 ^+ f6 ^* g8 ^+ f5 ^* g9 ^* $2))) in
+ let y4 : word 32 :=
+ (shiftr y3 26 ^+
+ (f5 ^* g0 ^+ f4 ^* g1 ^+ f3 ^* g2 ^+ f2 ^* g3 ^+ f1 ^* g4 ^+ f0 ^* g5 ^+
+ $19 ^* (f9 ^* g6 ^+ f8 ^* g7 ^+ f7 ^* g8 ^+ f6 ^* g9))) in
+ let y5 : word 32 :=
+ (shiftr y4 25 ^+
+ (f6 ^* g0 ^+ f5 ^* g1 ^* $2 ^+ f4 ^* g2 ^+ f3 ^* g3 ^* $2 ^+ f2 ^* g4 ^+ f1 ^* g5 ^* $2 ^+ f0 ^* g6 ^+
+ $19 ^* (f9 ^* g7 ^* $2 ^+ f8 ^* g8 ^+ f7 ^* g9 ^* $2))) in
+ let y6 : word 32 :=
+ (shiftr y5 26 ^+
+ (f7 ^* g0 ^+ f6 ^* g1 ^+ f5 ^* g2 ^+ f4 ^* g3 ^+ f3 ^* g4 ^+ f2 ^* g5 ^+ f1 ^* g6 ^+ f0 ^* g7 ^+
+ $19 ^* (f9 ^* g8 ^+ f8 ^* g9))) in
+ let y7 : word 32 :=
+ (shiftr y6 25 ^+
+ (f8 ^* g0 ^+ f7 ^* g1 ^* $2 ^+ f6 ^* g2 ^+ f5 ^* g3 ^* $2 ^+ f4 ^* g4 ^+ f3 ^* g5 ^* $2 ^+ f2 ^* g6 ^+ f1 ^* g7 ^* $2 ^+
+ f0 ^* g8 ^+ $19 ^* f9 ^* g9 ^* $2)) in
+ let y8 : word 32 :=
+ (shiftr y7 26 ^+
+ (f9 ^* g0 ^+ f8 ^* g1 ^+ f7 ^* g2 ^+ f6 ^* g3 ^+ f5 ^* g4 ^+ f4 ^* g5 ^+ f3 ^* g6 ^+ f2 ^* g7 ^+ f1 ^* g8 ^+
+ f0 ^* g9)) in
+ let y9 : word 32 :=
+ ($19 ^* shiftr y8 25 ^+
+ wand
+ (f0 ^* g0 ^+
+ $19 ^*
+ (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+
+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) (@NToWord 32 (N.ones 26%N))) in
+ let fg1 : word 32 := (shiftr y9 26 ^+
+ wand
+ (shiftr y 26 ^+
+ (f1 ^* g0 ^+ f0 ^* g1 ^+
+ $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9)))
+ (@NToWord 32 (N.ones 26%N))) in
+ fg1) <= b }.
+ Proof.
+ eexists.
+ (* Time word_bound. *) (* <- It works, but don't do this in the build! *)
+ Abort.
+
+ Require Import ZArith.
+ Variable shiftra : forall {l}, word l -> nat -> word l. (* "arithmetic" aka "signed" bitshift *)
+ Hypothesis shiftra_spec : forall {l} (w : word l) (n:nat), wordToZ (shiftra l w n) = Z.shiftr (wordToZ w) (Z.of_nat n).
+
+ Lemma example_shiftra : forall x : word 4, shiftra 4 x 2 <= 15.
+ Abort.
+
+ Lemma example_shiftra : forall x : word 4, x <= 7 -> shiftra 4 x 2 <= 1.
+ Abort.
+
+ Lemma example_mulmod_s_pp_shiftra :
+ { b | shiftra 32 (f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) 26 <= b}.
+ Abort.
+End MulmodExamples.
diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v
new file mode 100644
index 000000000..239bd6b71
--- /dev/null
+++ b/src/Assembly/Conversion.v
@@ -0,0 +1,17 @@
+
+Require Export Language.
+
+Module Type Conversion (A B: Language).
+
+ Parameter convertProgram: forall (x: A.Params) (y: B.Params),
+ A.Program x -> option (B.Program y).
+ Parameter convertState: forall (x: A.Params) (y: B.Params),
+ B.State y -> option (A.State x).
+
+ Axiom convert_spec: forall pa pb a a' b b' prog prog',
+ convertProgram pa pb prog = Some prog' ->
+ convertState pa pb a = Some a' ->
+ convertState pa pb b = Some b' ->
+ B.evaluatesTo pb prog' a b <-> A.evaluatesTo pa prog a' b'.
+
+End Conversion.
diff --git a/src/Assembly/Language.v b/src/Assembly/Language.v
new file mode 100644
index 000000000..460aff5fe
--- /dev/null
+++ b/src/Assembly/Language.v
@@ -0,0 +1,8 @@
+
+Module Type Language.
+ Parameter Params: Type.
+ Parameter Program: Params -> Type.
+ Parameter State: Params -> Type.
+
+ Parameter evaluatesTo: forall x: Params, Program x -> State x -> State x -> Prop.
+End Language.
diff --git a/src/Assembly/MultiBoundedWord.v b/src/Assembly/MultiBoundedWord.v
new file mode 100644
index 000000000..add2aa1a2
--- /dev/null
+++ b/src/Assembly/MultiBoundedWord.v
@@ -0,0 +1,252 @@
+
+Require Import Bedrock.Word Bedrock.Nomega.
+Require Import NArith PArith Ndigits Compare_dec Arith.
+Require Import ProofIrrelevance Ring.
+Require Import BoundedWord.
+
+Import BoundedWord.
+
+(* Parameters of boundedness calculations *)
+Notation "A <= B" := (wordLeN A B) (at level 70).
+Notation "$" := (natToWord _).
+
+(* Hypothesis-based word-bound tactic *)
+Ltac multi_apply0 A L := pose proof (L A).
+
+Ltac multi_apply1 A L :=
+ match goal with
+ | [ H: A <= ?b |- _] => pose proof (L A b H)
+ end.
+
+Ltac multi_apply2 A B L :=
+ match goal with
+ | [ H1: A <= ?b1, H2: B <= ?b2 |- _] => pose proof (L A B b1 b2 H1 H2)
+ end.
+
+Ltac multi_recurse n T :=
+ match goal with
+ | [ H: T <= _ |- _] => idtac
+ | _ =>
+ is_var T;
+ let T' := (eval cbv delta [T] in T) in multi_recurse n T';
+ match goal with
+ | [ H : T' <= ?x |- _ ] =>
+ pose proof (H : T <= x)
+ end
+
+ | _ =>
+ match T with
+ | ?W1 ^+ ?W2 =>
+ multi_recurse n W1; multi_recurse n W2;
+ multi_apply2 W1 W2 (@wplus_bound n)
+
+ | ?W1 ^* ?W2 =>
+ multi_recurse n W1; multi_recurse n W2;
+ multi_apply2 W1 W2 (@wmult_bound n)
+
+ | mask ?m ?w =>
+ multi_recurse n w;
+ multi_apply1 w (fun b => @mask_update_bound n w b)
+
+ | mask ?m ?w =>
+ multi_recurse n w;
+ pose proof (@mask_bound n w m)
+
+ | ?x ^& (@NToWord _ (N.ones ?m)) =>
+ multi_recurse n (mask (N.to_nat m) x);
+ match goal with
+ | [ H: (mask (N.to_nat m) x) <= ?b |- _] =>
+ pose proof (@mask_wand n x m b H)
+ end
+
+ | shiftr ?w ?bits =>
+ multi_recurse n w;
+ match goal with
+ | [ H: w <= ?b |- _] =>
+ pose proof (@shiftr_bound n w b bits H)
+ end
+
+ | NToWord _ ?k => pose proof (@constant_bound_N n k)
+ | natToWord _ ?k => pose proof (@constant_bound_nat n k)
+ | ($ ?k) => pose proof (@constant_bound_nat n k)
+ | _ => pose proof (@word_size_bound n T)
+ end
+ end.
+
+Lemma unwrap_let: forall {n} (y: word n) (f: word n -> word n) (b: N),
+ (let x := y in f x) <= b <-> let x := y in (f x <= b).
+Proof. intuition. Qed.
+
+Ltac multi_bound n :=
+ match goal with
+ | [|- let A := ?B in _] =>
+ multi_recurse n B; intro; multi_bound n
+ | [|- (let A := _ in _) <= _] =>
+ apply unwrap_let; multi_bound n
+ | [|- ?W <= _ ] =>
+ multi_recurse n W
+ end.
+
+(* Examples *)
+Lemma example1 : forall {n} (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
+ w1 <= b1
+ -> w2 <= b2
+ -> w3 <= b3
+ -> w4 <= b4
+ -> { b | let w5 := w2 ^* w3 in w1 ^+ w5 ^* w4 <= b }.
+Proof.
+ eexists.
+ multi_bound n.
+ eassumption.
+Defined.
+
+Lemma example2 : forall {n} (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
+ w1 <= b1
+ -> w2 <= b2
+ -> w3 <= b3
+ -> w4 <= b4
+ -> { b | (let w5 := (w2 ^* $7 ^* w3) in w1 ^+ w5 ^* w4 ^+ $8 ^+ w2) <= b }.
+Proof.
+ eexists.
+ multi_bound n.
+ eassumption.
+Defined.
+
+Lemma example3 : forall {n} (w1 w2 w3 w4 : word n),
+ w1 <= Npow2 3
+ -> w2 <= Npow2 4
+ -> w3 <= Npow2 8
+ -> w4 <= Npow2 16
+ -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }.
+Proof.
+ eexists.
+ multi_bound n.
+ eassumption.
+Defined.
+
+Section MulmodExamples.
+
+ Notation "A <= B" := (wordLeN A B) (at level 70).
+ Notation "$" := (natToWord 32).
+
+ Lemma example_and : forall x : word 32, wand x (NToWord 32 (N.ones 10)) <= 1023.
+ intros.
+ replace (wand x (NToWord 32 (N.ones 10))) with (mask 10 x) by admit.
+ multi_bound 32; eassumption.
+ Qed.
+
+ Lemma example_shiftr : forall x : word 32, shiftr x 30 <= 3.
+ intros.
+ replace 3%N with (N.shiftr (Npow2 32 - 1) (N.of_nat 30)) by (simpl; intuition).
+ multi_bound 32; eassumption.
+ Qed.
+
+ Lemma example_shiftr2 : forall x : word 32, x <= 1023 -> shiftr x 5 <= 31.
+ intros.
+ replace 31%N with (N.shiftr 1023%N 5%N) by (simpl; intuition).
+ multi_bound 32; eassumption.
+ Qed.
+
+ Variable f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : word 32.
+ Variable g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : word 32.
+ Hypothesis Hf0 : f0 <= 2^26.
+ Hypothesis Hf1 : f1 <= 2^25.
+ Hypothesis Hf2 : f2 <= 2^26.
+ Hypothesis Hf3 : f3 <= 2^25.
+ Hypothesis Hf4 : f4 <= 2^26.
+ Hypothesis Hf5 : f5 <= 2^25.
+ Hypothesis Hf6 : f6 <= 2^26.
+ Hypothesis Hf7 : f7 <= 2^25.
+ Hypothesis Hf8 : f8 <= 2^26.
+ Hypothesis Hf9 : f9 <= 2^25.
+ Hypothesis Hg0 : g0 <= 2^26.
+ Hypothesis Hg1 : g1 <= 2^25.
+ Hypothesis Hg2 : g2 <= 2^26.
+ Hypothesis Hg3 : g3 <= 2^25.
+ Hypothesis Hg4 : g4 <= 2^26.
+ Hypothesis Hg5 : g5 <= 2^25.
+ Hypothesis Hg6 : g6 <= 2^26.
+ Hypothesis Hg7 : g7 <= 2^25.
+ Hypothesis Hg8 : g8 <= 2^26.
+ Hypothesis Hg9 : g9 <= 2^25.
+
+ Lemma example_mulmod_s_ppt : { b | f0 ^* g0 <= b}.
+ eexists.
+ multi_bound 32; eassumption.
+ Defined.
+
+ Lemma example_mulmod_s_pp : { b | f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2) <= b}.
+ eexists.
+ multi_bound 32; eassumption.
+ Defined.
+
+ Lemma example_mulmod_s_pp_shiftr :
+ { b | shiftr (f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) 26 <= b}.
+ eexists.
+ multi_bound 32; eassumption.
+ Defined.
+
+ Lemma example_mulmod_u_fg1 : { b |
+ (let y : word 32 :=
+ (f0 ^* g0 ^+
+ $19 ^*
+ (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+
+ f1 ^* g9 ^* $2)) in
+ let y0 : word 32 :=
+ (shiftr y 26 ^+
+ (f1 ^* g0 ^+ f0 ^* g1 ^+
+ $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9))) in
+ let y1 : word 32 :=
+ (shiftr y0 25 ^+
+ (f2 ^* g0 ^+ f1 ^* g1 ^* $2 ^+ f0 ^* g2 ^+
+ $19 ^* (f9 ^* g3 ^* $2 ^+ f8 ^* g4 ^+ f7 ^* g5 ^* $2 ^+ f6 ^* g6 ^+ f5 ^* g7 ^* $2 ^+ f4 ^* g8 ^+ f3 ^* g9 ^* $2))) in
+ let y2 : word 32 :=
+ (shiftr y1 26 ^+
+ (f3 ^* g0 ^+ f2 ^* g1 ^+ f1 ^* g2 ^+ f0 ^* g3 ^+
+ $19 ^* (f9 ^* g4 ^+ f8 ^* g5 ^+ f7 ^* g6 ^+ f6 ^* g7 ^+ f5 ^* g8 ^+ f4 ^* g9))) in
+ let y3 : word 32 :=
+ (shiftr y2 25 ^+
+ (f4 ^* g0 ^+ f3 ^* g1 ^* $2 ^+ f2 ^* g2 ^+ f1 ^* g3 ^* $2 ^+ f0 ^* g4 ^+
+ $19 ^* (f9 ^* g5 ^* $2 ^+ f8 ^* g6 ^+ f7 ^* g7 ^* $2 ^+ f6 ^* g8 ^+ f5 ^* g9 ^* $2))) in
+ let y4 : word 32 :=
+ (shiftr y3 26 ^+
+ (f5 ^* g0 ^+ f4 ^* g1 ^+ f3 ^* g2 ^+ f2 ^* g3 ^+ f1 ^* g4 ^+ f0 ^* g5 ^+
+ $19 ^* (f9 ^* g6 ^+ f8 ^* g7 ^+ f7 ^* g8 ^+ f6 ^* g9))) in
+ let y5 : word 32 :=
+ (shiftr y4 25 ^+
+ (f6 ^* g0 ^+ f5 ^* g1 ^* $2 ^+ f4 ^* g2 ^+ f3 ^* g3 ^* $2 ^+ f2 ^* g4 ^+ f1 ^* g5 ^* $2 ^+ f0 ^* g6 ^+
+ $19 ^* (f9 ^* g7 ^* $2 ^+ f8 ^* g8 ^+ f7 ^* g9 ^* $2))) in
+ let y6 : word 32 :=
+ (shiftr y5 26 ^+
+ (f7 ^* g0 ^+ f6 ^* g1 ^+ f5 ^* g2 ^+ f4 ^* g3 ^+ f3 ^* g4 ^+ f2 ^* g5 ^+ f1 ^* g6 ^+ f0 ^* g7 ^+
+ $19 ^* (f9 ^* g8 ^+ f8 ^* g9))) in
+ let y7 : word 32 :=
+ (shiftr y6 25 ^+
+ (f8 ^* g0 ^+ f7 ^* g1 ^* $2 ^+ f6 ^* g2 ^+ f5 ^* g3 ^* $2 ^+ f4 ^* g4 ^+ f3 ^* g5 ^* $2 ^+ f2 ^* g6 ^+ f1 ^* g7 ^* $2 ^+
+ f0 ^* g8 ^+ $19 ^* f9 ^* g9 ^* $2)) in
+ let y8 : word 32 :=
+ (shiftr y7 26 ^+
+ (f9 ^* g0 ^+ f8 ^* g1 ^+ f7 ^* g2 ^+ f6 ^* g3 ^+ f5 ^* g4 ^+ f4 ^* g5 ^+ f3 ^* g6 ^+ f2 ^* g7 ^+ f1 ^* g8 ^+
+ f0 ^* g9)) in
+ let y9 : word 32 :=
+ ($19 ^* shiftr y8 25 ^+
+ wand
+ (f0 ^* g0 ^+
+ $19 ^*
+ (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+
+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) (@NToWord 32 (N.ones 26%N))) in
+ let fg1 : word 32 := (shiftr y9 26 ^+
+ wand
+ (shiftr y 26 ^+
+ (f1 ^* g0 ^+ f0 ^* g1 ^+
+ $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9)))
+ (@NToWord 32 (N.ones 26%N))) in
+ fg1) <= b }.
+ Proof.
+ eexists; multi_bound 32; eassumption.
+
+ Defined.
+
+ Eval simpl in (proj1_sig example_mulmod_u_fg1).
+
+End MulmodExamples.
diff --git a/src/Assembly/Output.ml b/src/Assembly/Output.ml
new file mode 100644
index 000000000..d84aee0a2
--- /dev/null
+++ b/src/Assembly/Output.ml
@@ -0,0 +1,14 @@
+
+open Result
+
+let list_to_string s =
+ let rec loop s n =
+ match s with
+ [] -> String.make n '?'
+ | car :: cdr ->
+ let result = loop cdr (n + 1) in
+ Bytes.set result n car;
+ result
+ in loop s 0 ;;
+
+print_string (list_to_string result) ;;
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
new file mode 100644
index 000000000..58215cdf2
--- /dev/null
+++ b/src/Assembly/Pipeline.v
@@ -0,0 +1,28 @@
+Require Import QhasmCommon QhasmEvalCommon.
+Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
+Require Import PseudoConversion AlmostConversion StringConversion.
+
+Module Pipeline.
+ Export AlmostQhasm Qhasm QhasmString.
+ Export Pseudo.
+
+ Transparent Pseudo.Program AlmostQhasm.Program Qhasm.Program QhasmString.Program.
+ Transparent Pseudo.Params AlmostQhasm.Params Qhasm.Params QhasmString.Params.
+
+ Definition toAlmost {w s n m} (p: @Pseudo w s n m) : option AlmostProgram :=
+ PseudoConversion.convertProgram (mkParams w s n m) tt p.
+
+ Definition toQhasm {w s n m} (p: @Pseudo w s n m) : option (list QhasmStatement) :=
+ omap (toAlmost p) (AlmostConversion.convertProgram tt tt).
+
+ Definition toString {w s n m} (p: @Pseudo w s n m) : option string :=
+ omap (toQhasm p) (StringConversion.convertProgram tt tt).
+End Pipeline.
+
+Module PipelineExample.
+ Import Pipeline.
+
+ Program Definition asdf: Program Unary32 := ($0 :+: $0)%p.
+
+ Definition exStr := Pipeline.toString asdf.
+End PipelineExample.
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
new file mode 100644
index 000000000..af311963d
--- /dev/null
+++ b/src/Assembly/Pseudize.v
@@ -0,0 +1,217 @@
+Require Export Bedrock.Word Bedrock.Nomega.
+Require Import NArith NPeano List Sumbool Compare_dec.
+Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State.
+Require Export Wordize Vectorize.
+
+Module Conversion.
+ Import Pseudo ListNotations StateCommon EvalUtil ListState.
+
+ Hint Unfold setList getList getVar setCarry setCarryOpt getCarry
+ getMem setMem overflows.
+
+ Lemma pseudo_var: forall {w s n} b k x v m c,
+ (k < n)%nat
+ -> nth_error x k = Some v
+ -> pseudoEval (@PVar w s n b (indexize k)) (x, m, c) = Some ([v], m, c).
+ Proof.
+ intros; autounfold; simpl; unfold indexize.
+ destruct (le_dec n 0); simpl. {
+ replace k with 0 in * by omega; autounfold; simpl in *.
+ rewrite H0; simpl; intuition.
+ }
+
+ replace (k mod n) with k by admit. (* TODO (rsloan): find lemma name *)
+
+ autounfold; simpl.
+ destruct (nth_error x k); simpl; try inversion H0; intuition.
+ Qed.
+
+ Lemma pseudo_mem: forall {w s} n v m c x name len index,
+ TripleM.find (w, name mod n, index mod len)%nat m = Some (@wordToN w v)
+ -> pseudoEval (@PMem w s n len (indexize name) (indexize index)) (x, m, c) = Some ([v], m, c).
+ Proof.
+ intros; autounfold; simpl.
+ unfold indexize;
+ destruct (le_dec n 0), (le_dec len 0);
+ try replace n with 0 in * by intuition;
+ try replace len with 0 in * by intuition;
+ autounfold; simpl in *; rewrite H;
+ autounfold; simpl; rewrite NToWord_wordToN;
+ intuition.
+ Qed.
+
+ Lemma pseudo_const: forall {w s n} x v m c,
+ pseudoEval (@PConst w s n v) (x, m, c) = Some ([v], m, c).
+ Proof. intros; simpl; intuition. Qed.
+
+ Lemma pseudo_plus:
+ forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1,
+ pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
+ -> pseudoEval (PBin n Add p) (x, m0, c0) =
+ Some ([out0 ^+ out1], m1,
+ Some (proj1_sig (bool_of_sumbool
+ (overflows w (&out0 + &out1)%N)%w))).
+ Proof.
+ intros; simpl; rewrite H; simpl.
+
+ pose proof (wordize_plus out0 out1).
+ destruct (overflows w _); autounfold; simpl; try rewrite H0;
+ try rewrite <- (@Npow2_ignore w (out0 ^+ out1));
+ try rewrite NToWord_wordToN; intuition.
+ Qed.
+
+ Lemma pseudo_bin:
+ forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1 op,
+ op <> Add
+ -> pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
+ -> pseudoEval (PBin n op p) (x, m0, c0) =
+ Some ([fst (evalIntOp op out0 out1)], m1, c1).
+ Proof.
+ intros; simpl; rewrite H0; simpl.
+
+ induction op;
+ try (contradict H; reflexivity);
+ unfold evalIntOp; autounfold; simpl;
+ reflexivity.
+ Qed.
+
+ Lemma pseudo_and:
+ forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1,
+ pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
+ -> pseudoEval (PBin n And p) (x, m0, c0) =
+ Some ([out0 ^& out1], m1, c1).
+ Proof.
+ intros.
+ replace (out0 ^& out1) with (fst (evalIntOp And out0 out1)).
+ - apply pseudo_bin; intuition; inversion H0.
+ - unfold evalIntOp; simpl; intuition.
+ Qed.
+
+ Lemma pseudo_awc:
+ forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c,
+ pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, Some c)
+ -> pseudoEval (PCarry n AddWithCarry p) (x, m0, c0) =
+ Some ([addWithCarry out0 out1 c], m1,
+ Some (proj1_sig (bool_of_sumbool (overflows w
+ (&out0 + &out1 + (if c then 1 else 0))%N)%w))).
+ Proof.
+ intros; simpl; rewrite H; simpl.
+
+ pose proof (wordize_awc out0 out1); unfold evalCarryOp.
+ destruct (overflows w ((& out0)%w + (& out1)%w +
+ (if c then 1%N else 0%N)));
+ autounfold; simpl; try rewrite H0; intuition.
+ Qed.
+
+ Lemma pseudo_shiftr:
+ forall {w s n} (p: @Pseudo w s n 1) x out m0 m1 c0 c1 k,
+ pseudoEval p (x, m0, c0) = Some ([out], m1, c1)
+ -> pseudoEval (PShift n Shr k p) (x, m0, c0) =
+ Some ([shiftr out k], m1, c1).
+ Proof.
+ intros; simpl; rewrite H; autounfold; simpl.
+ rewrite wordize_shiftr; rewrite NToWord_wordToN; intuition.
+ Qed.
+
+ Lemma pseudo_mult:
+ forall {w s n} (p: @Pseudo w s n 2) x out0 out1 m0 m1 c0 c1,
+ pseudoEval p (x, m0, c0) = Some ([out0; out1], m1, c1)
+ -> pseudoEval (PDual n Mult p) (x, m0, c0) =
+ Some ([out0 ^* out1; multHigh out0 out1], m1, c1).
+ Proof.
+ intros; simpl; rewrite H; autounfold; simpl; intuition.
+ Qed.
+
+ Lemma pseudo_comb:
+ forall {w s n a b} (p0: @Pseudo w s n a) (p1: @Pseudo w s n b)
+ input out0 out1 m0 m1 m2 c0 c1 c2,
+ pseudoEval p0 (input, m0, c0) = Some (out0, m1, c1)
+ -> pseudoEval p1 (input, m1, c1) = Some (out1, m2, c2)
+ -> pseudoEval (@PComb w s n _ _ p0 p1) (input, m0, c0) =
+ Some (out0 ++ out1, m2, c2).
+ Proof.
+ intros; autounfold; simpl.
+ rewrite H; autounfold; simpl.
+ rewrite H0; autounfold; simpl; intuition.
+ Qed.
+
+ Lemma pseudo_cons:
+ forall {w s n b} (p0: @Pseudo w s n 1) (p1: @Pseudo w s n b)
+ (p2: @Pseudo w s n (S b)) input x xs m0 m1 m2 c0 c1 c2,
+ pseudoEval p0 (input, m0, c0) = Some ([x], m1, c1)
+ -> pseudoEval p1 (input, m1, c1) = Some (xs, m2, c2)
+ -> p2 = (@PComb w s n _ _ p0 p1)
+ -> pseudoEval p2 (input, m0, c0) = Some (x :: xs, m2, c2).
+ Proof.
+ intros.
+ replace (x :: xs) with ([x] ++ xs) by (simpl; intuition).
+ rewrite H1.
+ apply (pseudo_comb p0 p1 input _ _ m0 m1 m2 c0 c1 c2); intuition.
+ Qed.
+
+ Lemma pseudo_let:
+ forall {w s n k m} (p0: @Pseudo w s n k) (p1: @Pseudo w s (n + k) m)
+ input out0 out1 m0 m1 m2 c0 c1 c2,
+ pseudoEval p0 (input, m0, c0) = Some (out0, m1, c1)
+ -> pseudoEval p1 (input ++ out0, m1, c1) = Some (out1, m2, c2)
+ -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) =
+ Some (out1, m2, c2).
+ Proof.
+ intros; autounfold; simpl.
+ rewrite H; autounfold; simpl.
+ rewrite H0; autounfold; simpl; intuition.
+ Qed.
+
+ Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type :=
+ {p: @Pseudo w s n m | forall x: (list (word w)),
+ List.length x = n -> exists m' c',
+ pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}.
+
+ Ltac autodestruct :=
+ repeat match goal with
+ | [H: context[Datatypes.length (cons _ _)] |- _] => simpl in H
+ | [H: context[Datatypes.length nil] |- _] => simpl in H
+ | [H: S ?a = S ?b |- _] => inversion H; clear H
+ | [H: (S ?a) = 0 |- _] => contradict H; intuition
+ | [H: 0 = (S ?a) |- _] => contradict H; intuition
+ | [H: 0 = 0 |- _] => clear H
+ | [x: list ?T |- _] =>
+ match goal with
+ | [H: context[Datatypes.length x] |- _] => destruct x
+ end
+ end.
+
+ Ltac pseudo_step :=
+ match goal with
+ | [ |- pseudoEval ?p _ = Some ([?x ^& ?y], _, _) ] =>
+ is_evar p; eapply pseudo_and
+ | [ |- pseudoEval ?p _ = Some ([?x ^+ ?y], _, _) ] =>
+ is_evar p; eapply pseudo_plus
+ | [ |- pseudoEval ?p _ = Some (cons ?x (cons _ _), _, _) ] =>
+ is_evar p; eapply pseudo_cons; try reflexivity
+ | [ |- pseudoEval ?p _ = Some ([natToWord _ ?x], _, _)%p ] =>
+ is_evar p; eapply pseudo_const
+ | [ |- @pseudoEval ?n _ _ _ ?P (?lst, _, _) =
+ Some ([nth ?i ?lst _], _, _)%p ] =>
+ eapply (pseudo_var None); simpl; intuition
+ end.
+
+ Ltac pseudo_solve :=
+ repeat eexists;
+ autounfold;
+ autodestruct;
+ repeat pseudo_step.
+
+ Definition convert_example: @pseudeq 32 W32 1 1 (fun v =>
+ let a := natToWord _ 1 in
+ let b := nth 0 v (wzero _) in
+ [a ^& b]).
+
+ cbv zeta; pseudo_solve.
+
+ Defined.
+
+ Eval simpl in (proj1_sig convert_example).
+
+End Conversion.
+
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
new file mode 100644
index 000000000..48e642151
--- /dev/null
+++ b/src/Assembly/Pseudo.v
@@ -0,0 +1,182 @@
+Require Import QhasmUtil QhasmCommon QhasmEvalCommon QhasmUtil State.
+Require Import Language.
+Require Import List Compare_dec.
+
+Module Pseudo <: Language.
+ Import EvalUtil ListState.
+
+ Inductive Pseudo {w: nat} {s: Width w}: nat -> nat -> Type :=
+ | PVar: forall n, option bool -> Index n -> Pseudo n 1
+ | PMem: forall n m , Index n -> Index m -> Pseudo n 1
+ | PConst: forall n, word w -> Pseudo n 1
+ | PBin: forall n, IntOp -> Pseudo n 2 -> Pseudo n 1
+ | PDual: forall n, DualOp -> Pseudo n 2 -> Pseudo n 2
+ | PCarry: forall n, CarryOp -> Pseudo n 2 -> Pseudo n 1
+ | PShift: forall n, RotOp -> Index w -> Pseudo n 1 -> Pseudo n 1
+ | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n
+ | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m
+ | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b)
+ | PCall: forall n m, Label -> Pseudo n m -> Pseudo n m
+ | PIf: forall n m, TestOp -> Index n -> Index n ->
+ Pseudo n m -> Pseudo n m -> Pseudo n m.
+
+ Hint Constructors Pseudo.
+
+ Record Params': Type := mkParams {
+ width: nat;
+ spec: Width width;
+ inputs: nat;
+ outputs: nat
+ }.
+
+ Definition Params := Params'.
+ Definition State (p: Params): Type := ListState (width p).
+ Definition Program (p: Params): Type :=
+ @Pseudo (width p) (spec p) (inputs p) (outputs p).
+
+ Definition Unary32: Params := mkParams 32 W32 1 1.
+ Definition Unary64: Params := mkParams 64 W64 1 1.
+
+ (* Evaluation *)
+
+ Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w): option (ListState w) :=
+ match prog with
+ | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st))
+ | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st))
+ | PConst n c => Some (setList [c] st)
+ | PBin n o p =>
+ omap (pseudoEval p st) (fun sp =>
+ match (getList sp) with
+ | [wa; wb] =>
+ let (v, c) := evalIntOp o wa wb in
+ Some (setList [v] (setCarryOpt c sp))
+ | _ => None
+ end)
+
+ | PCarry n o p =>
+ omap (pseudoEval p st) (fun sp =>
+ match (getList sp, getCarry sp) with
+ | ([wa; wb], Some c) =>
+ let (v, c') := evalCarryOp o wa wb c in
+ Some (setList [v] (setCarry c' sp))
+ | _ => None
+ end)
+
+ | PDual n o p =>
+ omap (pseudoEval p st) (fun sp =>
+ match (getList sp) with
+ | [wa; wb] =>
+ let (low, high) := evalDualOp o wa wb in
+ Some (setList [low; high] sp)
+ | _ => None
+ end)
+
+ | PShift n o a x =>
+ omap (pseudoEval x st) (fun sx =>
+ match (getList sx) with
+ | [wx] => Some (setList [evalRotOp o wx a] sx)
+ | _ => None
+ end)
+
+ | PLet n k m f g =>
+ omap (pseudoEval f st) (fun sf =>
+ omap (pseudoEval g (setList ((getList st) ++ (getList sf)) sf))
+ (fun sg => Some sg))
+
+ | PComb n a b f g =>
+ omap (pseudoEval f st) (fun sf =>
+ omap (pseudoEval g (setList (getList st) sf)) (fun sg =>
+ Some (setList ((getList sf) ++ (getList sg)) sg)))
+
+ | PIf n m t i0 i1 l r =>
+ omap (getVar i0 st) (fun v0 =>
+ omap (getVar i1 st) (fun v1 =>
+ if (evalTest t v0 v1)
+ then pseudoEval l st
+ else pseudoEval r st ))
+
+ | PFunExp n p e =>
+ (fix funexpseudo (e': nat) (st': ListState w) :=
+ match e' with
+ | O => Some st'
+ | S e'' =>
+ omap (pseudoEval p st') (fun st'' =>
+ funexpseudo e'' st'')
+ end) e st
+
+ | PCall n m _ p => pseudoEval p st
+ end.
+
+ Definition evaluatesTo (p: Params) (prog: Program p) (st st': State p) :=
+ pseudoEval prog st = Some st'.
+
+ Delimit Scope pseudo_notations with p.
+ Local Open Scope pseudo_notations.
+
+ Definition indexize {n: nat} (x: nat): Index n.
+ intros; destruct (le_dec n 0).
+
+ - exists 0; abstract intuition.
+ - exists (x mod n); abstract (
+ pose proof (mod_bound_pos x n); omega).
+ Defined.
+
+ Notation "% A" := (PVar _ (Some false) (indexize A))
+ (at level 20, right associativity) : pseudo_notations.
+
+ Notation "$ A" := (PVar _ (Some true) (indexize A))
+ (at level 20, right associativity) : pseudo_notations.
+
+ Notation "A :[ B ]:" := (PMem _ _ (indexize A) (indexize B))
+ (at level 20, right associativity) : pseudo_notations.
+
+ Notation "# A" := (PConst _ (natToWord _ A))
+ (at level 20, right associativity) : pseudo_notations.
+
+ Notation "A :+: B" := (PBin _ Add (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))
+ (at level 60, right associativity) : pseudo_notations.
+
+ Notation "A :&: B" := (PBin _ And (PComb _ _ _ A B))
+ (at level 45, right associativity) : pseudo_notations.
+
+ Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B))
+ (at level 45, right associativity) : pseudo_notations.
+
+ Notation "A :>>: B" := (PShift _ Shr (indexize B) A)
+ (at level 60, right associativity) : pseudo_notations.
+
+ Notation "A :<<: B" := (PShift _ Shl (indexize B) A)
+ (at level 60, right associativity) : pseudo_notations.
+
+ Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B))
+ (at level 55, right associativity) : pseudo_notations.
+
+ Notation "O :( A , B ): :?: L ::: R" :=
+ (PIf _ _ O (indexize A) (indexize B) L R)
+ (at level 70, right associativity) : pseudo_notations.
+
+ Notation "F :**: e" :=
+ (PFunExp _ F e)
+ (at level 70, right associativity) : pseudo_notations.
+
+ Notation "E :->: F" :=
+ (PLet _ _ _ E F)
+ (at level 70, right associativity) : pseudo_notations.
+
+ Notation "A :|: B" :=
+ (PComb _ _ _ A B)
+ (at level 65, left associativity) : pseudo_notations.
+
+ Notation "n ::: A :():" :=
+ (PCall _ _ n A)
+ (at level 65, left associativity) : pseudo_notations.
+
+ Close Scope pseudo_notations.
+End Pseudo.
+
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
new file mode 100644
index 000000000..35f8e1e30
--- /dev/null
+++ b/src/Assembly/PseudoConversion.v
@@ -0,0 +1,238 @@
+Require Export Language Conversion QhasmCommon QhasmEvalCommon QhasmUtil.
+Require Export Pseudo AlmostQhasm State.
+Require Import Bedrock.Word NArith NPeano Euclid.
+Require Import List Sumbool Vector.
+
+Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
+ Import AlmostQhasm EvalUtil ListState Pseudo ListNotations.
+
+ Section Conv.
+ Variable w: nat.
+ Variable s: Width w.
+
+ Definition MMap := NatM.t (Mapping w).
+ Definition mempty := NatM.empty (Mapping w).
+
+ Definition FMap := NatM.t (AlmostProgram * (list (Mapping w))).
+ Definition fempty := NatM.empty (AlmostProgram * (list (Mapping w))).
+
+ Definition getStart {n m} (prog: @Pseudo w s n m) :=
+ let ns := (fix getStart' {n' m'} (prog': @Pseudo w s n' m') :=
+ match prog' with
+ | PVar _ _ i => [proj1_sig i]
+ | PBin _ _ p => getStart' p
+ | PDual _ _ p => getStart' p
+ | PCarry _ _ p => getStart' p
+ | PShift _ _ _ p => getStart' p
+ | PFunExp _ p _ => getStart' p
+ | PCall _ _ _ p => getStart' p
+ | PIf _ _ _ _ _ l r => (getStart' l) ++ (getStart' r)
+ | PLet _ k _ a b => (n + k) :: (getStart' a) ++ (getStart' b)
+ | PComb _ _ _ a b => (getStart' a) ++ (getStart' b)
+ | _ => []
+ end) _ _ prog in
+
+ (fix maxN (lst: list nat) :=
+ match lst with
+ | [] => O
+ | x :: xs => max x (maxN xs)
+ end) (n :: m :: ns).
+
+ Definition addMap {T} (a b: (NatM.t T)) : NatM.t T :=
+ (fix add' (m: NatM.t T) (elts: list (nat * T)%type) :=
+ match elts with
+ | [] => m
+ | (k, v) :: elts' => add' (NatM.add k v m) elts'
+ end) a (NatM.elements b).
+
+ Fixpoint convertProgram' {n m} (prog: @Pseudo w s n m) (start: nat) (M: MMap) (F: FMap) :
+ option (AlmostProgram * (list (Mapping w)) * MMap * FMap) :=
+
+ let rM := fun (x: nat) => regM _ (reg s x) in
+ let sM := fun (x: nat) => stackM _ (stack s x) in
+ let reg' := reg s in
+ let stack' := stack s in
+ let const' := constant s in
+
+ let G := fun (k: nat) =>
+ match (NatM.find k M) with
+ | Some v => v
+ | _ => rM k (* TODO: more intelligent defaults *)
+ end in
+
+ let madd := fun (k: nat) (f: nat -> Mapping w) =>
+ NatM.add k (f k) in
+
+ let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping w)) =>
+ NatM.add k (f, r) in
+
+ match prog with
+ | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM M, F)
+ | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM M, F)
+ | PVar n None i => Some (ASkip, [G i], M, F)
+
+ | PConst n c =>
+ Some (AAssign (AConstInt (reg' start) (const' c)),
+ [rM start], madd start rM M, F)
+
+ | PMem n m v i =>
+ Some (AAssign (ARegMem (reg' start) (mem s v) i),
+ [rM start], madd start rM M, F)
+
+ | PBin n o p =>
+ match (convertProgram' p start M F) with
+ | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
+ Some (ASeq p' (AOp (IOpReg o (reg' a) (reg' b))),
+ [rM a], madd a rM (madd b rM M'), F')
+
+ | Some (p', [regM (reg _ _ a); constM c], M', F') =>
+ Some (ASeq p' (AOp (IOpConst o (reg' a) c)),
+ [rM a], madd a rM M', F')
+
+ | Some (p', [regM (reg _ _ a); memM _ b i], M', F') =>
+ Some (ASeq p' (AOp (IOpMem o (reg' a) b i)),
+ [rM a], madd a rM M', F')
+
+ | Some (p', [regM (reg _ _ a); stackM (stack _ _ b)], M', F') =>
+ Some (ASeq p' (AOp (IOpStack o (reg' a) (stack' b))),
+ [rM a], madd a rM (madd b sM M'), F')
+
+ | _ => None
+ end
+
+ | PCarry n o p =>
+ match (convertProgram' p start M F) with
+ | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
+ Some (ASeq p' (AOp (COp o (reg' a) (reg' b))),
+ [rM a], madd a rM (madd b rM M'), F')
+
+ | _ => None
+ end
+
+ | PDual n o p =>
+ match (convertProgram' p (S start) M F) with
+ | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
+ Some (ASeq p' (AOp (DOp o (reg' a) (reg' b) (Some (reg' start)))),
+ [rM a; rM start], madd a rM (madd b rM (madd start rM M')), F')
+
+ | _ => None
+ end
+
+ | PShift n o x p =>
+ match (convertProgram' p start M F) with
+ | Some (p', [regM (reg _ _ a)], M', F') =>
+ Some (ASeq p' (AOp (ROp o (reg' a) x)),
+ [rM a], madd a rM M', F')
+
+ | _ => None
+ end
+
+ | PLet n k m f g =>
+ match (convertProgram' f start M F) with
+ | None => None
+ | Some (fp, fm, M', F') =>
+ match (convertProgram' g (start + (length fm)) M' F') with
+ | None => None
+ | Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'')
+ end
+ end
+
+ | PComb n a b f g =>
+ match (convertProgram' f start M F) with
+ | None => None
+ | Some (fp, fm, M', F') =>
+ match (convertProgram' g (start + (length fm)) M' F') with
+ | None => None
+ | Some (gp, gm, M'', F'') => Some (ASeq fp gp, fm ++ gm, M'', F'')
+ end
+ end
+
+ | PIf n m o i0 i1 l r =>
+ match (convertProgram' l start M F) with
+ | None => None
+ | Some (lp, lr, lM, lF) =>
+
+ match (convertProgram' r start lM lF) with
+ | None => None
+ | Some (rp, rr, M', F') =>
+
+ if (list_eq_dec mapping_dec lr rr)
+ then
+ match (G (proj1_sig i0), G (proj1_sig i1)) with
+ | (regM r0, regM r1) => Some (ACond (CReg _ o r0 r1) lp rp, lr, M', F')
+ | (regM r, constM c) => Some (ACond (CConst _ o r c) lp rp, lr, M', F')
+ | _ => None
+ end
+ else None
+ end
+ end
+
+ | PFunExp n f e =>
+ match (convertProgram' f (S start) M F) with
+ | Some (fp, fr, M', F') =>
+ let a := start in
+ 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)))))),
+ fr, madd a rM M', F')
+
+ | _ => None
+ end
+
+ | PCall n m lbl f =>
+ match (convertProgram' f start M F) with
+ | Some (fp, fr, M', F') =>
+ let F'' := NatM.add lbl (fp, fr) F' in
+ Some (ACall lbl, fr, M', F'')
+ | None => None
+ end
+ end.
+
+ End Conv.
+
+ Definition convertProgram x y (prog: Program x) : option (AlmostQhasm.Program y) :=
+ let vs := max (inputs x) (outputs x) in
+ let M0 := mempty (width x) in
+ let F0 := fempty (width x) in
+
+ match (convertProgram' (width x) (spec x) prog vs M0 F0) with
+ | Some (prog', _, M, F) =>
+ Some (fold_left
+ (fun p0 t => match t with | (k, (v, _)) => ADef k v p0 end)
+ prog'
+ (of_list (NatM.elements F)))
+ | _ => None
+ end.
+
+ Fixpoint convertState x y (st: AlmostQhasm.State y) : option (State x) :=
+ let vars := max (inputs x) (outputs x) in
+
+ let try_cons := fun {T} (x: option T) (l: list T) =>
+ match x with | Some x' => x' :: l | _ => l end in
+
+ let get := fun i =>
+ match (FullState.getReg (reg (spec x) i) st,
+ FullState.getStack (stack (spec x) i) st) with
+ | (Some v, _) => Some v
+ | (_, Some v) => Some v
+ | _ => None
+ end in
+
+ let varList := (fix cs' (n: nat) :=
+ try_cons (get (vars - n)) (match n with | O => [] | S m => cs' m end)) vars in
+
+ match st with
+ | FullState.fullState _ _ memState _ carry =>
+ if (Nat.eq_dec (length varList) vars)
+ then Some (varList, memState, carry)
+ else None
+ end.
+
+ Lemma convert_spec: forall pa pb a a' b b' prog prog',
+ convertProgram pa pb prog = Some prog' ->
+ convertState pa pb a = Some a' ->
+ convertState pa pb b = Some b' ->
+ AlmostQhasm.evaluatesTo pb prog' a b <-> evaluatesTo pa prog a' b'.
+ Admitted.
+End PseudoConversion.
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
new file mode 100644
index 000000000..9ba2c0a56
--- /dev/null
+++ b/src/Assembly/Qhasm.v
@@ -0,0 +1,87 @@
+Require Import QhasmCommon QhasmEvalCommon.
+Require Import Language.
+Require Import List NPeano.
+
+Module Qhasm <: Language.
+ Import ListNotations.
+ Import QhasmEval.
+
+ (* A constant upper-bound on the number of operations we run *)
+ Definition Params := unit.
+ Definition State := fun (_: Params) => State.
+
+ Transparent Params.
+
+ (* Program Types *)
+ Inductive QhasmStatement :=
+ | QAssign: Assignment -> QhasmStatement
+ | QOp: Operation -> QhasmStatement
+ | QCond: Conditional -> Label -> QhasmStatement
+ | QLabel: Label -> QhasmStatement
+ | QCall: Label -> QhasmStatement
+ | QRet: QhasmStatement.
+
+ Hint Constructors QhasmStatement.
+
+ Definition Program := fun (_: Params) => list QhasmStatement.
+
+ (* Only execute while loops a fixed number of times.
+ TODO (rsloan): can we do any better? *)
+
+ Fixpoint getLabelMap' {x} (prog: Program x) (cur: LabelMap) (index: nat): LabelMap :=
+ match prog with
+ | p :: ps =>
+ match p with
+ | QLabel label => @getLabelMap' x ps (NatM.add label index cur) (S index)
+ | _ => @getLabelMap' x ps cur (S index)
+ end
+ | [] => cur
+ end.
+
+ Definition getLabelMap {x} (prog: Program x): LabelMap :=
+ getLabelMap' prog (NatM.empty nat) O.
+
+ Inductive QhasmEval {x}: nat -> Program x -> LabelMap -> State x -> State x -> Prop :=
+ | QEOver: forall p n m s, (n > (length p))%nat -> QhasmEval n p m s s
+ | QEZero: forall p s m, QhasmEval O p m s s
+ | QEAssign: forall n p m a s s' s'',
+ (nth_error p n) = Some (QAssign a)
+ -> evalAssignment a s = Some s'
+ -> QhasmEval (S n) p m s' s''
+ -> QhasmEval n p m s s''
+ | QEOp: forall n p m a s s' s'',
+ (nth_error p n) = Some (QOp a)
+ -> evalOperation a s = Some s'
+ -> QhasmEval (S n) p m s' s''
+ -> QhasmEval n p m s s''
+ | QECondTrue: forall (n loc next: nat) p m c l s s',
+ (nth_error p n) = Some (QCond c l)
+ -> evalCond c s = Some true
+ -> NatM.find l m = Some loc
+ -> QhasmEval loc p m s s'
+ -> QhasmEval n p m s s'
+ | QECondFalse: forall (n loc next: nat) p m c l s s',
+ (nth_error p n) = Some (QCond c l)
+ -> evalCond c s = Some false
+ -> QhasmEval (S n) p m s s'
+ -> QhasmEval n p m s s'
+ | QERet: forall (n n': nat) s s' s'' p m,
+ (nth_error p n) = Some QRet
+ -> popRet s = Some (s', n')
+ -> QhasmEval n' p m s' s''
+ -> QhasmEval n p m s s''
+ | QECall: forall (w n n' lbl: nat) s s' s'' p m,
+ (nth_error p n) = Some (QCall lbl)
+ -> NatM.find lbl m = Some n'
+ -> QhasmEval n' p m (pushRet (S n) s') s''
+ -> QhasmEval n p m s s''
+ | QELabel: forall n p m l s s',
+ (nth_error p n) = Some (QLabel l)
+ -> QhasmEval (S n) p m s s'
+ -> QhasmEval n p m s s'.
+
+ Definition evaluatesTo := fun (x: Params) p => @QhasmEval x O p (getLabelMap p).
+
+ (* world peace *)
+End Qhasm.
+
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
new file mode 100644
index 000000000..ccec401d2
--- /dev/null
+++ b/src/Assembly/QhasmCommon.v
@@ -0,0 +1,129 @@
+Require Export String List NPeano NArith.
+Require Export Bedrock.Word.
+
+(* Utilities *)
+Definition Label := nat.
+
+Definition Index (limit: nat) := {x: nat | (x <= (pred limit))%nat}.
+Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
+
+Inductive Either A B :=
+ | xleft: A -> Either A B
+ | xright: B -> Either A B.
+
+Definition convert {A B: Type} (x: A) (H: A = B): B :=
+ eq_rect A (fun B0 : Type => B0) x B H.
+
+(* Asm Types *)
+Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64.
+
+(* A constant value *)
+Inductive Const: nat -> Type :=
+ | constant: forall {n}, Width n -> word n -> Const n.
+
+(* A variable in any register *)
+Inductive Reg: nat -> Type :=
+ | reg: forall {n}, Width n -> nat -> Reg n.
+
+(* A variable on the stack. We should use this sparingly. *)
+Inductive Stack: nat -> Type :=
+ | stack: forall {n}, Width n -> nat -> Stack n.
+
+(* A pointer to a memory block. Called as:
+ mem width index length
+ where length is in words of size width.
+
+ All Mem pointers will be declared as Stack arguments in the
+ resulting qhasm output *)
+Inductive Mem: nat -> nat -> Type :=
+ | mem: forall {n m}, Width n -> nat -> Mem n m.
+
+(* The state of the carry flag:
+ 1 = Some true
+ 0 = Some false
+ unknown = None *)
+Definition Carry := option bool.
+
+(* Assignments *)
+
+Inductive Assignment : Type :=
+ | ARegMem: forall {n m}, Reg n -> Mem n m -> Index m -> Assignment
+ | AMemReg: forall {n m}, Mem n m -> Index m -> Reg n -> Assignment
+ | AStackReg: forall {n}, Stack n -> Reg n -> Assignment
+ | ARegStack: forall {n}, Reg n -> Stack n -> Assignment
+ | ARegReg: forall {n}, Reg n -> Reg n -> Assignment
+ | AConstInt: forall {n}, Reg n -> Const n -> Assignment.
+
+(* Operations *)
+
+Inductive IntOp :=
+ | Add: IntOp | Sub: IntOp
+ | Xor: IntOp | And: IntOp
+ | Or: IntOp.
+
+Inductive CarryOp := | AddWithCarry: CarryOp.
+
+Inductive DualOp := | Mult: DualOp.
+
+Inductive RotOp := | Shl: RotOp | Shr: RotOp.
+
+Inductive Operation :=
+ | IOpConst: forall {n}, IntOp -> Reg n -> Const n -> Operation
+ | IOpReg: forall {n}, IntOp -> Reg n -> Reg n -> Operation
+ | IOpMem: forall {n m}, IntOp -> Reg n -> Mem n m -> Index m -> Operation
+ | IOpStack: forall {n}, IntOp -> Reg n -> Stack n -> Operation
+ | DOp: forall {n}, DualOp -> Reg n -> Reg n -> option (Reg n) -> Operation
+ | ROp: forall {n}, RotOp -> Reg n -> Index n -> Operation
+ | COp: forall {n}, CarryOp -> Reg n -> Reg n -> Operation.
+
+(* Control Flow *)
+
+Inductive TestOp :=
+ | TEq: TestOp | TLt: TestOp | TLe: TestOp
+ | TGt: TestOp | TGe: TestOp.
+
+Inductive Conditional :=
+ | CTrue: Conditional
+ | CZero: forall n, Reg n -> Conditional
+ | CReg: forall n, TestOp -> Reg n -> Reg n -> Conditional
+ | CConst: forall n, TestOp -> Reg n -> Const n -> Conditional.
+
+(* Generalized Variable Entry *)
+
+Inductive Mapping (n: nat) :=
+ | regM: forall (r: Reg n), Mapping n
+ | stackM: forall (s: Stack n), Mapping n
+ | memM: forall {m} (x: Mem n m) (i: Index m), Mapping n
+ | constM: forall (x: Const n), Mapping n.
+
+(* Parameter Accessors *)
+
+Definition constWidth {n} (x: Const n): nat := n.
+
+Definition regWidth {n} (x: Reg n): nat := n.
+
+Definition stackWidth {n} (x: Stack n): nat := n.
+
+Definition memWidth {n m} (x: Mem n m): nat := n.
+
+Definition memLength {n m} (x: Mem n m): nat := m.
+
+Definition constValueW {n} (x: Const n): word n :=
+ match x with | @constant n _ v => v end.
+
+Definition constValueN {n} (x: Const n): nat :=
+ match x with | @constant n _ v => wordToNat v end.
+
+Definition regName {n} (x: Reg n): nat :=
+ match x with | @reg n _ v => v end.
+
+Definition stackName {n} (x: Stack n): nat :=
+ match x with | @stack n _ v => v end.
+
+Definition memName {n m} (x: Mem n m): nat :=
+ match x with | @mem n m _ v => v end.
+
+(* Hints *)
+Hint Constructors
+ Reg Stack Const Mem Mapping
+ Assignment Operation Conditional.
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
new file mode 100644
index 000000000..dbd46b1b4
--- /dev/null
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -0,0 +1,267 @@
+Require Import QhasmCommon QhasmUtil State.
+Require Import ZArith Sumbool.
+Require Import Bedrock.Word.
+Require Import Logic.Eqdep_dec ProofIrrelevance.
+
+Module EvalUtil.
+ Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
+ let c := (N.compare (wordToN a) (wordToN b)) in
+
+ let eqBit := match c with | Eq => true | _ => false end in
+ let ltBit := match c with | Lt => true | _ => false end in
+ let gtBit := match c with | Gt => true | _ => false end in
+
+ match o with
+ | TEq => eqBit
+ | TLt => ltBit
+ | TLe => orb (eqBit) (ltBit)
+ | TGt => gtBit
+ | TGe => orb (eqBit) (gtBit)
+ end.
+
+ Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool :=
+ match io with
+ | Add =>
+ let v := (wordToN x + wordToN y)%N in
+ let c := (overflows b (&x + &y)%N)%w in
+
+ match c as c' return c' = c -> _ with
+ | 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 :=
+ match io with
+ | AddWidthCarry =>
+ 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
+ | right _ => fun _ => (v, false)
+ | left _ => fun _ => (v, true)
+ end eq_refl
+ end.
+
+ Definition highBits {n} (m: nat) (x: word n) := snd (break m x).
+
+ Definition multHigh {n} (x y: word n): word n.
+ refine (@extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y)));
+ abstract omega.
+ Defined.
+
+ Definition evalDualOp {n} (duo: DualOp) (x y: word n) :=
+ match duo with
+ | Mult => (x ^* y, multHigh x y)
+ end.
+
+ Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
+ match ro with
+ | Shl => NToWord b (N.shiftl_nat (wordToN x) n)
+ | Shr => NToWord b (N.shiftr_nat (wordToN x) n)
+ end.
+
+ (* Width decideability *)
+
+ Definition getWidth (n: nat): option (Width n) :=
+ match n with
+ | 32 => Some W32
+ | 64 => Some W64
+ | _ => None
+ end.
+
+ Lemma getWidth_eq {n} (a: Width n): Some a = getWidth n.
+ Proof. induction a; unfold getWidth; simpl; intuition. Qed.
+
+ Lemma width_eq {n} (a b: Width n): a = b.
+ Proof.
+ assert (Some a = Some b) as H by (
+ replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition);
+ replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition);
+ intuition).
+ inversion H; intuition.
+ Qed.
+
+ (* Mapping Conversions *)
+
+ Definition wordToM {n: nat} {spec: Width n} (w: word n): Mapping n :=
+ constM _ (constant spec w).
+
+ Definition regToM {n: nat} {spec: Width n} (r: Reg n): Mapping n :=
+ regM _ r.
+
+ Definition stackToM {n: nat} {spec: Width n} (s: Stack n): Mapping n :=
+ stackM _ s.
+
+ Definition constToM {n: nat} {spec: Width n} (c: Const n): Mapping n :=
+ constM _ c.
+
+ Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}.
+ refine (match (a, b) as p' return (a, b) = p' -> _ with
+ | (regM v, regM v') => fun _ =>
+ if (Nat.eq_dec (regName v) (regName v'))
+ then left _
+ else right _
+
+ | (stackM v, stackM v') => fun _ =>
+ if (Nat.eq_dec (stackName v) (stackName v'))
+ then left _
+ else right _
+
+ | (constM v, constM v') => fun _ =>
+ if (Nat.eq_dec (constValueN v) (constValueN v'))
+ then left _
+ else right _
+
+ | (memM _ v i, memM _ v' i') => fun _ =>
+ if (Nat.eq_dec (memName v) (memName v'))
+ then if (Nat.eq_dec (memLength v) (memLength v'))
+ then if (Nat.eq_dec (proj1_sig i) (proj1_sig i'))
+ then left _ else right _ else right _ else right _
+
+ | _ => fun _ => right _
+ end (eq_refl (a, b))); abstract (
+ inversion_clear _H;
+ 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 ]).
+ Defined.
+
+ Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}.
+ assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true})
+ by abstract (destruct (a <? b)%nat; intuition);
+ destruct H.
+
+ - left; abstract (apply Nat.ltb_lt in e; intuition).
+
+ - right; abstract (rewrite Nat.ltb_lt in n; intuition).
+ Defined.
+
+ Fixpoint stackNames {n} (lst: list (Mapping n)): list nat :=
+ match lst with
+ | nil => nil
+ | cons c cs =>
+ match c with
+ | stackM v => cons (stackName v) (stackNames cs)
+ | _ => stackNames cs
+ end
+ end.
+
+ Fixpoint regNames {n} (lst: list (Mapping n)): list nat :=
+ match lst with
+ | nil => nil
+ | cons c cs =>
+ match c with
+ | regM v => cons (regName v) (regNames cs)
+ | _ => regNames cs
+ end
+ end.
+
+End EvalUtil.
+
+Module QhasmEval.
+ Export EvalUtil FullState.
+
+ Definition evalCond (c: Conditional) (state: State): option bool :=
+ match c with
+ | CTrue => Some true
+ | CZero n r =>
+ omap (getReg r state) (fun v =>
+ if (Nat.eq_dec O (wordToNat v))
+ then Some true
+ else Some false)
+ | CReg n o a b =>
+ omap (getReg a state) (fun va =>
+ omap (getReg b state) (fun vb =>
+ Some (evalTest o va vb)))
+ | CConst n o a c =>
+ omap (getReg a state) (fun va =>
+ Some (evalTest o va (constValueW c)))
+ end.
+
+ Definition evalOperation (o: Operation) (state: State): option State :=
+ match o with
+ | IOpConst _ o r c =>
+ omap (getReg r state) (fun v =>
+ let (v', co) := (evalIntOp o v (constValueW c)) in
+ Some (setCarryOpt co (setReg r v' state)))
+
+ | IOpReg _ o a b =>
+ omap (getReg a state) (fun va =>
+ omap (getReg b state) (fun vb =>
+ let (v', co) := (evalIntOp o va vb) in
+ Some (setCarryOpt co (setReg a v' state))))
+
+ | IOpStack _ o a b =>
+ omap (getReg a state) (fun va =>
+ omap (getStack b state) (fun vb =>
+ let (v', co) := (evalIntOp o va vb) in
+ Some (setCarryOpt co (setReg a v' state))))
+
+ | IOpMem _ _ o r m i =>
+ omap (getReg r state) (fun va =>
+ omap (getMem m i state) (fun vb =>
+ let (v', co) := (evalIntOp o va vb) in
+ Some (setCarryOpt co (setReg r v' state))))
+
+ | DOp _ o a b (Some x) =>
+ omap (getReg a state) (fun va =>
+ omap (getReg b state) (fun vb =>
+ let (low, high) := (evalDualOp o va vb) in
+ Some (setReg x high (setReg a low state))))
+
+ | DOp _ o a b None =>
+ omap (getReg a state) (fun va =>
+ omap (getReg b state) (fun vb =>
+ let (low, high) := (evalDualOp o va vb) in
+ Some (setReg a low state)))
+
+ | ROp _ o r i =>
+ omap (getReg r state) (fun v =>
+ let v' := (evalRotOp o v i) in
+ Some (setReg r v' state))
+
+ | COp _ o a b =>
+ omap (getReg a state) (fun va =>
+ omap (getReg b state) (fun vb =>
+ match (getCarry state) with
+ | None => None
+ | Some c0 =>
+ let (v', c') := (evalCarryOp o va vb c0) in
+ Some (setCarry c' (setReg a v' state))
+ end))
+ end.
+
+ Definition evalAssignment (a: Assignment) (state: State): option State :=
+ match a with
+ | ARegMem _ _ r m i =>
+ omap (getMem m i state) (fun v => Some (setReg r v state))
+ | AMemReg _ _ m i r =>
+ omap (getReg r state) (fun v => Some (setMem m i v state))
+ | AStackReg _ a b =>
+ omap (getReg b state) (fun v => Some (setStack a v state))
+ | ARegStack _ a b =>
+ omap (getStack b state) (fun v => Some (setReg a v state))
+ | ARegReg _ a b =>
+ omap (getReg b state) (fun v => Some (setReg a v state))
+ | AConstInt _ r c =>
+ Some (setReg r (constValueW c) state)
+ end.
+
+End QhasmEval.
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
new file mode 100644
index 000000000..078cf7780
--- /dev/null
+++ b/src/Assembly/QhasmUtil.v
@@ -0,0 +1,73 @@
+
+Require Import ZArith NArith NPeano.
+Require Import QhasmCommon.
+Require Export Bedrock.Word.
+
+Delimit Scope nword_scope with w.
+Local Open Scope nword_scope.
+
+Notation "& x" := (wordToN x) (at level 30) : nword_scope.
+Notation "** x" := (NToWord _ x) (at level 30) : nword_scope.
+
+Section Util.
+ Definition convS {A B: Set} (x: A) (H: A = B): B :=
+ eq_rect A (fun B0 : Set => B0) x B H.
+
+ Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
+ refine (split1 k (n - k) (convS w _)).
+ abstract (replace n with (k + (n - k)) by omega; intuition).
+ Defined.
+
+ Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
+ refine (split2 (n - k) k (convS w _)).
+ abstract (replace n with (k + (n - k)) by omega; intuition).
+ Defined.
+
+ Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
+ refine (convS (zext w (n - k)) _).
+ abstract (replace (k + (n - k)) with n by omega; intuition).
+ Defined.
+
+ Definition shiftr {n} (w: word n) (k: nat): word n :=
+ match (le_dec k n) with
+ | left p => extend p (high p w)
+ | right _ => wzero n
+ end.
+
+ Definition mask {n} (k: nat) (w: word n): word n :=
+ match (le_dec k n) with
+ | left p => extend p (low p w)
+ | right _ => w
+ end.
+
+ Definition overflows (n: nat) (x: N) :
+ {(x >= Npow2 n)%N} + {(x < Npow2 n)%N}.
+ refine (
+ let c := (x ?= Npow2 n)%N in
+ match c as c' return c = c' -> _ with
+ | Lt => fun _ => right _
+ | _ => fun _ => left _
+ end eq_refl); abstract (
+ unfold c in *; unfold N.lt, N.ge;
+ rewrite _H in *; intuition; try inversion H).
+ Defined.
+
+ Definition break {n} (m: nat) (x: word n): word m * word (n - m).
+ refine match (le_dec m n) with
+ | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x))
+ | right p => (extend _ x, _)
+ end; try abstract intuition.
+
+ replace (n - m) with O by abstract omega; exact WO.
+ Defined.
+
+ Definition addWithCarry {n} (x y: word n) (c: bool): word n :=
+ x ^+ y ^+ (natToWord _ (if c then 1 else 0)).
+
+ Definition omap {A B} (x: option A) (f: A -> option B) :=
+ match x with | Some y => f y | _ => None end.
+
+ Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
+End Util.
+
+Close Scope nword_scope. \ No newline at end of file
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
new file mode 100644
index 000000000..20bb532ad
--- /dev/null
+++ b/src/Assembly/State.v
@@ -0,0 +1,329 @@
+Require Export String List Logic.
+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 QhasmUtil QhasmCommon.
+
+(* We want to use pairs and triples as map keys: *)
+
+Module Pair_as_OT <: UsualOrderedType.
+ Definition t := (nat * nat)%type.
+
+ Definition eq := @eq t.
+ Definition eq_refl := @eq_refl t.
+ Definition eq_sym := @eq_sym t.
+ Definition eq_trans := @eq_trans t.
+
+ Definition lt (a b: t) :=
+ if (Nat.eq_dec (fst a) (fst b))
+ then lt (snd a) (snd b)
+ else lt (fst a) (fst b).
+
+ Lemma conv: forall {x0 x1 y0 y1: nat},
+ (x0 = y0 /\ x1 = y1) <-> (x0, x1) = (y0, y1).
+ Proof.
+ intros; split; intros.
+ - destruct H; destruct H0; subst; intuition.
+ - inversion_clear H; intuition.
+ Qed.
+
+ Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+ intros; destruct x as [x0 x1], y as [y0 y1], z as [z0 z1];
+ unfold lt in *; simpl in *;
+ destruct (Nat.eq_dec x0 y0), (Nat.eq_dec y0 z0), (Nat.eq_dec x0 z0);
+ omega.
+ Qed.
+
+ Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+ intros; destruct x as [x0 x1], y as [y0 y1];
+ unfold lt, eq in *; simpl in *;
+ destruct (Nat.eq_dec x0 y0); subst; intuition;
+ inversion H0; subst; omega.
+ Qed.
+
+ Definition compare x y : Compare lt eq x y.
+ destruct x as [x0 x1], y as [y0 y1];
+ destruct (Nat_as_OT.compare x0 y0);
+ unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
+
+ - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
+
+ - destruct (Nat_as_OT.compare x1 y1);
+ unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
+
+ + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
+ + apply EQ; abstract (unfold lt; simpl; subst; intuition).
+ + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+
+ - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+ Defined.
+
+ Definition eq_dec (a b: t): {a = b} + {a <> b}.
+ destruct (compare a b);
+ destruct a as [a0 a1], b as [b0 b1].
+
+ - right; abstract (
+ unfold lt in *; simpl in *;
+ destruct (Nat.eq_dec a0 b0); intuition;
+ inversion H; intuition).
+
+ - left; abstract (inversion e; intuition).
+
+ - right; abstract (
+ unfold lt in *; simpl in *;
+ destruct (Nat.eq_dec b0 a0); intuition;
+ inversion H; intuition).
+ Defined.
+End Pair_as_OT.
+
+Module Triple_as_OT <: UsualOrderedType.
+ Definition t := (nat * nat * nat)%type.
+
+ Definition get0 (x: t) := fst (fst x).
+ Definition get1 (x: t) := snd (fst x).
+ Definition get2 (x: t) := snd x.
+
+ Definition eq := @eq t.
+ Definition eq_refl := @eq_refl t.
+ Definition eq_sym := @eq_sym t.
+ Definition eq_trans := @eq_trans t.
+
+ Definition lt (a b: t) :=
+ if (Nat.eq_dec (get0 a) (get0 b))
+ then
+ if (Nat.eq_dec (get1 a) (get1 b))
+ then lt (get2 a) (get2 b)
+ else lt (get1 a) (get1 b)
+ else lt (get0 a) (get0 b).
+
+ Lemma conv: forall {x0 x1 x2 y0 y1 y2: nat},
+ (x0 = y0 /\ x1 = y1 /\ x2 = y2) <-> (x0, x1, x2) = (y0, y1, y2).
+ Proof.
+ intros; split; intros.
+ - destruct H; destruct H0; subst; intuition.
+ - inversion_clear H; intuition.
+ Qed.
+
+ Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+ intros; unfold lt in *;
+ destruct (Nat.eq_dec (get0 x) (get0 y)),
+ (Nat.eq_dec (get1 x) (get1 y)),
+ (Nat.eq_dec (get0 y) (get0 z)),
+ (Nat.eq_dec (get1 y) (get1 z)),
+ (Nat.eq_dec (get0 x) (get0 z)),
+ (Nat.eq_dec (get1 x) (get1 z));
+ omega.
+ Qed.
+
+ Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+ intros; unfold lt, eq in *;
+ destruct (Nat.eq_dec (get0 x) (get0 y)),
+ (Nat.eq_dec (get1 x) (get1 y));
+ subst; intuition;
+ 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_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).
+
+ - apply LT; compare_tmp x y.
+ - destruct (Nat_as_OT.compare (get1 x) (get1 y)).
+ + apply LT; compare_tmp x y.
+ + destruct (Nat_as_OT.compare (get2 x) (get2 y)).
+ * apply LT; compare_tmp x y.
+ * apply EQ; compare_eq x y.
+ * apply GT; compare_tmp y x.
+ + apply GT; compare_tmp y x.
+ - apply GT; compare_tmp y x.
+ Defined.
+
+ Definition eq_dec (a b: t): {a = b} + {a <> b}.
+ destruct (compare a b);
+ destruct a as [a a2], b as [b b2];
+ destruct a as [a0 a1], b as [b0 b1].
+
+ - right; abstract (
+ unfold lt, get0, get1, get2 in *; simpl in *;
+ destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1);
+ intuition; inversion H; intuition).
+
+ - left; abstract (inversion e; intuition).
+
+ - right; abstract (
+ unfold lt, get0, get1, get2 in *; simpl in *;
+ destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1);
+ intuition; inversion H; intuition).
+ Defined.
+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).
+
+ Definition NatNMap: Type := NatM.t N.
+ Definition PairNMap: Type := PairM.t N.
+ Definition TripleNMap: Type := TripleM.t N.
+ Definition LabelMap: Type := NatM.t nat.
+End StateCommon.
+
+Module ListState.
+ Export StateCommon.
+
+ Definition ListState (n: nat) := ((list (word n)) * TripleNMap * (option bool))%type.
+
+ Definition emptyState {n}: ListState n := ([], TripleM.empty N, None).
+
+ Definition getVar {n: nat} (name: nat) (st: ListState n): option (word n) :=
+ nth_error (fst (fst st)) name.
+
+ Definition getList {n: nat} (st: ListState n): list (word n) :=
+ fst (fst st).
+
+ Definition setList {n: nat} (lst: list (word n)) (st: ListState n): ListState n :=
+ (lst, snd (fst st), snd st).
+
+ Definition getMem {n: nat} (name index: nat) (st: ListState n): option (word n) :=
+ omap (TripleM.find (n, name, index) (snd (fst st))) (fun v => Some (NToWord n v)).
+
+ Definition setMem {n: nat} (name index: nat) (v: word n) (st: ListState n): ListState n :=
+ (fst (fst st), TripleM.add (n, name, index) (wordToN v) (snd (fst st)), snd st).
+
+ Definition getCarry {n: nat} (st: ListState n): option bool := (snd st).
+
+ Definition setCarry {n: nat} (v: bool) (st: ListState n): ListState n :=
+ (fst st, Some v).
+
+ Definition setCarryOpt {n: nat} (v: option bool) (st: ListState n): ListState n :=
+ match v with
+ | Some v' => (fst st, v)
+ | None => st
+ end.
+
+End ListState.
+
+Module FullState.
+ Export StateCommon.
+
+ (* The Big Definition *)
+
+ Inductive State :=
+ | fullState (regState: PairNMap)
+ (stackState: PairNMap)
+ (memState: TripleNMap)
+ (retState: list nat)
+ (carry: Carry): State.
+
+ Definition emptyState: State :=
+ fullState (PairM.empty N) (PairM.empty N) (TripleM.empty N) [] None.
+
+ (* Register *)
+
+ Definition getReg {n} (r: Reg n) (state: State): option (word n) :=
+ match state with
+ | fullState regS _ _ _ _ =>
+ match (PairM.find (n, regName r) regS) with
+ | Some v => Some (NToWord n v)
+ | None => None
+ end
+ end.
+
+ Definition setReg {n} (r: Reg n) (value: word n) (state: State): State :=
+ match state with
+ | fullState regS stackS memS retS carry =>
+ fullState (PairM.add (n, regName r) (wordToN value) regS)
+ stackS memS retS carry
+ end.
+
+ (* Stack *)
+
+ Definition getStack {n} (s: Stack n) (state: State): option (word n) :=
+ match state with
+ | fullState _ stackS _ _ _ =>
+ match (PairM.find (n, stackName s) stackS) with
+ | Some v => Some (NToWord n v)
+ | None => None
+ end
+ end.
+
+ Definition setStack {n} (s: Stack n) (value: word n) (state: State): State :=
+ match state with
+ | fullState regS stackS memS retS carry =>
+ fullState regS
+ (PairM.add (n, stackName s) (wordToN value) stackS)
+ memS retS carry
+ end.
+
+ (* Memory *)
+
+ Definition getMem {n m} (x: Mem n m) (i: Index m) (state: State): option (word n) :=
+ match state with
+ | fullState _ _ memS _ _ =>
+ match (TripleM.find (n, memName x, proj1_sig i) memS) with
+ | Some v => Some (NToWord n v)
+ | None => None
+ end
+ end.
+
+ Definition setMem {n m} (x: Mem n m) (i: Index m) (value: word n) (state: State): State :=
+ match state with
+ | fullState regS stackS memS retS carry =>
+ fullState regS stackS
+ (TripleM.add (n, memName x, proj1_sig i) (wordToN value) memS)
+ retS carry
+ end.
+
+ (* Return Pointers *)
+
+ Definition pushRet (x: nat) (state: State): State :=
+ match state with
+ | fullState regS stackS memS retS carry =>
+ fullState regS stackS memS (cons x retS) carry
+ end.
+
+ Definition popRet (state: State): option (State * nat) :=
+ match state with
+ | fullState regS stackS memS [] carry => None
+ | fullState regS stackS memS (r :: rs) carry =>
+ Some (fullState regS stackS memS rs carry, r)
+ end.
+
+ (* Carry State Manipulations *)
+
+ Definition getCarry (state: State): Carry :=
+ match state with
+ | fullState _ _ _ _ b => b
+ end.
+
+ Definition setCarry (value: bool) (state: State): State :=
+ match state with
+ | fullState regS stackS memS retS carry =>
+ fullState regS stackS memS retS (Some value)
+ end.
+
+ Definition setCarryOpt (value: option bool) (state: State): State :=
+ match value with
+ | Some c' => setCarry c' state
+ | _ => state
+ end.
+End FullState. \ No newline at end of file
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
new file mode 100644
index 000000000..c365c5824
--- /dev/null
+++ b/src/Assembly/StringConversion.v
@@ -0,0 +1,386 @@
+Require Export Language Conversion.
+Require Export String Ascii Basics Sumbool.
+Require Import QhasmCommon QhasmEvalCommon QhasmUtil Qhasm.
+Require Import NArith NPeano.
+Require Export Bedrock.Word.
+
+Module QhasmString <: Language.
+ Definition Params := unit.
+ Definition Program := fun (_: Params) => string.
+ Definition State := fun (_: Params) => unit.
+
+ Definition evaluatesTo x (p: Program x) (i o: State x): Prop := True.
+End QhasmString.
+
+Module StringConversion <: Conversion Qhasm QhasmString.
+ Import Qhasm ListNotations.
+
+ (* The easy one *)
+ Definition convertState x y (st: QhasmString.State y): option (Qhasm.State x) := None.
+
+ (* Hexadecimal Primitives *)
+
+ Section Hex.
+ Local Open Scope string_scope.
+
+ Definition natToDigit (n : nat) : string :=
+ match n with
+ | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3"
+ | 4 => "4" | 5 => "5" | 6 => "6" | 7 => "7"
+ | 8 => "8" | 9 => "9" | 10 => "A" | 11 => "B"
+ | 12 => "C" | 13 => "D" | 14 => "E" | _ => "F"
+ end.
+
+ Fixpoint nToHex' (n: N) (digitsLeft: nat): string :=
+ match digitsLeft with
+ | O => ""
+ | S nextLeft =>
+ match n with
+ | N0 => "0"
+ | _ => (nToHex' (N.shiftr_nat n 4) nextLeft) ++
+ (natToDigit (N.to_nat (N.land n 15%N)))
+ end
+ end.
+
+ Definition nToHex (n: N): string :=
+ let size := (N.size n) in
+ let div4 := fun x => (N.shiftr x 2%N) in
+ let size' := (size + 4 - (N.land size 3))%N in
+ nToHex' n (N.to_nat (div4 size')).
+
+ End Hex.
+
+ (* Conversion of elements *)
+
+ Section Elements.
+ Local Open Scope string_scope.
+
+ Definition nameSuffix (n: nat): string :=
+ (nToHex (N.of_nat n)).
+
+ Coercion wordToString {n} (w: word n): string :=
+ "0x" ++ (nToHex (wordToN w)).
+
+ Coercion constToString {n} (c: Const n): string :=
+ match c with | constant _ _ w => wordToString w end.
+
+ Coercion regToString {n} (r: Reg n): string :=
+ match r with
+ | reg _ W32 n => "w" ++ (nameSuffix n)
+ | reg _ W64 n => "d" ++ (nameSuffix n)
+ end.
+
+ Coercion natToString (n: nat): string :=
+ "0x" ++ (nToHex (N.of_nat n)).
+
+ Coercion stackToString {n} (s: Stack n): string :=
+ match s with
+ | stack _ W32 n => "ws" ++ (nameSuffix n)
+ | stack _ W64 n => "ds" ++ (nameSuffix n)
+ end.
+
+ Coercion memToString {n m} (s: Mem n m): string :=
+ match s with
+ | mem _ _ W32 v => "wm" ++ (nameSuffix v)
+ | mem _ _ W64 v => "dm" ++ (nameSuffix v)
+ end.
+
+ Coercion stringToSome (x: string): option string := Some x.
+
+ Definition stackLocation {n} (s: Stack n): word 32 :=
+ combine (natToWord 8 n) (natToWord 24 n).
+
+ Definition assignmentToString (a: Assignment): option string :=
+ let f := fun x => if (Nat.eq_dec x 32) then "32" else "64" in
+ match a with
+ | ARegStack n r s => r ++ " = *(int" ++ f n ++ " *)" ++ s
+ | AStackReg n s r => "*(int" ++ f n ++ " *) " ++ s ++ " = " ++ r
+ | ARegMem n m r v i => r ++ " = " ++ "*(int" ++ f n ++ " *) (" ++ v ++ " + " ++ i ++ ")"
+ | AMemReg n m v i r => "*(int" ++ f n ++ " *) (" ++ v ++ " + " ++ i ++ ") = " ++ r
+ | ARegReg n a b => a ++ " = " ++ b
+ | AConstInt n r c => r ++ " = " ++ c
+ end.
+
+ Coercion intOpToString (b: IntOp): string :=
+ match b with
+ | Add => "+"
+ | Sub => "-"
+ | Xor => "^"
+ | And => "&"
+ | Or => "|"
+ end.
+
+ Coercion dualOpToString (b: DualOp): string :=
+ match b with
+ | Mult => "*"
+ end.
+
+ Coercion carryOpToString (b: CarryOp): string :=
+ match b with
+ | AddWithCarry => "+"
+ end.
+
+ Coercion rotOpToString (r: RotOp): string :=
+ match r with
+ | Shl => "<<"
+ | Shr => ">>"
+ end.
+
+ Definition operationToString (op: Operation): option string :=
+ let f := fun x => if (Nat.eq_dec x 32) then "32" else "64" in
+ match op with
+ | IOpConst n o r c =>
+ r ++ " " ++ o ++ "= " ++ c
+ | IOpReg n o a b =>
+ a ++ " " ++ o ++ "= " ++ b
+ | IOpMem n _ o a b i =>
+ a ++ " " ++ o ++ "= *(int" ++ (f n) ++ "* " ++ b ++ " + " ++ i ++ ")"
+ | IOpStack n o a b =>
+ a ++ " " ++ o ++ "= " ++ b
+ | DOp n o a b x =>
+ match x with
+ | Some r =>
+ "inline " ++ r ++ " " ++ a ++ " " ++ o ++ "= " ++ b
+ | None => a ++ " " ++ o ++ "= " ++ b
+ end
+ | COp n o a b =>
+ a ++ " " ++ o ++ "= " ++ b
+ | ROp n o r i =>
+ r ++ " " ++ o ++ "= " ++ i
+ end.
+
+ Definition testOpToString (t: TestOp): bool * string :=
+ match t with
+ | TEq => (true, "=")
+ | TLt => (true, "<")
+ | TGt => (true, ">")
+ | TLe => (false, ">")
+ | TGe => (false, "<")
+ end.
+
+ Definition conditionalToString (c: Conditional): string * string :=
+ match c with
+ | CTrue => ("=? 0", "=")
+ | CZero n r => ("=? " ++ r, "=")
+ | CReg n t a b =>
+ match (testOpToString t) with
+ | (true, s) =>
+ (s ++ "? " ++ a ++ " - " ++ b, s)
+ | (false, s) =>
+ (s ++ "? " ++ a ++ " - " ++ b, "!" ++ s)
+ end
+
+ | CConst n t a b =>
+ match (testOpToString t) with
+ | (true, s) =>
+ (s ++ "? " ++ a ++ " - " ++ b, s)
+ | (false, s) =>
+ (s ++ "? " ++ a ++ " - " ++ b, "!" ++ s)
+ end
+ end.
+
+ End Elements.
+
+ Section Parsing.
+ Definition convM {n m} (x: list (Mapping n)): list (Mapping m).
+ destruct (Nat.eq_dec n m); subst. exact x. exact [].
+ Defined.
+
+ Arguments regM [n] r.
+ Arguments stackM [n] s.
+ Arguments memM [n m] x i.
+ Arguments constM [n] x.
+
+ Fixpoint entries (width: nat) (prog: list QhasmStatement): list (Mapping width) :=
+ match prog with
+ | cons s next =>
+ match s with
+ | QAssign a =>
+ match a with
+ | ARegStack n r s => convM [regM r; stackM s]
+ | AStackReg n s r => convM [regM r; stackM s]
+ | ARegMem n m a b i => convM [regM a; memM b i]
+ | AMemReg n m a i b => convM [memM a i; regM b]
+ | ARegReg n a b => convM [regM a; regM b]
+ | AConstInt n r c => convM [regM r; constM c]
+ end
+ | QOp o =>
+ match o with
+ | IOpConst _ o a c => convM [regM a; constM c]
+ | IOpReg _ o a b => convM [regM a; regM b]
+ | IOpStack _ o a b => convM [regM a; stackM b]
+ | IOpMem _ _ o a b i => convM [regM a; memM b i]
+ | DOp _ o a b (Some x) => convM [regM a; regM b; regM x]
+ | DOp _ o a b None => convM [regM a; regM b]
+ | ROp _ o a i => convM [regM a]
+ | COp _ o a b => convM [regM a; regM b]
+ end
+ | QCond c _ =>
+ match c with
+ | CTrue => []
+ | CZero n r => convM [regM r]
+ | CReg n o a b => convM [regM a; regM b]
+ | CConst n o a c => convM [regM a; constM c]
+ end
+ | _ => []
+ end ++ (entries width next)
+ | nil => nil
+ end.
+
+ Definition flatMapOpt {A B} (lst: list A) (f: A -> option B): list B :=
+ fold_left
+ (fun lst a => match (f a) with | Some x => cons x lst | _ => lst end)
+ lst [].
+
+ Definition flatMapList {A B} (lst: list A) (f: A -> list B): list B :=
+ fold_left (fun lst a => lst ++ (f a)) lst [].
+
+ Fixpoint dedup {n} (l : list (Mapping n)) : list (Mapping n) :=
+ match l with
+ | [] => []
+ | x::xs =>
+ if in_dec EvalUtil.mapping_dec x xs
+ then dedup xs
+ else x::(dedup xs)
+ end.
+
+ Definition getRegNames (n: nat) (lst: list (Mapping n)): list nat :=
+ flatMapOpt (dedup lst) (fun e =>
+ match e with | regM (reg _ _ x) => Some x | _ => None end).
+
+ Definition getStackNames (n: nat) (lst: list (Mapping n)): list nat :=
+ flatMapOpt (dedup lst) (fun e =>
+ match e with | stackM (stack _ _ x) => Some x | _ => None end).
+
+ Definition getMemNames (n: nat) (lst: list (Mapping n)): list nat :=
+ flatMapOpt (dedup lst) (fun e =>
+ match e with | memM _ (mem _ _ _ x) _ => Some x | _ => None end).
+
+ Fixpoint getInputs' (n: nat) (prog: list QhasmStatement) (init: list (Mapping n)): list (Mapping n) :=
+ let f := fun rs => filter (fun x =>
+ negb (proj1_sig (bool_of_sumbool (in_dec EvalUtil.mapping_dec x init)))) rs in
+ let g := fun {w} p => (@convM w n (fst p), @convM w n (snd p)) in
+ match prog with
+ | [] => []
+ | cons p ps =>
+ let requiredCommaUsed := match p with
+ | QAssign a =>
+ match a with
+ | ARegStack n r s => g ([stackM s], [regM r; stackM s])
+ | AStackReg n s r => g ([regM r], [regM r; stackM s])
+ | ARegMem n m r x i => g ([memM x i], [regM r; memM x i])
+ | AMemReg n m x i r => g ([regM r], [regM r; memM x i])
+ | ARegReg n a b => g ([regM b], [regM a; regM b])
+ | AConstInt n r c => g ([], [regM r])
+ end
+ | QOp o =>
+ match o with
+ | IOpConst _ o a c => g ([regM a], [regM a])
+ | IOpReg _ o a b => g ([regM a], [regM a; regM b])
+ | IOpStack _ o a b => g ([regM a], [regM a; stackM b])
+ | IOpMem _ _ o a b i => g ([regM a], [regM a; memM b i])
+ | DOp _ o a b (Some x) => g ([regM a; regM b], [regM a; regM b; regM x])
+ | DOp _ o a b None => g ([regM a; regM b], [regM a; regM b])
+ | ROp _ o a i => g ([regM a], [regM a])
+ | COp _ o a b => g ([regM a], [regM a; regM b])
+ end
+ | QCond c _ =>
+ match c with
+ | CTrue => ([], [])
+ | CZero n r => g ([], [regM r])
+ | CReg n o a b => g ([], [regM a; regM b])
+ | CConst n o a c => g ([], [regM a])
+ end
+ | _ => ([], [])
+ end in match requiredCommaUsed with
+ | (r, u) => ((f r) ++ (getInputs' n ps ((f u) ++ init)))
+ end
+ end.
+
+ Definition getInputs (n: nat) (prog: list QhasmStatement) := getInputs' n prog [].
+
+ Definition mappingDeclaration {n} (x: Mapping n): option string :=
+ match x with
+ | regM (reg _ w x) =>
+ match w with
+ | W32 => Some ("int32 " ++ (reg w x))%string
+ | W64 => Some ("int64 " ++ (reg w x))%string
+ end
+
+ | stackM (stack _ w x) =>
+ match w with
+ | W32 => Some ("stack32 " ++ (stack w x))%string
+ | W64 => Some ("stack64 " ++ (stack w x))%string
+ end
+
+ | memM _ (mem _ m w x) _ =>
+ match w with
+ | W32 => Some ("stack32 " ++ (@mem _ m w x))%string
+ | W64 => Some ("stack64 " ++ (@mem _ m w x))%string
+ end
+
+ | _ => None
+ end.
+
+ Definition inputDeclaration {n} (x: Mapping n): option string :=
+ match x with
+ | regM r => Some ("input " ++ r)%string
+ | stackM s => Some ("input " ++ s)%string
+ | memM _ m i => Some ("input " ++ m)%string
+ | _ => None
+ end.
+
+ End Parsing.
+
+ (* Macroscopic Conversion Methods *)
+ Definition optionToList {A} (o: option A): list A :=
+ match o with
+ | Some a => [a]
+ | None => []
+ end.
+
+ Definition convertStatement (statement: QhasmStatement): list string :=
+ match statement with
+ | QAssign a => optionToList (assignmentToString a)
+ | QOp o => optionToList (operationToString o)
+ | QCond c l =>
+ match (conditionalToString c) with
+ | (s1, s2) =>
+ let s' := ("goto lbl" ++ l ++ " if " ++ s2)%string in
+ [s1; s']
+ end
+ | QLabel l => [("lbl" ++ l ++ ": ")%string]
+ | QCall l => [("push %eip+2")%string; ("goto" ++ l)%string]
+ | QRet => [("pop %eip")%string]
+ end.
+
+ Transparent Qhasm.Program QhasmString.Program.
+
+ Definition convertProgram x y (prog: Qhasm.Program x): option (QhasmString.Program y) :=
+ let decls := fun x => flatMapList (dedup (entries x prog))
+ (compose optionToList mappingDeclaration) in
+
+ let inputs := fun x => flatMapList (getInputs x prog)
+ (compose optionToList inputDeclaration) in
+
+ let stmts := (flatMapList prog convertStatement) in
+ let enter := [("enter prog")%string] in
+ let leave := [("leave")%string] in
+ let blank := [EmptyString] in
+ let newline := String (ascii_of_nat 10) EmptyString in
+
+ Some (fold_left (fun x y => (x ++ newline ++ y)%string)
+ (decls 32 ++ inputs 32 ++
+ decls 64 ++ inputs 64 ++ blank ++
+ enter ++ blank ++
+ stmts ++ blank ++
+ leave ++ blank) EmptyString).
+
+ Lemma convert_spec: forall pa pb a a' b b' prog prog',
+ convertProgram pa pb prog = Some prog' ->
+ convertState pa pb a = Some a' ->
+ convertState pa pb b = Some b' ->
+ QhasmString.evaluatesTo pb prog' a b <-> Qhasm.evaluatesTo pa prog a' b'.
+ Admitted.
+
+End StringConversion.
diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v
new file mode 100644
index 000000000..f8139bf92
--- /dev/null
+++ b/src/Assembly/Vectorize.v
@@ -0,0 +1,75 @@
+Require Export Bedrock.Word Bedrock.Nomega.
+Require Import NPeano NArith PArith Ndigits Compare_dec Arith.
+Require Import ProofIrrelevance Ring List.
+Require Import MultiBoundedWord.
+
+Section Vector.
+ Import ListNotations.
+
+ Definition vec T n := {x: list T | length x = n}.
+
+ Definition vget {n T} (x: vec T n) (i: {v: nat | (v < n)%nat}): T.
+ refine (
+ match (proj1_sig x) as x' return (proj1_sig x) = x' -> _ with
+ | [] => fun _ => _
+ | x0 :: xs => fun _ => nth (proj1_sig i) (proj1_sig x) x0
+ end eq_refl); abstract (
+ destruct x as [x xp], i as [i ip]; destruct x as [|x0 xs];
+ simpl in xp; subst; inversion _H; clear _H; omega).
+ Defined.
+
+ Lemma vget_spec: forall {T n} (x: vec T n) (i: {v: nat | (v < n)%nat}) (d: T),
+ vget x i = nth (proj1_sig i) (proj1_sig x) d.
+ Proof.
+ intros; destruct x as [x xp], i as [i ip];
+ destruct x as [|x0 xs]; induction i; unfold vget; simpl;
+ intuition; try (simpl in xp; subst; omega);
+ induction n; simpl in xp; try omega; clear IHi IHn.
+
+ apply nth_indep.
+ assert (length xs = n) by omega; subst.
+ omega.
+ Qed.
+
+ Definition vec0 {T} : vec T 0.
+ refine (exist _ [] _); abstract intuition.
+ Defined.
+
+ Lemma lift0: forall {T n} (x: T), vec (word n) 0 -> T.
+ intros; refine x.
+ Defined.
+
+ Lemma liftS: forall {T n m} (f: vec (word n) m -> word n -> T),
+ (vec (word n) (S m) -> T).
+ Proof.
+ intros T n m f v; destruct v as [v p]; induction m, v;
+ try (abstract (inversion p)).
+
+ - refine (f (exist _ [] _) w); abstract intuition.
+ - refine (f (exist _ v _) w); abstract intuition.
+ Defined.
+
+ Lemma vecToList: forall T n m (f: vec (word n) m -> T),
+ (list (word n) -> option T).
+ Proof.
+ intros T n m f x; destruct (Nat.eq_dec (length x) m).
+
+ - refine (Some (f (exist _ x _))); abstract intuition.
+ - refine None.
+ Defined.
+End Vector.
+
+Ltac vectorize :=
+ repeat match goal with
+ | [ |- context[?a - 1] ] =>
+ let c := eval simpl in (a - 1) in
+ replace (a - 1) with c by omega
+ | [ |- vec (word ?n) O -> ?T] => apply (@lift0 T n)
+ | [ |- vec (word ?n) ?m -> ?T] => apply (@liftS T n (m - 1))
+ end.
+
+Section Examples.
+ Lemma vectorize_example: (vec (word 32) 2 -> word 32).
+ vectorize; refine (@wplus 32).
+ Qed.
+End Examples.
diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v
new file mode 100644
index 000000000..e5ad3f066
--- /dev/null
+++ b/src/Assembly/Wordize.v
@@ -0,0 +1,507 @@
+
+Require Export Bedrock.Word Bedrock.Nomega.
+Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec Compare_dec.
+Require Import FunctionalExtensionality ProofIrrelevance.
+Require Import QhasmUtil QhasmEvalCommon.
+
+Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add
+ Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N.
+
+Open Scope nword_scope.
+
+Section WordizeUtil.
+ Lemma break_spec: forall (m n: nat) (x: word n) low high,
+ (low, high) = break m x
+ -> &x = (&high * Npow2 m + &low)%N.
+ Proof.
+ intros; unfold break in *; destruct (le_dec m n);
+ inversion H; subst; clear H; simpl.
+ Admitted.
+
+ Lemma mask_wand : forall (n: nat) (x: word n) m b,
+ (& (mask (N.to_nat m) x) < b)%N
+ -> (& (x ^& (@NToWord n (N.ones m))) < b)%N.
+ Proof.
+ Admitted.
+
+ Lemma convS_id: forall A x p, x = (@convS A A x p).
+ Proof.
+ intros; unfold convS; vm_compute.
+ replace p with (eq_refl A); intuition.
+ apply proof_irrelevance.
+ Qed.
+
+ Lemma word_param_eq: forall n m, word n = word m -> n = m.
+ Proof. (* TODO: How do we prove this *) Admitted.
+
+ Lemma word_conv_eq: forall {n m} (y: word m) p,
+ &y = &(@convS (word m) (word n) y p).
+ Proof.
+ intros.
+ revert p.
+ destruct (Nat.eq_dec n m).
+
+ - rewrite e; intros; apply f_equal; apply convS_id.
+
+ - intros; contradict n0.
+ apply word_param_eq; rewrite p; intuition.
+ Qed.
+
+ Lemma to_nat_lt: forall x b, (x < b)%N <-> (N.to_nat x < N.to_nat b)%nat.
+ Proof. (* via Nat2N.inj_compare *) Admitted.
+
+ Lemma of_nat_lt: forall x b, (x < b)%nat <-> (N.of_nat x < N.of_nat b)%N.
+ Proof. (* via N2Nat.inj_compare *) Admitted.
+
+ Lemma Npow2_spec : forall n, Npow2 n = N.pow 2 (N.of_nat n).
+ Proof. (* by induction and omega *) Admitted.
+
+ Lemma NToWord_wordToN: forall sz x, NToWord sz (wordToN x) = x.
+ Proof.
+ intros.
+ rewrite NToWord_nat.
+ rewrite wordToN_nat.
+ rewrite Nat2N.id.
+ rewrite natToWord_wordToNat.
+ intuition.
+ Qed.
+
+ Lemma wordToN_NToWord: forall sz x, (x < Npow2 sz)%N -> wordToN (NToWord sz x) = x.
+ Proof.
+ intros.
+ rewrite NToWord_nat.
+ rewrite wordToN_nat.
+ rewrite <- (N2Nat.id x).
+ apply Nat2N.inj_iff.
+ rewrite Nat2N.id.
+ apply natToWord_inj with (sz:=sz);
+ try rewrite natToWord_wordToNat;
+ intuition.
+
+ - apply wordToNat_bound.
+ - rewrite <- Npow2_nat; apply to_nat_lt; assumption.
+ Qed.
+
+ Lemma word_size_bound : forall {n} (w: word n), (&w < Npow2 n)%N.
+ Proof.
+ intros; pose proof (wordToNat_bound w) as B;
+ rewrite of_nat_lt in B;
+ rewrite <- Npow2_nat in B;
+ rewrite N2Nat.id in B;
+ rewrite <- wordToN_nat in B;
+ assumption.
+ Qed.
+
+ Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N.
+ Proof.
+ intros; induction x.
+
+ - simpl; apply N.lt_1_r; intuition.
+
+ - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition.
+ apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0.
+
+ + intuition; inversion H.
+
+ + apply N.neq_0_lt_0 in IHx; intuition.
+ Qed.
+
+ Lemma natToWord_convS: forall {n m} (x: word n) p,
+ & x = & @convS (word n) (word m) x p.
+ Proof. admit. Qed.
+
+ Lemma natToWord_combine: forall {n} (x: word n) k,
+ & x = & combine x (wzero k).
+ Proof. admit. Qed.
+
+ Lemma natToWord_split1: forall {n} (x: word n) p,
+ & x = & split1 n 0 (convS x p).
+ Proof. admit. Qed.
+
+ Lemma extend_bound: forall k n (p: (k <= n)%nat) (w: word k),
+ (& (extend p w) < Npow2 k)%N.
+ Proof.
+ intros.
+ assert (n = k + (n - k)) by abstract omega.
+ replace (& (extend p w)) with (& w); try apply word_size_bound.
+ unfold extend.
+ rewrite <- word_conv_eq.
+ unfold zext.
+ clear; revert w; induction (n - k).
+
+ - intros.
+ assert (word k = word (k + 0)) as Z by intuition.
+ replace w with (split1 k 0 (convS w Z)).
+ replace (wzero 0) with (split2 k 0 (convS w Z)).
+ rewrite <- natToWord_split1 with (p := Z).
+ rewrite combine_split.
+ apply natToWord_convS.
+
+ + admit.
+ + admit.
+
+ - intros; rewrite <- natToWord_combine; intuition.
+ Qed.
+
+ Lemma Npow2_split: forall a b,
+ (Npow2 (a + b) = (Npow2 a) * (Npow2 b))%N.
+ Proof.
+ intros; revert a.
+ induction b.
+
+ - intros; simpl; replace (a + 0) with a; nomega.
+
+ - intros.
+ replace (a + S b) with (S a + b) by intuition.
+ rewrite (IHb (S a)); simpl; clear IHb.
+ induction (Npow2 a), (Npow2 b); simpl; intuition.
+ rewrite Pos.mul_xO_r; intuition.
+ Qed.
+
+ Lemma Npow2_ignore: forall {n} (x: word n),
+ x = NToWord _ (& x + Npow2 n).
+ Proof. intros. Admitted.
+
+End WordizeUtil.
+
+(** Wordization Lemmas **)
+
+Section Wordization.
+
+ Lemma wordize_plus': forall {n} (x y: word n) (b: N),
+ (b <= Npow2 n)%N
+ -> (&x < b)%N
+ -> (&y < (Npow2 n - b))%N
+ -> (&x + &y)%N = & (x ^+ y).
+ Proof.
+ intros.
+ unfold wplus, wordBin.
+ rewrite wordToN_NToWord; intuition.
+ apply (N.lt_le_trans _ (b + &y)%N _).
+
+ - apply N.add_lt_le_mono; try assumption; intuition.
+
+ - replace (Npow2 n) with (b + Npow2 n - b)%N by nomega.
+ replace (b + Npow2 n - b)%N with (b + (Npow2 n - b))%N by (
+ replace (b + (Npow2 n - b))%N with ((Npow2 n - b) + b)%N by nomega;
+ rewrite (N.sub_add b (Npow2 n)) by assumption;
+ nomega).
+
+ apply N.add_le_mono_l; try nomega.
+ apply N.lt_le_incl; assumption.
+ Qed.
+
+ Lemma wordize_plus: forall {n} (x y: word n),
+ if (overflows n (&x + &y)%N)
+ then (&x + &y)%N = (& (x ^+ y) + Npow2 n)%N
+ else (&x + &y)%N = & (x ^+ y).
+ Proof. Admitted.
+
+ Lemma wordize_awc: forall {n} (x y: word n) (c: bool),
+ if (overflows n (&x + &y + (if c then 1 else 0))%N)
+ then (&x + &y + (if c then 1 else 0))%N = (&(addWithCarry x y c) + Npow2 n)%N
+ else (&x + &y + (if c then 1 else 0))%N = &(addWithCarry x y c).
+ Proof. Admitted.
+
+ Lemma wordize_mult': forall {n} (x y: word n) (b: N),
+ (1 < n)%nat -> (0 < b)%N
+ -> (&x < b)%N
+ -> (&y < (Npow2 n) / b)%N
+ -> (&x * &y)%N = & (x ^* y).
+ Proof.
+ intros; unfold wmult, wordBin.
+ rewrite wordToN_NToWord; intuition.
+ apply (N.lt_le_trans _ (b * ((Npow2 n) / b))%N _).
+
+ - apply N.mul_lt_mono; assumption.
+
+ - apply N.mul_div_le; nomega.
+ Qed.
+
+ Lemma wordize_mult: forall {n} (x y: word n) (b: N),
+ (&x * &y)%N = (&(x ^* y) +
+ &((EvalUtil.highBits (n/2) x) ^* (EvalUtil.highBits (n/2) y)) * Npow2 n)%N.
+ Proof. intros. Admitted.
+
+ Lemma wordize_and: forall {n} (x y: word n),
+ N.land (&x) (&y) = & (x ^& y).
+ Proof.
+ intros; pose proof (Npow2_gt0 n).
+ pose proof (word_size_bound x).
+ pose proof (word_size_bound y).
+
+ induction n.
+
+ - rewrite (shatter_word_0 x) in *.
+ rewrite (shatter_word_0 y) in *.
+ simpl; intuition.
+
+ - rewrite (shatter_word x) in *.
+ rewrite (shatter_word y) in *.
+ induction (whd x), (whd y).
+
+ + admit.
+ + admit.
+ + admit.
+ + admit.
+ Qed.
+
+ Lemma wordize_shiftr: forall {n} (x: word n) (k: nat),
+ (N.shiftr_nat (&x) k) = & (shiftr x k).
+ Proof.
+ intros.
+
+ admit.
+ Qed.
+
+End Wordization.
+
+Section Bounds.
+
+ Theorem constant_bound_N : forall {n} (k: word n),
+ (& k < & k + 1)%N.
+ Proof. intros; nomega. Qed.
+
+ Theorem constant_bound_nat : forall (n k: nat),
+ (N.of_nat k < Npow2 n)%N
+ -> (& (@natToWord n k) < (N.of_nat k) + 1)%N.
+ Proof.
+ intros.
+ rewrite wordToN_nat.
+ rewrite wordToNat_natToWord_idempotent;
+ try assumption; nomega.
+ Qed.
+
+ Lemma let_bound : forall {n} (x: word n) (f: word n -> word n) xb fb,
+ (& x < xb)%N
+ -> (forall x', & x' < xb -> & (f x') < fb)%N
+ -> ((let k := x in &(f k)) < fb)%N.
+ Proof. intros; eauto. Qed.
+
+ Definition Nlt_dec (x y: N): {(x < y)%N} + {(x >= y)%N}.
+ refine (
+ let c := N.compare x y in
+ match c as c' return c = c' -> _ with
+ | Lt => fun _ => left _
+ | _ => fun _ => right _
+ end eq_refl);
+ abstract (unfold c in *; try first [
+ apply N.compare_eq_iff in _H
+ | apply N.compare_lt_iff in _H
+ | pose proof (N.compare_antisym x y) as _H0;
+ rewrite _H in _H0; simpl in _H0;
+ apply N.compare_lt_iff in _H0 ]; nomega).
+ Defined.
+
+ Theorem wplus_bound : forall {n} (w1 w2 : word n) b1 b2,
+ (&w1 < b1)%N
+ -> (&w2 < b2)%N
+ -> (&(w1 ^+ w2) < b1 + b2)%N.
+ Proof.
+ intros.
+
+ destruct (Nlt_dec (b1 + b2)%N (Npow2 n));
+ rewrite <- wordize_plus' with (b := b1);
+ try apply N.add_lt_mono;
+ try assumption.
+
+ (* A couple inequality subgoals *)
+ Admitted.
+
+ Theorem wmult_bound : forall {n} (w1 w2 : word n) b1 b2,
+ (1 < n)%nat
+ -> (&w1 < b1)%N
+ -> (&w2 < b2)%N
+ -> (&(w1 ^* w2) < b1 * b2)%N.
+ Proof.
+ intros.
+ destruct (Nlt_dec (b1 * b2)%N (Npow2 n));
+ rewrite <- wordize_mult' with (b := b1);
+ try apply N.mul_lt_mono;
+ try assumption;
+ try nomega.
+
+ (* A couple inequality subgoals *)
+ Admitted.
+
+ Theorem shiftr_bound : forall {n} (w : word n) b bits,
+ (&w < b)%N
+ -> (&(shiftr w bits) < N.succ (N.shiftr_nat b bits))%N.
+ Proof.
+ intros.
+ assert (& shiftr w bits <= N.shiftr_nat b bits)%N. {
+ rewrite <- wordize_shiftr.
+ induction bits; unfold N.shiftr_nat in *; simpl; intuition.
+
+ - unfold N.le, N.lt in *; rewrite H; intuition; inversion H0.
+
+ - revert IHbits;
+ generalize (nat_iter bits N.div2 (& w)),
+ (nat_iter bits N.div2 b);
+ clear; intros x y H.
+
+ admit. (* Monotonicity of N.div2 *)
+ }
+
+ apply N.le_lteq in H0; destruct H0; nomega.
+ Qed.
+
+ Theorem mask_bound : forall {n} (w : word n) m,
+ (n > 1)%nat ->
+ (&(mask m w) < Npow2 m)%N.
+ Proof.
+ intros.
+ unfold mask in *; destruct (le_dec m n); simpl;
+ try apply extend_bound.
+
+ pose proof (word_size_bound w).
+ apply (N.le_lt_trans _ (Npow2 n) _).
+
+ - unfold N.le, N.lt in *; rewrite H0; intuition; inversion H1.
+
+ - clear H H0.
+ replace m with ((m - n) + n) by nomega.
+ replace (Npow2 n) with (1 * (Npow2 n))%N
+ by (rewrite N.mul_comm; nomega).
+ rewrite Npow2_split.
+ apply N.mul_lt_mono_pos_r.
+
+ + apply Npow2_gt0.
+
+ + assert (0 < m - n)%nat by omega.
+ induction (m - n); try inversion H; try abstract (
+ simpl; replace 2 with (S 1) by omega;
+ apply N.lt_1_2).
+
+ assert (0 < n1)%nat as Z by omega; apply IHn1 in Z.
+ apply (N.le_lt_trans _ (Npow2 n1) _).
+
+ * admit.
+ * admit.
+ Qed.
+
+ Theorem mask_update_bound : forall {n} (w : word n) b m,
+ (n > 1)%nat
+ -> (&w < b)%N
+ -> (&(mask m w) < (N.min b (Npow2 m)))%N.
+ Proof.
+ intros; unfold mask, N.min;
+ destruct (le_dec m n),
+ (N.compare b (Npow2 m));
+ simpl; try assumption.
+
+ Admitted.
+
+End Bounds.
+
+(** Wordization Tactics **)
+
+Ltac wordize_ast :=
+ repeat match goal with
+ | [ H: (& ?x < ?b)%N |- context[((& ?x) + (& ?y))%N] ] => rewrite (wordize_plus' x y b)
+ | [ H: (& ?x < ?b)%N |- context[((& ?x) * (& ?y))%N] ] => rewrite (wordize_mult' x y b)
+ | [ |- context[N.land (& ?x) (& ?y)] ] => rewrite (wordize_and x y)
+ | [ |- context[N.shiftr (& ?x) ?k] ] => rewrite (wordize_shiftr x k)
+ | [ |- (_ < _ / _)%N ] => unfold N.div; simpl
+ | [ |- context[Npow2 _] ] => simpl
+ | [ |- (?x < ?c)%N ] => assumption
+ | [ |- _ = _ ] => reflexivity
+ end.
+
+Ltac lt_crush := try abstract (clear; vm_compute; intuition).
+
+(** Bounding Tactics **)
+
+Ltac multi_apply0 A L := pose proof (L A).
+
+Ltac multi_apply1 A L :=
+ match goal with
+ | [ H: A < ?b |- _] => pose proof (L A b H)
+ end.
+
+Ltac multi_apply2 A B L :=
+ match goal with
+ | [ H1: A < ?b1, H2: B < ?b2 |- _] => pose proof (L A B b1 b2 H1 H2)
+ end.
+
+Ltac multi_recurse n T :=
+ match goal with
+ | [ H: (T < _)%N |- _] => idtac
+ | _ =>
+ is_var T;
+ let T' := (eval cbv delta [T] in T) in multi_recurse n T';
+ match goal with
+ | [ H : T' < ?x |- _ ] =>
+ pose proof (H : T < x)
+ end
+
+ | _ =>
+ match T with
+ | ?W1 ^+ ?W2 =>
+ multi_recurse n W1; multi_recurse n W2;
+ multi_apply2 W1 W2 (@wplus_bound n)
+
+ | ?W1 ^* ?W2 =>
+ multi_recurse n W1; multi_recurse n W2;
+ multi_apply2 W1 W2 (@wmult_bound n)
+
+ | mask ?m ?w =>
+ multi_recurse n w;
+ multi_apply1 w (fun b => @mask_update_bound n w b)
+
+ | mask ?m ?w =>
+ multi_recurse n w;
+ pose proof (@mask_bound n w m)
+
+ | ?x ^& (@NToWord _ (N.ones ?m)) =>
+ multi_recurse n (mask (N.to_nat m) x);
+ match goal with
+ | [ H: (& (mask (N.to_nat m) x) < ?b)%N |- _] =>
+ pose proof (@mask_wand n x m b H)
+ end
+
+ | shiftr ?w ?bits =>
+ multi_recurse n w;
+ match goal with
+ | [ H: (w < ?b)%N |- _] =>
+ pose proof (@shiftr_bound n w b bits H)
+ end
+
+ | NToWord _ ?k => pose proof (@constant_bound_N n k)
+ | natToWord _ ?k => pose proof (@constant_bound_nat n k)
+ | _ => pose proof (@word_size_bound n T)
+ end
+ end.
+
+Lemma unwrap_let: forall {n} (y: word n) (f: word n -> word n) (b: N),
+ (&(let x := y in f x) < b)%N <-> let x := y in (&(f x) < b)%N.
+Proof. intuition. Qed.
+
+Ltac multi_bound n :=
+ match goal with
+ | [|- let A := ?B in _] =>
+ multi_recurse n B; intro; multi_bound n
+ | [|- ((let A := _ in _) < _)%N] =>
+ apply unwrap_let; multi_bound n
+ | [|- (?W < _)%N ] =>
+ multi_recurse n W
+ end.
+
+(** Examples **)
+
+Module WordizationExamples.
+
+ Lemma wordize_example0: forall (x y z: word 16),
+ (wordToN x < 10)%N ->
+ (wordToN y < 10)%N ->
+ (wordToN z < 10)%N ->
+ & (x ^* y) = (&x * &y)%N.
+ Proof.
+ intros.
+ wordize_ast; lt_crush.
+ transitivity 10%N; try assumption; lt_crush.
+ Qed.
+
+End WordizationExamples.
+
+Close Scope nword_scope.
diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v
new file mode 100644
index 000000000..73eb17549
--- /dev/null
+++ b/src/Galois/GaloisField.v
@@ -0,0 +1,259 @@
+Require Import BinInt BinNat ZArith Znumtheory.
+Require Import BoolEq Field_theory.
+Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
+Require Import Crypto.Tactics.VerdiTactics.
+
+(* This file is for the actual field tactics and some specialized
+ * morphisms that help field operate.
+ *
+ * When you want a Galois Field, this is the /only module/ you
+ * should import, because it automatically pulls in everything
+ * from Galois and the Modulus.
+ *)
+Module GaloisField (M: Modulus).
+ Module G := Galois M.
+ Module T := GaloisTheory M.
+ Export M G T.
+
+ (* Define a "ring morphism" between GF and Z, i.e. an equivalence
+ * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
+ *
+ * Doing this allows us to do our coefficient manipulations in Z
+ * rather than GF, because we know it's equivalent to inject the
+ * result afterward.
+ *)
+ Lemma GFring_morph:
+ ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq
+ 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+ inject.
+ Proof.
+ constructor; intros; try galois;
+ try (apply gf_eq; simpl; intuition).
+
+ apply Zmod_small; destruct modulus; simpl;
+ apply prime_ge_2 in p; intuition.
+
+ replace (- (x mod modulus)) with (0 - (x mod modulus));
+ try rewrite Zminus_mod_idemp_r; trivial.
+
+ replace x with y; intuition.
+ symmetry; apply Zeq_bool_eq; trivial.
+ Qed.
+
+ (* Redefine our division theory under the ring morphism *)
+ Lemma GFmorph_div_theory:
+ div_theory eq Zplus Zmult inject Z.quotrem.
+ Proof.
+ constructor; intros; intuition.
+ replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
+ try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+
+ eq_remove_proofs; demod;
+ rewrite <- (Z.quot_rem' a b);
+ destruct a; simpl; trivial.
+ Qed.
+
+ (* Some simple utility lemmas *)
+ Lemma injectZeroIsGFZero :
+ GFzero = inject 0.
+ Proof.
+ apply gf_eq; simpl; trivial.
+ Qed.
+
+ Lemma injectOneIsGFOne :
+ GFone = inject 1.
+ Proof.
+ apply gf_eq; simpl; intuition.
+ symmetry; apply Zmod_small; destruct modulus; simpl;
+ apply prime_ge_2 in p; intuition.
+ Qed.
+
+ Lemma divOneIsX :
+ forall (x: GF), (x / 1)%GF = x.
+ Proof.
+ intros; unfold GFdiv.
+
+ replace (GFinv 1)%GF with 1%GF by (
+ replace (GFinv 1)%GF with (GFinv 1 * 1)%GF by ring;
+ rewrite GF_multiplicative_inverse; intuition).
+
+ ring.
+ Qed.
+
+ Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
+ Proof.
+ intuition; solve_by_inversion.
+ Qed.
+
+ (* Change all GFones to (inject 1) and GFzeros to (inject 0) so that
+ * we can use our ring morphism to simplify them
+ *)
+ Ltac GFpreprocess :=
+ repeat rewrite injectZeroIsGFZero;
+ repeat rewrite injectOneIsGFOne.
+
+ (* Split up the equation (because field likes /\, then
+ * change back all of our GFones and GFzeros.
+ *
+ * TODO (adamc): what causes it to generate these subproofs?
+ *)
+ Ltac GFpostprocess :=
+ repeat split;
+
+ repeat match goal with
+ | [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
+ replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
+ end;
+
+ repeat rewrite <- injectZeroIsGFZero;
+ repeat rewrite <- injectOneIsGFOne;
+ repeat rewrite divOneIsX.
+
+ (* Tactic to passively convert from GF to Z in special circumstances *)
+ Ltac GFconstant t :=
+ match t with
+ | inject ?x => x
+ | _ => NotConstant
+ end.
+
+ (* Add our ring with all the fixin's *)
+ Add Ring GFring_Z : GFring_theory
+ (morphism GFring_morph,
+ constants [GFconstant],
+ div GFmorph_div_theory,
+ power_tac GFpower_theory [GFexp_tac]).
+
+ (* Add our field with all the fixin's *)
+ Add Field GFfield_Z : GFfield_theory
+ (morphism GFring_morph,
+ preprocess [GFpreprocess],
+ postprocess [GFpostprocess],
+ constants [GFconstant],
+ div GFmorph_div_theory,
+ power_tac GFpower_theory [GFexp_tac]).
+
+ Local Open Scope GF_scope.
+
+ Lemma GF_mul_eq : forall x y z, z <> 0 -> x * z = y * z -> x = y.
+ Proof.
+ intros ? ? ? z_nonzero mul_z_eq.
+ replace x with (x * 1) by field.
+ rewrite <- (GF_multiplicative_inverse z_nonzero).
+ replace (x * (GFinv z * z)) with ((x * z) * GFinv z) by ring.
+ rewrite mul_z_eq.
+ replace (y * z * GFinv z) with (y * (GFinv z * z)) by ring.
+ rewrite GF_multiplicative_inverse; auto; field.
+ Qed.
+
+ Lemma GF_mul_0_l : forall x, 0 * x = 0.
+ Proof.
+ intros; field.
+ Qed.
+
+ Lemma GF_mul_0_r : forall x, x * 0 = 0.
+ Proof.
+ intros; field.
+ Qed.
+
+ Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
+ intros.
+ assert (H := Z.eq_dec (inject x) (inject y)).
+
+ destruct H.
+
+ - left; galois; intuition.
+
+ - right; intuition.
+ rewrite H in n.
+ assert (y = y); intuition.
+ Qed.
+
+ Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
+ intros; intuition; subst.
+ assert (0 * b = 0) by field; intuition.
+ Qed.
+
+ Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
+ intros; intuition; subst.
+ assert (a * 0 = 0) by field; intuition.
+ Qed.
+
+ Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
+ intros.
+ assert (Z := GF_eq_dec a 0); destruct Z.
+
+ - left; intuition.
+
+ - assert (a * b / a = 0) by
+ ( rewrite H; field; intuition ).
+
+ field_simplify in H0.
+ replace (b/1) with b in H0 by (field; intuition).
+ right; intuition.
+ apply n in H0; intuition.
+ Qed.
+
+ Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
+ intros; intuition; subst.
+ apply mul_zero_why in H1.
+ destruct H1; subst; intuition.
+ Qed.
+ Hint Resolve mul_nonzero_nonzero.
+
+ Lemma GFexp_distr_mul : forall x y z, (0 <= z)%N ->
+ (x ^ z) * (y ^ z) = (x * y) ^ z.
+ Proof.
+ intros.
+ replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
+ apply natlike_ind with (x := Z.of_N z); simpl; [ field | |
+ replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
+ intros z' z'_nonneg IHz'.
+ rewrite Z2N.inj_succ by auto.
+ rewrite (GFexp_pred x) by apply N.neq_succ_0.
+ rewrite (GFexp_pred y) by apply N.neq_succ_0.
+ rewrite (GFexp_pred (x * y)) by apply N.neq_succ_0.
+ rewrite N.pred_succ.
+ rewrite <- IHz'.
+ field.
+ Qed.
+
+ Lemma GF_square_mul : forall x y z, (y <> 0) ->
+ x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
+ Proof.
+ intros ? ? ? y_nonzero A.
+ exists (x / y).
+ assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div. {
+ unfold GFdiv, GFexp, GFexp'.
+ replace (GFinv (y * y)) with (GFinv y * GFinv y); try ring.
+ unfold GFinv.
+ destruct (N.eq_dec (N.pred (totientToN totient)) 0) as [ eq_zero | neq_zero ];
+ [ rewrite eq_zero | rewrite GFexp_distr_mul ]; try field.
+ simpl.
+ do 2 rewrite <- Z2N.inj_pred.
+ replace 0%N with (Z.to_N 0%Z) by auto.
+ apply Z2N.inj_le; modulus_bound.
+ }
+ assert (y ^ 2 <> 0) as y2_nonzero by (apply mul_nonzero_nonzero; auto).
+ rewrite (GF_mul_eq _ z (y ^ 2)); auto.
+ unfold GFdiv.
+ rewrite <- A.
+ field; auto.
+ Qed.
+
+ Lemma sqrt_solutions : forall x y, y ^ 2 = x ^ 2 -> y = x \/ y = GFopp x.
+ Proof.
+ intros.
+ (* TODO(jadep) *)
+ Admitted.
+
+ Lemma GFopp_swap : forall x y, GFopp x = y <-> x = GFopp y.
+ Proof.
+ split; intro; subst; field.
+ Qed.
+
+ Lemma GFopp_involutive : forall x, GFopp (GFopp x) = x.
+ Proof.
+ intros; field.
+ Qed.
+
+End GaloisField.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 16:01:03 +0000