From 0fca6c1db266e9d65953a655d9bceb51ea2b76cf Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Thu, 26 May 2016 12:01:08 -0400 Subject: Major language refactoring to support Memory and AddWithCarry --- src/Assembly/AlmostConversion.v | 2 +- src/Assembly/PseudoMedialConversion.v | 10 - src/Assembly/QhasmCommon.v | 182 ++++++------ src/Assembly/QhasmEvalCommon.v | 191 ++++++------ src/Assembly/QhasmUtil.v | 93 +++--- src/Assembly/State.v | 526 +++++++++++++++++----------------- src/Assembly/StringConversion.v | 30 -- 7 files changed, 500 insertions(+), 534 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v index 6d2fa1b50..339a36bbc 100644 --- a/src/Assembly/AlmostConversion.v +++ b/src/Assembly/AlmostConversion.v @@ -17,7 +17,7 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm. | AOp a => [ QOp a ] | ACond c a b => let tru := N.to_nat (N.shiftl 1 label0) in - let finish := S tru in + let finish := S tru [QJmp c tru] ++ (almostToQhasm' b label1) ++ [QJmp TestTrue finish] ++ diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v index 5e671775c..79653136c 100644 --- a/src/Assembly/PseudoMedialConversion.v +++ b/src/Assembly/PseudoMedialConversion.v @@ -12,11 +12,6 @@ Module PseudoMedialConversion (Arch: PseudoMachine). Module P := Pseudo Arch. Module M := Medial Arch. - Inductive Mapping (n: nat) := - | regM: forall (r: IReg n) (v: nat), v = getIRegIndex r -> Mapping n - | stackM: forall (r: Stack n) (v: nat), v = getStackIndex r -> Mapping n - | constM: forall (r: IConst n) (v: nat), v = getIConstValue r -> Mapping n. - Definition wordToM {n: nat} {spec: ISize n} (w: word n): Mapping n. destruct spec; first [ refine (@constM 32 (constInt32 w) (wordToNat w) _) @@ -88,11 +83,6 @@ Module PseudoMedialConversion (Arch: PseudoMachine). then Some res else None. - 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). - Fixpoint range (start len: nat): list nat := match len with | O => [] diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 5e2077c5a..fe6746382 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -1,72 +1,79 @@ Require Export String List NPeano NArith. Require Export Bedrock.Word. -(* A formalization of x86 qhasm *) +(* Utilities *) Definition Label := nat. + Definition Index (limit: nat) := {x: nat | (x < limit)%nat}. +Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. -(* Sugar and Tactics *) +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. -Notation "'always' A" := (fun _ => A) (at level 90) : state_scope. -Notation "'cast' e" := (convert e _) (at level 20) : state_scope. -Notation "'lift' e" := (exist _ e _) (at level 20) : state_scope. -Notation "'contra'" := (False_rec _ _) : state_scope. - -Obligation Tactic := abstract intuition. - (* Asm Types *) -Inductive ISize: nat -> Type := - | I32: ISize 32 - | I64: ISize 64. +Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64. -Inductive IConst: nat -> Type := - | constInt32: word 32 -> IConst 32 - | constInt64: word 64 -> IConst 64. +(* A constant value *) +Inductive Const: nat -> Type := + | const: forall {n}, Width n -> word n -> Const n. -Inductive IReg: nat -> Type := - | regInt32: nat -> IReg 32 - | regInt64: nat -> IReg 64. +(* 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 := - | stack32: nat -> Stack 32 - | stack64: nat -> Stack 64 - | stack128: nat -> Stack 128. + | stack: forall {n}, Width n -> nat -> Stack n. -Definition CarryState := option bool. +(* 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 := - | ARegStackInt: forall n, IReg n -> Stack n -> Assignment - | AStackRegInt: forall n, Stack n -> IReg n -> Assignment - | ARegRegInt: forall n, IReg n -> IReg n -> Assignment - | AConstInt: forall n, IReg n -> IConst n -> Assignment - | AIndex: forall n m, IReg n -> Stack m -> Index (m/n)%nat -> Assignment - | APtr: forall n, IReg 32 -> Stack n -> Assignment. -Hint Constructors Assignment. +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 := - | IPlus: IntOp | IMinus: IntOp - | IXor: IntOp | IAnd: IntOp | IOr: IntOp. + | Add: IntOp | Sub: IntOp + | Xor: IntOp | And: IntOp + | Or: IntOp. -Inductive DualOp := - | IMult: DualOp. +Inductive CarryOp := | AddWithCarry: CarryOp. -Inductive RotOp := - | Shl: RotOp | Shr: RotOp. +Inductive DualOp := | Mult: DualOp. -Inductive Operation := - | IOpConst: forall n, IntOp -> IReg n -> IConst n -> Operation - | IOpReg: forall n, IntOp -> IReg n -> IReg n -> Operation - | DOpReg: forall n, DualOp -> IReg n -> IReg n -> option (IReg n) -> Operation - | OpRot: forall n, RotOp -> IReg n -> Index n -> Operation. +Inductive RotOp := | Shl: RotOp | Shr: RotOp. -Hint Constructors Operation. +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 + | 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 *) @@ -75,50 +82,47 @@ Inductive TestOp := | TGt: TestOp | TGe: TestOp. Inductive Conditional := - | TestTrue: Conditional - | TestFalse: Conditional - | TestInt: forall n, TestOp -> IReg n -> IReg n -> Conditional. - -Hint Constructors Conditional. - -(* Reg, Stack, Const Utilities *) - -Definition getIRegWords {n} (x: IReg n) := - match x with - | regInt32 loc => 1 - | regInt64 loc => 2 - end. - -Definition getStackWords {n} (x: Stack n) := - match x with - | stack32 loc => 1 - | stack64 loc => 2 - | stack128 loc => 4 - end. - -Definition getIConstValue {n} (x: IConst n): nat := - match x with - | constInt32 v => wordToNat v - | constInt64 v => wordToNat v - end. - -Definition getIRegIndex {n} (x: IReg n): nat := - match x with - | regInt32 loc => loc - | regInt64 loc => loc - end. - -Definition getStackIndex {n} (x: Stack n): nat := - match x with - | stack32 loc => loc - | stack64 loc => loc - | stack128 loc => loc - end. - -(* For register allocation checking *) -Definition intRegCount (base: nat): nat := - match base with - | 32 => 7 - | 64 => 8 - | _ => 0 - end. + | 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), 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 | @const n _ v => v end. + +Definition constValueN {n} (x: Const n): nat := + match x with | @const 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 index b6261d1c6..ea39a04ac 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -22,112 +22,123 @@ Definition evalTest {n} (o: TestOp) (a b: word n): bool := Definition evalCond (c: Conditional) (state: State): option bool := match c with - | TestTrue => Some true - | TestFalse => Some false - | TestInt n t a b => - match (getIntReg a state) with - | Some va => - match (getIntReg b state) with - | Some vb => Some (evalTest t va vb) - | _ => None - end - | _ => None - end + | 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 evalIOp {b} (io: IntOp) (x y: word b) := +Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool := match io with - | IPlus => wplus x y - | IMinus => wminus x y - | IXor => wxor x y - | IAnd => wand x y - | IOr => wor x y + | Add => + let v := (wordToN x + wordToN y)%N in + let c := (N.compare v (Npow2 b)) in + + match c as c' return c' = c -> _ with + | Lt => fun _ => (NToWord b v, Some false) + | _ => 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 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) +Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool := + match io with + | AddWidthCarry => + let v := (wordToN x + wordToN y + (if c then 1%N else 0%N))%N in + let c := (N.compare v (Npow2 b)) in + + match c as c' return c' = c -> _ with + | Lt => fun _ => (NToWord b v, false) + | _ => fun _ => (NToWord b v, true) + end eq_refl end. Definition evalDualOp {b} (duo: DualOp) (x y: word b) := match duo with - | IMult => - let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in + | Mult => + let v := (wordToN x * wordToN y)%N in + let wres := NToWord (b + b) v in (split1 b b wres, split2 b b wres) end. -Definition evalOperation (o: Operation) (state: State): option State := - let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) => - match (xo, yo) with - | (Some x, Some y) => f x y - | _ => None - end in - - match o with - | IOpConst n o r c => - liftOpt (fun x y => setIntReg r (evalIOp o x y) state) - (getIntReg r state) - (match c with | constInt32 v => Some v | constInt64 v => Some v end) - - | IOpReg n o a b => - liftOpt (fun x y => setIntReg a (evalIOp o x y) state) - (getIntReg a state) (getIntReg b state) - - | DOpReg n o a b h => - liftOpt (fun x y => - match (evalDualOp o x y) with - | (lw, hw) => - match (setIntReg a lw state) with - | Some st' => - match h with - | Some hr => setIntReg hr hw st' - | _ => Some st' - end - | None => None - end - end) - (getIntReg a state) (getIntReg b state) - - | OpRot n o r i => - match (getIntReg r state) with - | Some va => setIntReg r (evalRotOp o va i) state - | None => None - 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. -Definition getIConst {n} (c: IConst n): word n := - match c with - | constInt32 v => v - | constInt64 v => v +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)))) + + | 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 := - let liftOpt := fun {A B} (f: A -> option B) (xo: option A) => - match xo with - | (Some x') => f x' - | _ => None - end in - match a with - | ARegStackInt n r s => - liftOpt (fun x => setIntReg r x state) (getStack s state) - - | AStackRegInt n s r => - liftOpt (fun x => setStack s x state) (getIntReg r state) - - | ARegRegInt n a b => - liftOpt (fun x => setIntReg a x state) (getIntReg b state) - - | AConstInt n r c => setIntReg r (getIConst c) state - - | AIndex n m a b i => - match (getStack b state) with - | Some v => setIntReg a (trunc n (getIndex v m i)) state - | _ => None - end - - | APtr n r s => - setIntReg r (NToWord 32 (N.of_nat (getStackIndex s))) state + | 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. diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index dea937ac1..2dc3f6ade 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -4,56 +4,43 @@ Require Import QhasmCommon. Require Export Bedrock.Word. Module Util. - - Inductive Either A B := | xleft: A -> Either A B | xright: B -> Either A B. - - Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. - Coercion indexToNat : Index >-> nat. - - (* Magical Bitwise Manipulations *) - - (* Force w to be m bits long, by truncation or zero-extension *) - Definition trunc {n} (m: nat) (w: word n): word m. - destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s]. - - - replace m with (n + (m - n)) by abstract intuition. - refine (zext w (m - n)). - - - rewrite <- s; assumption. - - - replace n with (m + (n - m)) in w by abstract intuition. - refine (split1 m (n-m) w). - Defined. - - (* Get the index-th m-bit block of w *) - Definition getIndex {n} (w: word n) (m index: nat): word m. - replace n with - ((min n (m * index)) + (n - (min n (m * index))))%nat - in w by abstract ( - assert ((min n (m * index)) <= n)%nat - by apply Nat.le_min_l; - intuition). - - refine - (trunc m - (split2 (min n (m * index)) (n - min n (m * index)) w)). - Defined. - - (* set the index-th m-bit block of w to s *) - Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n := - (w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat))))) - ^| (trunc n (combine s (wzero (index * m)%nat))). - - (* Iterating Stack Operations *) - Lemma getStackWords_spec: forall {n} (x: Stack n), n = 32 * (getStackWords x). - Proof. intros; destruct x; simpl; intuition. Qed. - - Definition segmentStackWord {n} (x: Stack n) (w: word n): word (32 * (getStackWords x)). - intros; destruct x; simpl; intuition. - Defined. - - Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n. - intros; destruct x; simpl; intuition. - Defined. - - End Util. + (* Magical Bitwise Manipulations *) + + (* Force w to be m bits long, by truncation or zero-extension *) + Definition trunc {n} (m: nat) (w: word n): word m. + destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s]. + + - replace m with (n + (m - n)) by abstract intuition. + refine (zext w (m - n)). + + - rewrite <- s; assumption. + + - replace n with (m + (n - m)) in w by abstract intuition. + refine (split1 m (n-m) w). + Defined. + + (* Get the index-th m-bit block of w *) + Definition getIndex {n} (w: word n) (m index: nat): word m. + replace n with + ((min n (m * index)) + (n - (min n (m * index))))%nat + in w by abstract ( + assert ((min n (m * index)) <= n)%nat + by apply Nat.le_min_l; + intuition). + + refine + (trunc m + (split2 (min n (m * index)) (n - min n (m * index)) w)). + Defined. + + (* set the index-th m-bit block of w to s *) + Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n := + (w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat))))) + ^| (trunc n (combine s (wzero (index * m)%nat))). + + (* Option utilities *) + 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. diff --git a/src/Assembly/State.v b/src/Assembly/State.v index 0840538bc..df8bc97c1 100644 --- a/src/Assembly/State.v +++ b/src/Assembly/State.v @@ -1,274 +1,278 @@ Require Export String List Logic. Require Export Bedrock.Word. -Require Import ZArith NArith NPeano. -Require Import Coq.Structures.OrderedTypeEx. -Require Import FMapAVL FMapList. -Require Import JMeq. +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. -(* There's a lot in here. - We don't want to automatically give it all to the client. *) +(* 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 State. - Import ListNotations. - Import Util. - - Module NatM := FMapAVL.Make(Nat_as_OT). - Definition DefMap: Type := NatM.t N. - Definition StateMap: Type := NatM.t DefMap. - Definition LabelMap: Type := NatM.t nat. - - Delimit Scope state_scope with state. - Local Open Scope state_scope. - - (* The Big Definition *) - - Inductive State := - | fullState (intRegState: StateMap) - (stackState: DefMap) - (carryBit: CarryState): State. - - Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N) None. - - (* Register State Manipulations *) - - Definition getIntReg {n} (reg: IReg n) (state: State): option (word n) := - match state with - | fullState intRegState _ _ => - match (NatM.find n intRegState) with - | Some map => - match (NatM.find (getIRegIndex reg) map) with - | Some m => Some (NToWord n m) - | _ => None - end - | None => None - end - end. - - Definition setIntReg {n} (reg: IReg n) (value: word n) (state: State): option State := - match state with - | fullState intRegState stackState carryState => - match (NatM.find n intRegState) with - | Some map => - Some (fullState - (NatM.add n (NatM.add (getIRegIndex reg) (wordToN value) map) intRegState) - stackState - carryState) - | None => None - end - end. - - (* Carry State Manipulations *) - - Definition getCarry (state: State): CarryState := - match state with - | fullState _ _ b => b - end. - - Definition setCarry (value: bool) (state: State): State := - match state with - | fullState intRegState stackState carryState => - fullState intRegState stackState (Some value) - end. - - (* Per-word Stack Operations *) - - Definition getStack32 (entry: Stack 32) (state: State): option (word 32) := - match state with - | fullState _ stackState _ => - match entry with - | stack32 loc => - match (NatM.find loc stackState) with - | Some n => Some (NToWord 32 n) - | _ => None - end - end - end. - - Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State := + Import ListNotations Util. + + 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. + + Delimit Scope state_scope with state. + Open Scope state_scope. + + (* The Big Definition *) + + Inductive State := + | fullState (regState: PairNMap) + (stackState: PairNMap) + (memState: TripleNMap) + (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 carry => + fullState (PairM.add (n, regName r) (wordToN value) regS) + stackS memS 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 carry => + fullState regS + (PairM.add (n, stackName s) (wordToN value) stackS) + memS 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 carry => + fullState regS stackS + (TripleM.add (n, memName x, proj1_sig i) (wordToN value) memS) + carry + 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 intRegState stackState carryState => - match entry with - | stack32 loc => - (Some (fullState intRegState - (NatM.add loc (wordToN value) stackState) - carryState)) - end + | fullState regS stackS memS carry => + fullState regS stackS memS (Some value) end. - (* Inductive Word Manipulations*) - - Definition getWords' {n} (st: (list (word 32)) * word (32 * n)) : - Either (list (word 32)) ((list (word 32)) * word (32 * (n - 1))). - - destruct (Nat.eq_dec n 0) as [H | H]; - destruct st as [lst w]. - - - refine (xleft _ _ lst). - - - refine (xright _ _ - (cons (split1 32 (32 * (n - 1)) (cast w)) lst, - (split2 32 (32 * (n - 1)) (cast w)))); - intuition. - Defined. - - Section GetWords. - Program Fixpoint getWords'_iter (n: nat) (st: (list (word 32)) * word (32 * n)): list (word 32) := - match n with - | O => fst st - | S m => - match (getWords' st) with - | xleft lst => lst - | xright st => cast (getWords'_iter m st) - end - end. - - Definition getWords {len} (wd: word (32 * len)): list (word 32) := - getWords'_iter len ([], wd). - End GetWords. - - Section JoinWords. - - Inductive Any (U: nat -> Type) (lim: nat) := | any: forall n, (n <= lim)%nat -> U n -> Any U lim. - - Definition getAnySize {U lim} (a: Any U lim) := - match a as a' return a = a' -> _ with - | any n p v => fun _ => n - end (eq_refl a). - - Lemma lim_prop: forall (n lim: nat), (n <= lim)%nat -> ((n - 1) <= lim)%nat. - Proof. intros; intuition. Qed. - - Lemma zero_prop: forall (n m: nat), n = S m -> n <> 0. - Proof. intros; intuition. Qed. - - Fixpoint anyExp {U: nat -> Type} - {lim: nat} - (f: forall n, (n <> 0)%nat -> (n <= lim)%nat -> U n -> U (n - 1)) - (rem: nat) - (cur: Any U lim): option {a: Any U lim | getAnySize a = 0}. - - refine match rem with - | O => None - | S rem' => - match cur as c' return cur = c' -> _ with - | any n p v => always - match (Nat.eq_dec n 0) with - | left peq => Some (lift cur) - | right pneq => - anyExp U lim f rem' (any U lim (n - 1) (lim_prop n lim p) (f n pneq p v)) - end - end (eq_refl cur) - end. - - subst; unfold getAnySize; intuition. - - Defined. - - Definition JoinWordType (len: nat): nat -> Type := fun n => option (word (32 * (len - n))). - - Definition joinWordUpdate (len: nat) (wds: list (option (word 32))): - forall n, (n <> 0)%nat -> (n <= len)%nat -> JoinWordType len n -> JoinWordType len (n - 1). - - intros n H0 Hlen v; unfold JoinWordType in v. - refine match v with - | Some cur => - match (nth_error wds n) with - | Some (Some w) => Some (cast (combine w cur)) - | _ => None - end - | _ => None - end. - - abstract (replace (32 + 32 * (len - n)) with (32 * (len - (n - 1))); intuition). - Defined. - - Definition joinWordOpts (wds: list (option (word 32))): option (word (32 * (length wds))). - refine ( - let len := (length wds) in - let start := (any (JoinWordType len) len len _ (cast (Some (wzero 0)))) in - let aopt := anyExp (cast (joinWordUpdate len wds)) (length wds) start in - match aopt as aopt' return aopt = aopt' -> _ with - | Some a => always - match (proj1_sig a) as a' return (proj1_sig a) = a' -> _ with - | any n p v => always (cast v) - end (eq_refl (proj1_sig a)) - | _ => always None - end (eq_refl aopt) - ); try abstract intuition. - - - abstract ( unfold JoinWordType; replace (32 * (len-len)) with 0; intuition). - - - destruct a; simpl in _H0; destruct x, aopt. - - + abstract ( - destruct s; unfold getAnySize in e; simpl in e; subst; - inversion _H0; - unfold JoinWordType; - replace (len - 0) with len by intuition; - unfold len; intuition ). - - + inversion _H. - Defined. - - End JoinWords. - - (* Stack Manipulations *) - - Fixpoint getStack_iter (rem: nat) (loc: nat) (state: State): list (option (word 32)) := - match rem with - | O => [] - | (S rem') => - (getStack32 (stack32 loc) state) :: - (getStack_iter rem' (loc + 32) state) + Definition setCarryOpt (value: option bool) (state: State): State := + match value with + | Some c' => setCarry c' state + | _ => state end. - Lemma getStack_iter_length: forall rem loc state, - length (getStack_iter rem loc state) = rem. - Proof. - induction rem; intuition. - - replace (getStack_iter (S rem) loc state) with - ((getStack32 (stack32 loc) state) :: - (getStack_iter rem (loc + 32) state)) by intuition. - - replace (Datatypes.length _) with - (1 + Datatypes.length (getStack_iter rem (loc + 32) state)) by intuition. - - rewrite IHrem; intuition. - Qed. - - Definition getStack {n} (entry: Stack n) (state: State) : option (word n). - - refine ( - let m := getStackWords entry in - let i := getStackIndex entry in - let wos := (getStack_iter m i state) in - let joined := (joinWordOpts wos) in - - match joined as j return j = joined -> _ with - | Some w => always Some (cast w) - | None => always None - end (eq_refl joined) - ); abstract ( - intuition; - unfold wos; - rewrite getStack_iter_length; - destruct entry; simpl; intuition). - - Defined. - - Definition setStack {n} (entry: Stack n) (value: word n) (state: State) : option State := - (fix setStack_iter (wds: list (word 32)) (nextLoc: nat) (state: State) := - match wds with - | [] => Some state - | w :: ws => - match (setStack32 (stack32 nextLoc) w state) with - | Some st' => setStack_iter ws (S nextLoc) st' - | None => None - end - end) (getWords (segmentStackWord entry value)) (getStackIndex entry) state. - -End State. +End State. \ No newline at end of file diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v index 9eeb0f2ca..abd5b9367 100644 --- a/src/Assembly/StringConversion.v +++ b/src/Assembly/StringConversion.v @@ -187,36 +187,6 @@ Module StringConversion <: Conversion Qhasm QhasmString. simpl in H; inversion H; intuition. Qed. - Lemma triple_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. - - Definition triple_dec (x y: nat * nat * nat): {x = y} + {x <> y}. - refine (match x as x' return x' = _ -> _ with - | (x0, x1, x2) => fun _ => - match y as y' return y' = _ -> _ with - | (y0, y1, y2) => fun _ => - _ (Nat.eq_dec x0 y0) (Nat.eq_dec x1 y1) (Nat.eq_dec x2 y2) - end (eq_refl y) - end (eq_refl x)); - rewrite <- _H, <- _H0; - clear _H _H0 x y p p0; - intros. - - intros; destruct x6, x7, x8; first [ - left; abstract (subst; intuition) - | right; abstract (intro; - apply triple_conv in H; - destruct H; destruct H0; intuition) - ]. - Defined. - Definition entry_dec (x y: Entry): {x = y} + {x <> y}. refine (_ (triple_dec (entryId x) (entryId y))). intros; destruct x0. -- cgit v1.2.3