diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Assembly/AlmostConversion.v | 22 | ||||
-rw-r--r-- | src/Assembly/Pipeline.v | 30 | ||||
-rw-r--r-- | src/Assembly/PipelineExample.v | 53 | ||||
-rw-r--r-- | src/Assembly/Pseudo.v | 33 | ||||
-rw-r--r-- | src/Assembly/PseudoConversion.v | 348 | ||||
-rw-r--r-- | src/Assembly/QhasmCommon.v | 6 | ||||
-rw-r--r-- | src/Assembly/QhasmEvalCommon.v | 2 | ||||
-rw-r--r-- | src/Assembly/StringConversion.v | 26 |
8 files changed, 246 insertions, 274 deletions
diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v index e1fc988f1..878aa37bf 100644 --- a/src/Assembly/AlmostConversion.v +++ b/src/Assembly/AlmostConversion.v @@ -6,7 +6,7 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm. Import QhasmCommon AlmostQhasm Qhasm. Import ListNotations. - Fixpoint almostToQhasm' (prog: AlmostProgram) (lblStart: N): Qhasm.Program := + Fixpoint almostToQhasm' (prog: AlmostProgram) (lblStart: N): list QhasmStatement := let label0 := (lblStart * 2)%N in let label1 := (label0 + 1)%N in @@ -44,13 +44,21 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm. | ACall lbl => [QCall lbl] end. - Definition convertProgram (prog: AlmostQhasm.Program) := Some (almostToQhasm' prog 0%N). - Definition convertState (st: Qhasm.State): option AlmostQhasm.State := Some st. + Transparent Qhasm.Program AlmostQhasm.Program. - Lemma convert_spec: forall a a' b b' prog prog', - convertProgram prog = Some prog' -> - convertState a = Some a' -> convertState b = Some b' -> - Qhasm.evaluatesTo prog' a b <-> AlmostQhasm.evaluatesTo prog a' b'. + 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/Pipeline.v b/src/Assembly/Pipeline.v index b0cd4018e..acdfc3b03 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -4,16 +4,20 @@ Require Import Pseudo Qhasm AlmostQhasm Conversion Language. Require Import PseudoConversion AlmostConversion StringConversion. Module Pipeline. - Export Pseudo Util. + Export Util AlmostQhasm Qhasm QhasmString. + Export Pseudo. - Definition toAlmost (p: Pseudo inVars outVars): option AlmostQhasm.Program := - PseudoConversion.convertProgram p. + Transparent Pseudo.Program AlmostQhasm.Program Qhasm.Program QhasmString.Program. + Transparent Pseudo.Params AlmostQhasm.Params Qhasm.Params QhasmString.Params. - Definition toQhasm (p: Pseudo inVars outVars): option Qhasm.Program := - omap (toAlmost p) AlmostConversion.convertProgram. + Definition toAlmost {w s n m} (p: @Pseudo w s n m) : option AlmostProgram := + PseudoConversion.convertProgram (mkParams w s n m) tt p. - Definition toString (p: Pseudo inVars outVars): option string := - omap (toQhasm p) StringConversion.convertProgram. + 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. @@ -21,13 +25,7 @@ Module PipelineExample. Program Definition asdf: Program Unary32 := ($0 :+: $0)%p. - Definition exStr := Pipeline.toString ex. - | Some x => x - | None => EmptyString - end. - Defined. - -Open Scope string_scope. -Print Result. + Definition exStr := Pipeline.toString asdf. -Extraction "Result.ml" Result. + Eval vm_compute in exStr. +End PipelineExample. diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v deleted file mode 100644 index 8f7d43b9d..000000000 --- a/src/Assembly/PipelineExample.v +++ /dev/null @@ -1,53 +0,0 @@ - -Require Import QhasmCommon QhasmEvalCommon. -Require Import Pseudo Qhasm AlmostQhasm Medial Conversion Language. -Require Import PseudoMedialConversion AlmostConversion StringConversion. - -Extraction Language Ocaml. -Require Import ExtrOcamlString ExtrOcamlBasic. -Require Import Coq.Strings.String. - -Module Progs. - Module Arch := PseudoUnary32. - Module C32 := PseudoMedialConversion Arch. - - Import C32.P. - - Definition omap {A B} (f: A -> option B) (x: option A): option B := - match x with - | Some v => f v - | None => None - end. - - Definition prog0: C32.P.Program. - refine - (PBin _ Add (PComb _ _ _ - (PVar 1 (exist _ 0 _)) - (PConst _ (natToWord _ 1)))); abstract intuition. - Defined. - - Definition prog1: option C32.M.Program := - C32.PseudoConversion.convertProgram prog0. - - Definition prog2: option AlmostQhasm.Program := - omap C32.MedialConversion.convertProgram prog1. - - Definition prog3: option Qhasm.Program := - omap AlmostConversion.convertProgram prog2. - - Definition prog4: option string := - omap StringConversion.convertProgram prog3. -End Progs. - -Definition Result: string. - let res := eval vm_compute in ( - match Progs.prog4 with - | Some x => x - | None => EmptyString - end) in exact res. -Defined. - -Open Scope string_scope. -Print Result. - -Extraction "Result.ml" Result. diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index c4249804d..ede9607cf 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -5,19 +5,20 @@ Require Import List. Module Pseudo <: Language. Import EvalUtil ListState Util. - Inductive Pseudo {w: nat} {spec: Width w}: nat -> nat -> Type := + 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 + | 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 - | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m | 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. + | 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. @@ -110,7 +111,6 @@ Module Pseudo <: Language. pseudoEval prog st = Some st'. Delimit Scope pseudo_notations with p. - Open Scope pseudo_notations. Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n. intros; exists (x mod n); @@ -123,7 +123,7 @@ Module Pseudo <: Language. Notation "$ A" := (PVar _ (Some true) (indexize _ _ A)) (at level 20, right associativity) : pseudo_notations. - Notation "'MEM' ( A , B )" := (PMem _ _ (indexize _ _ A) (indexize _ _ B)) + Notation "A :[ B ]:" := (PMem _ _ (indexize _ _ A) (indexize _ _ B)) (at level 20, right associativity) : pseudo_notations. Notation "# A" := (PConst _ (natToWord _ A)) @@ -144,35 +144,32 @@ Module Pseudo <: Language. Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B)) (at level 45, right associativity) : pseudo_notations. - Notation "A :|: B" := (PBin _ Or (PComb _ _ _ A B)) - (at level 60, 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)) + Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B)) (at level 55, right associativity) : pseudo_notations. - Notation "'IF' O ( A , B ) 'THEN' L 'ELSE' R" := + Notation "O :( A , B ): :?: L ::: R" := (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R) - (at level 70, left associativity) : pseudo_notations. + (at level 70, right associativity) : pseudo_notations. - Notation "'EXP' ( e ) ( F )" := + Notation "F :**: e" := (PFunExp _ F e) - (at level 70, left associativity) : pseudo_notations. + (at level 70, right associativity) : pseudo_notations. - Notation "'LET' E 'IN' F" := + Notation "E :->: F" := (PLet _ _ _ E F) - (at level 70, left associativity) : pseudo_notations. + (at level 70, right associativity) : pseudo_notations. - Notation "A | B" := + Notation "A :|: B" := (PComb _ _ _ A B) (at level 65, left associativity) : pseudo_notations. - Notation "'CALL' n ::: A" := + Notation "n ::: A :():" := (PCall _ _ n A) (at level 65, left associativity) : pseudo_notations. End Pseudo. diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v index 39b655e47..65c80a960 100644 --- a/src/Assembly/PseudoConversion.v +++ b/src/Assembly/PseudoConversion.v @@ -1,185 +1,202 @@ - Require Export Language Conversion QhasmEvalCommon QhasmUtil. Require Export Pseudo AlmostQhasm State. -Require Export Bedrock.Word NArith NPeano Euclid. -Require Export List Sumbool Vector. +Require Import Bedrock.Word NArith NPeano Euclid. +Require Import List Sumbool Vector. Module PseudoConversion <: Conversion Pseudo AlmostQhasm. - Import QhasmCommon AlmostQhasm EvalUtil Util Pseudo StateCommon. - Import ListNotations. - - Definition MMap {w} := NatM.t (Mapping w). - Definition mempty {w} := NatM.empty (Mapping w). - - Definition FMap {w} := NatM.t (AlmostProgram * (list (Mapping w))). - Definition fempty {w} := NatM.empty (AlmostProgram * (list (Mapping w))). - - Definition getStart {w s n m} (prog: @Pseudo w s n m) := - let ns := (fix getStart' {n' m'} (p': @Pseudo w s n' m') := - match p' with - | PVar _ _ i => [proj1_sig i] - | PBin _ _ p => getStart' p - | PDual _ _ p => getStart' p - | PCarry _ _ p => getStart' p - | PShift _ _ _ p => getStart' p - | PIf _ _ _ _ _ l r => (getStart' l) ++ (getStart' r) - | PFunExp _ p _ => getStart' p - | PLet _ k _ a b => (n + k) :: (getStart' a) ++ (getStart' b) - | PComb _ _ _ a b => (getStart' a) ++ (getStart' b) - | PCall _ _ _ p => getStart' p - | _ => [] - end) _ _ prog in - - maxN (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 n m) (start: nat) (M: MMap) (F: FMap): - option (AlmostProgram * (list (Mapping width)) * MMap * FMap) := - let rM := fun (x: nat) => regM _ (reg width_spec x) in - let sM := fun (x: nat) => stackM _ (stack width_spec x) in - - let reg' := reg width_spec in - let stack' := stack width_spec in - let const' := const width_spec 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 width) => NatM.add k (f k) in - let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping width)) => 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 width_spec 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 + Import AlmostQhasm EvalUtil ListState Util 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') + | 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 + | _ => 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') + | 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 + | _ => 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') + | 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 + | _ => 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 + | PLet n k m f g => + match (convertProgram' f start M F) with | None => None - | Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'') + | 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 - 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 + | PComb n a b f g => + match (convertProgram' f start M F) with | None => None - | Some (gp, gm, M'', F'') => Some (ASeq fp gp, fm ++ gm, M'', F'') + | 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 - 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 + | PIf n m o i0 i1 l r => + match (convertProgram' l start M F) 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 + | 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 - 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') + | 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 - | _ => 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 + | 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. - Definition convertProgram (prog: Pseudo inVars outVars): option AlmostProgram := - match (convertProgram' prog (max inVars outVars) mempty fempty) with + 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) @@ -188,15 +205,15 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. | _ => None end. - Fixpoint convertState (st: AlmostQhasm.State): option State := - let vars := max inVars outVars in + 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 width_spec i) st, - FullState.getStack (stack width_spec i) st) with + 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 @@ -212,9 +229,10 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm. else None end. - Lemma convert_spec: forall a a' b b' prog prog', - convertProgram prog = Some prog' -> - convertState a = Some a' -> convertState b = Some b' -> - AlmostQhasm.evaluatesTo prog' a b <-> evaluatesTo prog a' b'. + 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/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 21f846cb5..654f109f3 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -19,7 +19,7 @@ Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64. (* A constant value *) Inductive Const: nat -> Type := - | const: forall {n}, Width n -> word n -> Const n. + | constant: forall {n}, Width n -> word n -> Const n. (* A variable in any register *) Inductive Reg: nat -> Type := @@ -109,10 +109,10 @@ 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. + match x with | @constant n _ v => v end. Definition constValueN {n} (x: Const n): nat := - match x with | @const n _ v => wordToNat v end. + match x with | @constant n _ v => wordToNat v end. Definition regName {n} (x: Reg n): nat := match x with | @reg n _ v => v end. diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v index b12e27e19..566d7b892 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -88,7 +88,7 @@ Module EvalUtil. (* Mapping Conversions *) Definition wordToM {n: nat} {spec: Width n} (w: word n): Mapping n := - constM _ (const spec w). + constM _ (constant spec w). Definition regToM {n: nat} {spec: Width n} (r: Reg n): Mapping n := regM _ r. diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v index 151eaa3f7..f3ff40ff7 100644 --- a/src/Assembly/StringConversion.v +++ b/src/Assembly/StringConversion.v @@ -5,17 +5,18 @@ Require Import NArith NPeano. Require Export Bedrock.Word. Module QhasmString <: Language. - Definition Program := string. - Definition State := unit. + Definition Params := unit. + Definition Program := fun (_: Params) => string. + Definition State := fun (_: Params) => unit. - Definition evaluatesTo (p: Program) (i o: State): Prop := True. + 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 (st: QhasmString.State): option Qhasm.State := None. + Definition convertState x y (st: QhasmString.State y): option (Qhasm.State x) := None. (* Hexadecimal Primitives *) @@ -62,7 +63,7 @@ Module StringConversion <: Conversion Qhasm QhasmString. "0x" ++ (nToHex (wordToN w)). Coercion constToString {n} (c: Const n): string := - match c with | const _ _ w => wordToString w end. + match c with | constant _ _ w => wordToString w end. Coercion regToString {n} (r: Reg n): string := match r with @@ -191,7 +192,7 @@ Module StringConversion <: Conversion Qhasm QhasmString. Arguments memM [n m] x i. Arguments constM [n] x. - Fixpoint entries (width: nat) (prog: Program): list (Mapping width) := + Fixpoint entries (width: nat) (prog: list QhasmStatement): list (Mapping width) := match prog with | cons s next => match s with @@ -354,7 +355,9 @@ Module StringConversion <: Conversion Qhasm QhasmString. | QRet => [("pop %eip")%string] end. - Definition convertProgram (prog: Qhasm.Program): option string := + 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 @@ -374,10 +377,11 @@ Module StringConversion <: Conversion Qhasm QhasmString. stmts ++ blank ++ leave ++ blank) EmptyString). - Lemma convert_spec: forall a a' b b' prog prog', - convertProgram prog = Some prog' -> - convertState a = Some a' -> convertState b = Some b' -> - QhasmString.evaluatesTo prog' a b <-> Qhasm.evaluatesTo prog a' b'. + 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. |