diff options
-rw-r--r-- | src/hls/DMemorygen.v | 2 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 2 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 302 | ||||
-rw-r--r-- | src/hls/HTLPargenproof.v | 983 | ||||
-rw-r--r-- | src/hls/Predicate.v | 2 |
5 files changed, 1043 insertions, 248 deletions
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v index bef9f3d..1b7d2e0 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021-2023 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 7dd1c97..34ba238 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -207,8 +207,6 @@ Fixpoint from_predicated_inv (a: predicated pred_expression): pred_op := Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) := Option.map simplify (combine_pred a b). -Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default T p. - Definition assert_ (b: bool): option unit := if b then Some tt else None. diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 1bc0fd5..e9061a5 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -33,6 +33,11 @@ Require Import vericert.hls.Verilog. Require Import vericert.hls.Gible. Require Import vericert.hls.GiblePar. Require Import vericert.hls.Predicate. +Require Import vericert.common.Errormonad. +Import ErrorMonad. +Import ErrorMonadExtra. + +#[local] Open Scope monad_scope. #[local] Hint Resolve AssocMap.gempty : htlh. #[local] Hint Resolve AssocMap.gso : htlh. @@ -40,62 +45,14 @@ Require Import vericert.hls.Predicate. #[local] Hint Resolve Ple_refl : htlh. #[local] Hint Resolve Ple_succ : htlh. -Record state: Type := mkstate { - st_st : reg; - st_freshreg: reg; - st_freshstate: node; - st_scldecls: AssocMap.t (option io * scl_decl); - st_arrdecls: AssocMap.t (option io * arr_decl); - st_datapath: datapath; +Record control_regs: Type := mk_control_regs { + ctrl_st : reg; + ctrl_stack : reg; + ctrl_preg : reg; + ctrl_fin : reg; + ctrl_return : reg; }. -Definition init_state (st : reg) : state := - mkstate st - 1%positive - 1%positive - (AssocMap.empty (option io * scl_decl)) - (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt). - -Module HTLState <: State. - - Definition st := state. - - Inductive st_incr: state -> state -> Prop := - state_incr_intro: - forall (s1 s2: state), - st_st s1 = st_st s2 -> - Ple s1.(st_freshreg) s2.(st_freshreg) -> - Ple s1.(st_freshstate) s2.(st_freshstate) -> - (forall n, - s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> - st_incr s1 s2. - #[export] Hint Constructors st_incr : htlh. - - Definition st_prop := st_incr. - #[export] Hint Unfold st_prop : htlh. - - Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. - - Lemma st_trans : - forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. - Proof. - intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence. - - destruct H4 with n; destruct H7 with n; intuition congruence. - Qed. - -End HTLState. -Export HTLState. - -Module HTLMonad := Statemonad(HTLState). -Export HTLMonad. - -Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). -Import HTLMonadExtra. -Export MonadNotation. - -#[local] Open Scope monad_scope. - Definition pred_lit (preg: reg) (pred: predicate) := Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)). @@ -133,62 +90,6 @@ Definition state_goto (preg: reg) (p: option pred_op) (st : reg) (n : node) : st Definition state_cond (preg: reg) (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt := translate_predicate Vblock preg p (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). -Definition check_empty_node_datapath: - forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. -Proof. - intros. case (s.(st_datapath)!n); tauto. -Defined. - -Definition append_instr (n : node) (st : stmnt) (d : datapath) : datapath := - match AssocMap.get n d with - | Some st' => AssocMap.set n (Vseq st' st) d - | None => AssocMap.set n st d - end. - -Lemma declare_reg_state_incr : - forall i s r sz, - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - s.(st_datapath)). -Proof. Admitted. - -Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := - fun s => OK tt (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - s.(st_datapath)) - (declare_reg_state_incr i s r sz). - -Lemma declare_arr_state_incr : - forall i s r sz ln, - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - s.(st_scldecls) - (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls)) - s.(st_datapath)). -Proof. Admitted. - -Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon unit := - fun s => OK tt (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - s.(st_scldecls) - (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls)) - s.(st_datapath)) - (declare_arr_state_incr i s r sz ln). - Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. @@ -201,15 +102,17 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := Definition boplitz (op: binop) (r: reg) (l: Z) : expr := Vbinop op (Vvar r) (Vlit (ZToValue l)). +Definition error {A} m := @Errors.Error A (Errors.msg m). + Definition translate_comparison (c : Integers.comparison) (args : list reg) : Errors.res expr := match c, args with - | Integers.Ceq, r1::r2::nil => Errors.OK (bop Veq r1 r2) - | Integers.Cne, r1::r2::nil => Errors.OK (bop Vne r1 r2) - | Integers.Clt, r1::r2::nil => Errors.OK (bop Vlt r1 r2) - | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgt r1 r2) - | Integers.Cle, r1::r2::nil => Errors.OK (bop Vle r1 r2) - | Integers.Cge, r1::r2::nil => Errors.OK (bop Vge r1 r2) - | _, _ => Errors.Error (Errors.msg "Htlgen: comparison instruction not implemented: other") + | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) + | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) + | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) + | _, _ => error "Htlpargen: comparison instruction not implemented: other" end. Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) @@ -221,7 +124,7 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) | Integers.Cgt, r1::nil => Errors.OK (boplit Vgt r1 i) | Integers.Cle, r1::nil => Errors.OK (boplit Vle r1 i) | Integers.Cge, r1::nil => Errors.OK (boplit Vge r1 i) - | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + | _, _ => error "Htlpargen: comparison_imm instruction not implemented: other" end. Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : Errors.res expr := @@ -230,7 +133,7 @@ Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : E | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgtu r1 r2) | Integers.Cle, r1::r2::nil => Errors.OK (bop Vleu r1 r2) | Integers.Cge, r1::r2::nil => Errors.OK (bop Vgeu r1 r2) - | _, _ => Errors.Error (Errors.msg "Htlgen: comparison instruction not implemented: other") + | _, _ => Errors.Error (Errors.msg "Htlpargen: comparison instruction not implemented: other") end. Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int) @@ -240,7 +143,7 @@ Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) | Integers.Cgt, r1::nil => Errors.OK (boplit Vgtu r1 i) | Integers.Cle, r1::nil => Errors.OK (boplit Vleu r1 i) | Integers.Cge, r1::nil => Errors.OK (boplit Vgeu r1 i) - | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + | _, _ => Errors.Error (Errors.msg "Htlpargen: comparison_imm instruction not implemented: other") end. Definition translate_condition (c : Op.condition) (args : list reg) : Errors.res expr := @@ -249,9 +152,9 @@ Definition translate_condition (c : Op.condition) (args : list reg) : Errors.res | Op.Ccompu c, _ => translate_comparisonu c args | Op.Ccompimm c i, _ => translate_comparison_imm c args i | Op.Ccompuimm c i, _ => translate_comparison_immu c args i - | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") - | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") - | _, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: other") + | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: Cmasknotzero") + | _, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: other") end. Definition check_address_parameter_signed (p : Z) : bool := @@ -299,8 +202,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex | Op.Osub, r1::r2::nil => Errors.OK (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => Errors.OK (bop Vmul r1 r2) | Op.Omulimm n, r::nil => Errors.OK (boplit Vmul r n) - | Op.Omulhs, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: mulhs") - | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: mulhu") + | Op.Omulhs, r1::r2::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: mulhu") | Op.Odiv, r1::r2::nil => Errors.OK (bop Vdiv r1 r2) | Op.Odivu, r1::r2::nil => Errors.OK (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => Errors.OK (bop Vmod r1 r2) @@ -322,7 +225,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex (Vbinop Vshru (Vvar r) (Vlit n))) | Op.Oshru, r1::r2::nil => Errors.OK (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => Errors.OK (boplit Vshru r n) - | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: Ororimm") (*Errors.OK (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) | Op.Oshldimm n, r::nil => Errors.OK (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) @@ -331,7 +234,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex do tc <- translate_condition c rl; Errors.OK (Vternary tc (Vvar r1) (Vvar r2)) | Op.Olea a, _ => translate_eff_addressing a args - | _, _ => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: other") + | _, _ => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: other") end. Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) @@ -393,8 +296,6 @@ Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr) Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.") end. -Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p. - Definition transf_instr (fin rtrn stack state preg: reg) (dc: pred_op * stmnt) (i: instr) : Errors.res (pred_op * stmnt) := @@ -423,20 +324,17 @@ Definition transf_instr (fin rtrn stack state preg: reg) Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt) end. -Definition fold_leftE {A B} (f: A -> B -> Errors.res A) (l: list B) (el: A): Errors.res A := - fold_left (fun a b => do a' <- a; f a' b) l (Errors.OK el). - Definition transf_chained_block (fin rtrn stack state preg: reg) (dc: @pred_op positive * stmnt) (block: list instr) : Errors.res (pred_op * stmnt) := - fold_leftE (transf_instr fin rtrn stack state preg) block dc. + mfold_left (transf_instr fin rtrn stack state preg) block (ret dc). Definition transf_parallel_block (fin rtrn stack state preg: reg) (dc: @pred_op positive * stmnt) (block: list (list instr)) : Errors.res (pred_op * stmnt) := - fold_leftE (transf_chained_block fin rtrn stack state preg) block dc. + mfold_left (transf_chained_block fin rtrn stack state preg) block (ret dc). Definition transf_parallel_full_block (fin rtrn stack state preg: reg) (dc: node * @pred_op positive * datapath) @@ -457,85 +355,14 @@ Definition transf_seq_block (fin rtrn stack state preg: reg) (d: datapath) (n: node) (block: list (list (list instr))) : Errors.res datapath := - do res <- fold_leftE - (transf_parallel_full_block fin rtrn stack state preg) block (n, Ptrue, d); + do res <- mfold_left + (transf_parallel_full_block fin rtrn stack state preg) block (ret (n, Ptrue, d)); let '(_, _, d') := res in Errors.OK d'. -#[local] Close Scope error_monad_scope. -#[local] Open Scope monad_scope. - -Program Definition transf_seq_blockM (fin rtrn stack preg: reg) (ni: node * ParBB.t): mon unit := - fun st => +Definition transf_seq_blockM (ctrl: control_regs) (d: datapath) (ni: node * ParBB.t): res datapath := let (n, i) := ni in - match transf_seq_block fin rtrn stack st.(st_st) preg st.(st_datapath) n i with - | Errors.OK d => - OK tt (mkstate st.(st_st) - st.(st_freshreg) - st.(st_freshstate) - st.(st_scldecls) - st.(st_arrdecls) - d) _ - | Errors.Error m => Error m - end. -Next Obligation. -admit. -Admitted. - -Definition declare_regs (i: instr): mon unit := - match i with - | RBop _ _ _ d => declare_reg None d 32 - | RBload _ _ _ _ d => declare_reg None d 32 - | _ => ret tt - end. - -Definition declare_all_regs (ni: node * ParBB.t): mon unit := - let (n, i) := ni in - ParBB.foldl _ (fun (st_f: mon unit) i => do _tt <- st_f; declare_regs i) i (ret tt). - -Lemma create_reg_state_incr: - forall s sz i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - (st_datapath s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_reg (i : option io) (sz : nat) : mon reg := - fun s => let r := s.(st_freshreg) in - OK r (mkstate - s.(st_st) - (Pos.succ r) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - (st_arrdecls s) - (st_datapath s)) - (create_reg_state_incr s sz i). - -Lemma create_arr_state_incr: - forall s sz ln i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := - fun s => let r := s.(st_freshreg) in - OK (r, ln) (mkstate - s.(st_st) - (Pos.succ r) - (st_freshstate s) - s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s)) - (create_arr_state_incr s sz ln i). + transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) ctrl.(ctrl_preg) d n i. Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). @@ -580,61 +407,46 @@ Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {T end; unfold module_ordering; auto. Defined. -Definition transf_module (f: function) : mon DHTL.module. - refine ( +Program Definition transl_module (f: function) : res DHTL.module := if stack_correct f.(fn_stacksize) then - do fin <- create_reg (Some Voutput) 1; - do rtrn <- create_reg (Some Voutput) 32; - do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do start <- create_reg (Some Vinput) 1; - do rst <- create_reg (Some Vinput) 1; - do clk <- create_reg (Some Vinput) 1; - do preg <- create_reg None 128; - do _stmnt <- collectlist (transf_seq_blockM fin rtrn stack preg) (Maps.PTree.elements f.(GiblePar.fn_code)); - do _stmnt' <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(GiblePar.fn_params); - do _stmnt'' <- collectlist declare_all_regs (Maps.PTree.elements f.(GiblePar.fn_code)); - do current_state <- get; - match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, - decide_order (st_st current_state) fin rtrn stack start rst clk preg, - max_list_dec (GiblePar.fn_params f) (st_st current_state) + let st := Pos.succ (max_reg_function f) in + let fin := Pos.succ st in + let rtrn := Pos.succ fin in + let stack := Pos.succ rtrn in + let start := Pos.succ stack in + let rst := Pos.succ start in + let clk := Pos.succ rst in + let preg := Pos.succ clk in + do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack preg fin rtrn)) + (Maps.PTree.elements f.(GiblePar.fn_code)) (ret (PTree.empty _)); + match zle (Z.pos (max_pc_map _stmnt)) Integers.Int.max_unsigned, + decide_order st fin rtrn stack start rst clk preg, + max_list_dec (GiblePar.fn_params f) st with | left LEDATA, left MORD, left WFPARAMS => ret (DHTL.mkmodule f.(GiblePar.fn_params) - current_state.(st_datapath) + _stmnt f.(fn_entrypoint) - current_state.(st_st) + st stack - stack_len + (Z.to_nat (f.(fn_stacksize) / 4)) fin rtrn start rst clk preg - current_state.(st_scldecls) - current_state.(st_arrdecls) + (AssocMap.empty _) + (AssocMap.empty _) None (max_pc_wf _ LEDATA) MORD _ WFPARAMS) - | _, _, _ => error (Errors.msg "More than 2^32 states.") + | _, _, _ => error "More than 2^32 states." end - else error (Errors.msg "Stack size misalignment.")); discriminate. -Defined. - -Definition max_state (f: function) : state := - let st := Pos.succ (max_reg_function f) in - mkstate st - (Pos.succ st) - (Pos.succ (max_pc_function f)) - (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) - (st_arrdecls (init_state st)) - (st_datapath (init_state st)). - -Definition transl_module (f : function) : Errors.res DHTL.module := - run_mon (max_state f) (transf_module f). + else error "Stack size misalignment.". Definition transl_fundef := transf_partial_fundef transl_module. diff --git a/src/hls/HTLPargenproof.v b/src/hls/HTLPargenproof.v new file mode 100644 index 0000000..5c0272f --- /dev/null +++ b/src/hls/HTLPargenproof.v @@ -0,0 +1,983 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +Require Import Coq.micromega.Lia. + +Require Import compcert.lib.Maps. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require compcert.backend.Registers. +Require Import compcert.common.Linking. +Require Import compcert.common.Memory. +Require compcert.common.Globalenvs. +Require Import compcert.lib.Integers. +Require Import compcert.common.AST. + +Require Import vericert.common.IntegerExtra. +Require Import vericert.common.Vericertlib. +Require Import vericert.common.ZExtra. +Require Import vericert.hls.Array. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.DHTL. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.HTLPargen. +Require Import vericert.hls.HTLPargen. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. +Require vericert.hls.Verilog. +Require Import vericert.common.Errormonad. +Import ErrorMonad. +Import ErrorMonadExtra. + +Require Import Lia. + +Local Open Scope assocmap. + +#[local] Hint Resolve AssocMap.gss : htlproof. +#[local] Hint Resolve AssocMap.gso : htlproof. + +#[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. + +Inductive match_assocmaps : GiblePar.function -> Gible.regset -> assocmap -> Prop := + match_assocmap : forall f rs am, + (forall r, Ple r (max_reg_function f) -> + val_value_lessdef (Registers.Regmap.get r rs) am#r) -> + match_assocmaps f rs am. +#[local] Hint Constructors match_assocmaps : htlproof. + +Inductive match_arrs (m : DHTL.module) (f : GiblePar.function) (sp : Values.val) (mem : mem) : + Verilog.assocmap_arr -> Prop := +| match_arr : forall asa stack, + asa ! (m.(DHTL.mod_stk)) = Some stack /\ + stack.(arr_length) = Z.to_nat (f.(GiblePar.fn_stacksize) / 4) /\ + (forall ptr, + 0 <= ptr < Z.of_nat m.(DHTL.mod_stk_len) -> + opt_val_value_lessdef (Mem.loadv AST.Mint32 mem + (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr)))) + (Option.default (NToValue 0) + (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> + match_arrs m f sp mem asa. + +Definition stack_based (v : Values.val) (sp : Values.block) : Prop := + match v with + | Values.Vptr sp' off => sp' = sp + | _ => True + end. + +Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := + forall r, stack_based (Registers.Regmap.get r rs) sp. + +Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) + (sp : Values.val) : Prop := + forall ptr, + 0 <= ptr < (stack_length / 4) -> + stack_based (Option.default + Values.Vundef + (Mem.loadv AST.Mint32 m + (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr))))) + spb. + +Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := + forall ptr v, + hi <= ptr <= Ptrofs.max_unsigned -> + Z.modulo ptr 4 = 0 -> + Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Ptrofs.repr ptr )) = None /\ + Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Ptrofs.repr ptr )) v = None. + +Inductive match_frames : list GiblePar.stackframe -> list DHTL.stackframe -> Prop := +| match_frames_nil : + match_frames nil nil. + +Inductive match_constants : DHTL.module -> assocmap -> Prop := + match_constant : + forall m asr, + asr!(DHTL.mod_reset m) = Some (ZToValue 0) -> + asr!(DHTL.mod_finish m) = Some (ZToValue 0) -> + match_constants m asr. + +Definition state_st_wf (m : DHTL.module) (s : DHTL.state) := + forall st asa asr res, + s = DHTL.State res m st asa asr -> + asa!(m.(DHTL.mod_st)) = Some (posToValue st). +#[local] Hint Unfold state_st_wf : htlproof. + +Inductive match_states : GiblePar.state -> DHTL.state -> Prop := +| match_state : forall asa asr sf f sp sp' rs mem m st res ps + (MASSOC : match_assocmaps f rs asr) + (TF : transl_module f = Errors.OK m) + (WF : state_st_wf m (DHTL.State res m st asr asa)) + (MF : match_frames sf res) + (MARR : match_arrs m f sp mem asa) + (SP : sp = Values.Vptr sp' (Ptrofs.repr 0)) + (RSBP : reg_stack_based_pointers sp' rs) + (ASBP : arr_stack_based_pointers sp' mem (f.(GiblePar.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(GiblePar.fn_stacksize)) mem) + (CONST : match_constants m asr), + (* Add a relation about ps compared with the state register. *) + match_states (GiblePar.State sf f sp st rs ps mem) + (DHTL.State res m st asr asa) +| match_returnstate : + forall + v v' stack mem res + (MF : match_frames stack res), + val_value_lessdef v v' -> + match_states (GiblePar.Returnstate stack v mem) (DHTL.Returnstate res v') +| match_initial_call : + forall f m m0 + (TF : transl_module f = Errors.OK m), + match_states (GiblePar.Callstate nil (AST.Internal f) nil m0) (DHTL.Callstate nil m nil). +#[local] Hint Constructors match_states : htlproof. + +Definition match_prog (p: GiblePar.program) (tp: DHTL.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ + main_is_internal p = true. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + +#[global] Instance TransfHTLLink (tr_fun: GiblePar.program -> Errors.res DHTL.program): + TransfLink (fun (p1: GiblePar.program) (p2: DHTL.program) => match_prog p1 p2). +Proof. + red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + apply link_prog_inv in H. + + unfold match_prog in *. + unfold main_is_internal in *. simplify. repeat (unfold_match H4). + repeat (unfold_match H3). simplify. + subst. rewrite H0 in *. specialize (H (AST.prog_main p2)). + exploit H. + apply Genv.find_def_symbol. exists b. split. + assumption. apply Genv.find_funct_ptr_iff. eassumption. + apply Genv.find_def_symbol. exists b0. split. + assumption. apply Genv.find_funct_ptr_iff. eassumption. + intros. inv H3. inv H5. destruct H6. inv H5. +Qed. + +Definition match_prog' (p: GiblePar.program) (tp: DHTL.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + +Lemma match_prog_matches : + forall p tp, match_prog p tp -> match_prog' p tp. +Proof. unfold match_prog. tauto. Qed. + +Lemma transf_program_match: + forall p tp, HTLPargen.transl_program p = Errors.OK tp -> match_prog p tp. +Proof. + intros. unfold transl_program in H. + destruct (main_is_internal p) eqn:?; try discriminate. + unfold match_prog. split. + apply Linking.match_transform_partial_program; auto. + assumption. +Qed. + +Lemma regs_lessdef_add_greater : + forall f rs1 rs2 n v, + Plt (max_reg_function f) n -> + match_assocmaps f rs1 rs2 -> + match_assocmaps f rs1 (AssocMap.set n v rs2). +Proof. + inversion 2; subst. + intros. constructor. + intros. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso. eauto. + apply Pos.le_lt_trans with _ _ n in H2. + unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. +Qed. +#[local] Hint Resolve regs_lessdef_add_greater : htlproof. + +Lemma regs_lessdef_add_match : + forall f rs am r v v', + val_value_lessdef v v' -> + match_assocmaps f rs am -> + match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). +Proof. + inversion 2; subst. + constructor. intros. + destruct (peq r0 r); subst. + rewrite Registers.Regmap.gss. + unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gss. assumption. + + rewrite Registers.Regmap.gso; try assumption. + unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso; eauto. +Qed. +#[local] Hint Resolve regs_lessdef_add_match : htlproof. + +Lemma list_combine_none : + forall n l, + length l = n -> + list_combine Verilog.merge_cell (list_repeat None n) l = l. +Proof. + induction n; intros; crush. + - symmetry. apply length_zero_iff_nil. auto. + - destruct l; crush. + rewrite list_repeat_cons. + crush. f_equal. + eauto. +Qed. + +Lemma combine_none : + forall n a, + a.(arr_length) = n -> + arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. +Proof. + intros. + unfold combine. + crush. + + rewrite <- (arr_wf a) in H. + apply list_combine_none. + assumption. +Qed. + +Lemma list_combine_lookup_first : + forall l1 l2 n, + length l1 = length l2 -> + nth_error l1 n = Some None -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. +Proof. + induction l1; intros; crush. + + rewrite nth_error_nil in H0. + discriminate. + + destruct l2 eqn:EQl2. crush. + simpl in H. inv H. + destruct n; simpl in *. + inv H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_first : + forall a1 a2 n, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some None -> + array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_first; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Lemma list_combine_lookup_second : + forall l1 l2 n x, + length l1 = length l2 -> + nth_error l1 n = Some (Some x) -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). +Proof. + induction l1; intros; crush; auto. + + destruct l2 eqn:EQl2. crush. + simpl in H. inv H. + destruct n; simpl in *. + inv H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_second : + forall a1 a2 n x, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some (Some x) -> + array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_second; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Ltac unfold_func H := + match type of H with + | ?f = _ => unfold f in H; repeat (unfold_match H) + | ?f _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) + end. + +Lemma init_reg_assoc_empty : + forall f l, + match_assocmaps f (Gible.init_regs nil l) (DHTL.init_regs nil l). +Proof. + induction l; simpl; constructor; intros. + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. + + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. +Qed. + +Lemma arr_lookup_some: + forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr) + (stack : Array (option value)) (H5 : asa ! r = Some stack) n, + exists x, Verilog.arr_assocmap_lookup asa r n = Some x. +Proof. + intros z r0 r asr asa stack H5 n. + eexists. + unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. +Qed. +#[local] Hint Resolve arr_lookup_some : htlproof. + +Section CORRECTNESS. + + Variable prog : GiblePar.program. + Variable tprog : DHTL.program. + + Hypothesis TRANSL : match_prog prog tprog. + + Lemma TRANSL' : + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + Proof. intros; apply match_prog_matches; assumption. Qed. + + Let ge : GiblePar.genv := Globalenvs.Genv.globalenv prog. + Let tge : DHTL.genv := Globalenvs.Genv.globalenv tprog. + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. + + Lemma function_ptr_translated: + forall (b: Values.block) (f: GiblePar.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. + Proof. + intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma functions_translated: + forall (v: Values.val) (f: GiblePar.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Proof. + intros. exploit (Genv.find_funct_match TRANSL'); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof + (Genv.senv_transf_partial TRANSL'). + #[local] Hint Resolve senv_preserved : htlproof. + + Lemma ptrofs_inj : + forall a b, + Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b. + Proof. + intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned. + rewrite H. auto. + Qed. + + Lemma op_stack_based : + forall F V sp v m args rs op ge ver, + translate_instr op args = Errors.OK ver -> + reg_stack_based_pointers sp rs -> + @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op + (List.map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> + stack_based v sp. + Proof. + Ltac solve_no_ptr := + match goal with + | H: reg_stack_based_pointers ?sp ?rs |- stack_based (Registers.Regmap.get ?r ?rs) _ => + solve [apply H] + | H1: reg_stack_based_pointers ?sp ?rs, H2: Registers.Regmap.get _ _ = Values.Vptr ?b ?i + |- context[Values.Vptr ?b _] => + let H := fresh "H" in + assert (H: stack_based (Values.Vptr b i) sp) by (rewrite <- H2; apply H1); simplify; solve [auto] + | |- context[Registers.Regmap.get ?lr ?lrs] => + destruct (Registers.Regmap.get lr lrs) eqn:?; simplify; auto + | |- stack_based (?f _) _ => unfold f + | |- stack_based (?f _ _) _ => unfold f + | |- stack_based (?f _ _ _) _ => unfold f + | |- stack_based (?f _ _ _ _) _ => unfold f + | H: ?f _ _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H); inv H + | H: ?f _ _ _ _ _ _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H); inv H + | H: map (fun r : positive => Registers.Regmap.get r _) ?args = _ |- _ => + destruct args; inv H + | |- context[if ?c then _ else _] => destruct c; try discriminate + | H: match _ with _ => _ end = Some _ |- _ => repeat (unfold_match H; try discriminate) + | H: match _ with _ => _ end = OK _ _ _ |- _ => repeat (unfold_match H; try discriminate) + | |- context[match ?g with _ => _ end] => destruct g; try discriminate + | |- _ => simplify; solve [auto] + end. + intros **. + unfold translate_instr in *. + unfold_match H; repeat (unfold_match H); simplify; try solve [repeat solve_no_ptr]. + subst. + unfold translate_eff_addressing in H. + repeat (unfold_match H; try discriminate); simplify; try solve [repeat solve_no_ptr]. + Qed. + + Lemma int_inj : + forall x y, + Int.unsigned x = Int.unsigned y -> + x = y. + Proof. + intros. rewrite <- Int.repr_unsigned at 1. rewrite <- Int.repr_unsigned. + rewrite <- H. trivial. + Qed. + + Lemma Ptrofs_compare_correct : + forall a b, + Ptrofs.ltu (valueToPtr a) (valueToPtr b) = Int.ltu a b. + Proof. + intros. unfold valueToPtr. unfold Ptrofs.ltu. unfold Ptrofs.of_int. unfold Int.ltu. + rewrite !Ptrofs.unsigned_repr in *; auto using Int.unsigned_range_2. + Qed. + + Lemma eval_cond_correct : + forall stk f sp pc rs m res ml st asr asa e b f' args cond pr, + match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) -> + (forall v, In v args -> Ple v (max_reg_function f)) -> + Op.eval_condition cond (List.map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> + translate_condition cond args = OK e -> + Verilog.expr_runp f' asr asa e (boolToValue b). + Proof. + intros * MSTATE MAX_FUN EVAL TR_INSTR. + unfold translate_condition, translate_comparison, translate_comparisonu, translate_comparison_imm, translate_comparison_immu in TR_INSTR. + repeat (destruct_match; try discriminate); subst; unfold ret in *; match goal with H: OK _ = OK _ |- _ => inv H end; unfold bop in *; cbn in *; + try (solve [econstructor; try econstructor; eauto; unfold binop_run; + unfold Values.Val.cmp_bool, Values.Val.cmpu_bool in EVAL; repeat (destruct_match; try discriminate); inv EVAL; + inv MSTATE; inv MASSOC; + assert (X: Ple p (max_reg_function f)) by eauto; + assert (X1: Ple p0 (max_reg_function f)) by eauto; + apply H in X; apply H in X1; + rewrite Heqv in X; + rewrite Heqv0 in X1; + inv X; inv X1; auto; try (rewrite Ptrofs_compare_correct; auto)| + econstructor; try econstructor; eauto; unfold binop_run; + unfold Values.Val.cmp_bool, Values.Val.cmpu_bool in EVAL; repeat (destruct_match; try discriminate); inv EVAL; + inv MSTATE; inv MASSOC; + assert (X: Ple p (max_reg_function f)) by eauto; + apply H in X; + rewrite Heqv in X; + inv X; auto]). + Qed. + + Lemma eval_cond_correct' : + forall e stk f sp pc rs m res ml st asr asa v f' args cond pr, + match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) -> + (forall v, In v args -> Ple v (max_reg_function f)) -> + Values.Val.of_optbool None = v -> + translate_condition cond args = OK e -> + exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. + Proof. + intros * MSTATE MAX_FUN EVAL TR_INSTR. + unfold translate_condition, translate_comparison, translate_comparisonu, + translate_comparison_imm, translate_comparison_immu, bop, boplit in *. + repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor. + Qed. + + Ltac eval_correct_tac := + match goal with + | |- context[valueToPtr] => unfold valueToPtr + | |- context[valueToInt] => unfold valueToInt + | |- context[bop] => unfold bop + | H : context[bop] |- _ => unfold bop in H + | |- context[boplit] => unfold boplit + | H : context[boplit] |- _ => unfold boplit in H + | |- context[boplitz] => unfold boplitz + | H : context[boplitz] |- _ => unfold boplitz in H + | |- val_value_lessdef Values.Vundef _ => solve [constructor] + | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H + | |- val_value_lessdef (Values.Vint _) _ => constructor; auto + | H : ret _ _ = OK _ _ _ |- _ => inv H + | H : _ :: _ = _ :: _ |- _ => inv H + | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate + | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H + | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H + | |- Verilog.expr_runp _ _ _ ?f _ => + match f with + | Verilog.Vternary _ _ _ => idtac + | _ => econstructor + end + | |- val_value_lessdef (?f _ _) _ => unfold f + | |- val_value_lessdef (?f _) _ => unfold f + | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H) + | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _ + |- _ => rewrite H1 in H2; inv H2 + | |- _ => eexists; split; try constructor; solve [eauto] + | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate + | H : ?b = _ |- _ = boolToValue ?b => rewrite H + end. + + Lemma eval_correct_Oshrximm : + forall sp rs m v e asr asa f f' stk pc args res ml st n pr, + match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) -> + Forall (fun x => (Ple x (max_reg_function f))) args -> + Op.eval_operation ge sp (Op.Oshrximm n) + (List.map (fun r : BinNums.positive => + Registers.Regmap.get r rs) args) m = Some v -> + translate_instr (Op.Oshrximm n) args = OK e -> + exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. + Proof. + intros * MSTATE INSTR EVAL TR_INSTR. + pose proof MSTATE as MSTATE_2. inv MSTATE. + inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; + unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL. + (*repeat (simplify; eval_correct_tac; unfold valueToInt in * ). + destruct (Z_lt_ge_dec (Int.signed i0) 0). + econstructor.*) + unfold Values.Val.shrx in *. + destruct v0; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:?; try discriminate. + inversion H1. clear H1. + assert (Int.unsigned n <= 30). + { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate. + rewrite Int.unsigned_repr in l by (simplify; lia). + replace 31 with (Z.succ 30) in l by auto. + apply Zlt_succ_le in l. + auto. + } + rewrite IntExtra.shrx_shrx_alt_equiv in H2 by auto. + unfold IntExtra.shrx_alt in *. + destruct (zlt (Int.signed i) 0). + - repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue; + repeat (simplify; eval_correct_tac). + unfold valueToInt in *. inv INSTR. apply H in H4. rewrite H3 in H4. + inv H4. clear H5. + unfold Int.lt in *. rewrite zlt_true in Heqb0. simplify. + rewrite Int.unsigned_repr in Heqb0. discriminate. + simplify; lia. + unfold ZToValue. rewrite Int.signed_repr by (simplify; lia). + auto. + rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_true; try lia. + simplify. inv INSTR. clear H5. apply H in H4. rewrite H3 in H4. inv H4. auto. + - econstructor; econstructor; [eapply Verilog.erun_Vternary_false|idtac]; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue; + repeat (simplify; eval_correct_tac). + inv INSTR. clear H5. apply H in H4. rewrite H3 in H4. + inv H4. + unfold Int.lt in *. rewrite zlt_false in Heqb0. simplify. + rewrite Int.unsigned_repr in Heqb0. lia. + simplify; lia. + unfold ZToValue. rewrite Int.signed_repr by (simplify; lia). + auto. + rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_false; try lia. + simplify. inv INSTR. apply H in H4. unfold valueToInt in *. rewrite H3 in H4. inv H4. auto. + Qed. + + Lemma max_reg_function_use: + forall l y m, + Forall (fun x => Ple x m) l -> + In y l -> + Ple y m. + Proof. + intros. eapply Forall_forall in H; eauto. + Qed. + + Ltac eval_correct_tac' := + match goal with + | |- context[valueToPtr] => unfold valueToPtr + | |- context[valueToInt] => unfold valueToInt + | |- context[bop] => unfold bop + | H : context[bop] |- _ => unfold bop in H + | |- context[boplit] => unfold boplit + | H : context[boplit] |- _ => unfold boplit in H + | |- context[boplitz] => unfold boplitz + | H : context[boplitz] |- _ => unfold boplitz in H + | |- val_value_lessdef Values.Vundef _ => solve [constructor] + | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H + | |- val_value_lessdef (Values.Vint _) _ => constructor; auto + | H : ret _ _ = OK _ _ _ |- _ => inv H + | H : context[max_reg_function ?f] + |- context[_ (Registers.Regmap.get ?r ?rs) (Registers.Regmap.get ?r0 ?rs)] => + let HPle1 := fresh "HPle" in + let HPle2 := fresh "HPle" in + assert (HPle1 : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto])); + assert (HPle2 : Ple r0 (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto])); + apply H in HPle1; apply H in HPle2; eexists; split; + [econstructor; eauto; constructor; trivial | inv HPle1; inv HPle2; try (constructor; auto)] + | H : context[max_reg_function ?f] + |- context[_ (Registers.Regmap.get ?r ?rs) _] => + let HPle1 := fresh "HPle" in + assert (HPle1 : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto])); + apply H in HPle1; eexists; split; + [econstructor; eauto; constructor; trivial | inv HPle1; try (constructor; auto)] + | H : _ :: _ = _ :: _ |- _ => inv H + | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate + | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H + | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H + | |- Verilog.expr_runp _ _ _ ?f _ => + match f with + | Verilog.Vternary _ _ _ => idtac + | _ => econstructor + end + | |- val_value_lessdef (?f _ _) _ => unfold f + | |- val_value_lessdef (?f _) _ => unfold f + | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H) + | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _ + |- _ => rewrite H1 in H2; inv H2 + | |- _ => eexists; split; try constructor; solve [eauto] + | H : context[max_reg_function ?f] |- context[_ (Verilog.Vvar ?r) (Verilog.Vvar ?r0)] => + let HPle1 := fresh "H" in + let HPle2 := fresh "H" in + assert (HPle1 : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto])); + assert (HPle2 : Ple r0 (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto])); + apply H in HPle1; apply H in HPle2; eexists; split; try constructor; eauto + | H : context[max_reg_function ?f] |- context[Verilog.Vvar ?r] => + let HPle := fresh "H" in + assert (HPle : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto])); + apply H in HPle; eexists; split; try constructor; eauto + | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate + | H : ?b = _ |- _ = boolToValue ?b => rewrite H + end. + + Lemma int_unsigned_lt_ptrofs_max : + forall a, + 0 <= Int.unsigned a <= Ptrofs.max_unsigned. + Proof. + intros. pose proof (Int.unsigned_range_2 a). + assert (Int.max_unsigned = Ptrofs.max_unsigned) by auto. + lia. + Qed. + + Lemma ptrofs_unsigned_lt_int_max : + forall a, + 0 <= Ptrofs.unsigned a <= Int.max_unsigned. + Proof. + intros. pose proof (Ptrofs.unsigned_range_2 a). + assert (Int.max_unsigned = Ptrofs.max_unsigned) by auto. + lia. + Qed. + + Hint Resolve int_unsigned_lt_ptrofs_max : int_ptrofs. + Hint Resolve ptrofs_unsigned_lt_int_max : int_ptrofs. + Hint Resolve Ptrofs.unsigned_range_2 : int_ptrofs. + Hint Resolve Int.unsigned_range_2 : int_ptrofs. + +(* Ptrofs.agree32_of_int_eq: forall (a : ptrofs) (b : int), Ptrofs.agree32 a b -> Ptrofs.of_int b = a *) +(* Ptrofs.agree32_of_int: Archi.ptr64 = false -> forall b : int, Ptrofs.agree32 (Ptrofs.of_int b) b *) +(* Ptrofs.agree32_sub: *) +(* Archi.ptr64 = false -> *) +(* forall (a1 : ptrofs) (b1 : int) (a2 : ptrofs) (b2 : int), *) +(* Ptrofs.agree32 a1 b1 -> Ptrofs.agree32 a2 b2 -> Ptrofs.agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2) *) + Lemma eval_correct_sub : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.sub a b) (Int.sub a' b'). + Proof. + intros * HPLE HPLE0. + assert (ARCHI: Archi.ptr64 = false) by auto. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto]. + - rewrite ARCHI. constructor. unfold valueToPtr. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr; auto with int_ptrofs. + apply Ptrofs.agree32_sub; auto; rewrite <- Int.repr_unsigned; now apply Ptrofs.agree32_repr. + - rewrite ARCHI. destruct_match; constructor. + unfold Ptrofs.to_int. unfold valueToInt. + apply int_inj. rewrite Int.unsigned_repr; auto with int_ptrofs. + apply Ptrofs.agree32_sub; auto; unfold valueToPtr; now apply Ptrofs.agree32_of_int. + Qed. + + Lemma eval_correct_mul : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.mul a b) (Int.mul a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_mul' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.mul a (Values.Vint n)) (Int.mul a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_and : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.and a b) (Int.and a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_and' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.and a (Values.Vint n)) (Int.and a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_or : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.or a b) (Int.or a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_or' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.or a (Values.Vint n)) (Int.or a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_xor : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.xor a b) (Int.xor a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_xor' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.xor a (Values.Vint n)) (Int.xor a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto]. + Qed. + + Lemma eval_correct_shl : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.shl a b) (Int.shl a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try destruct_match; now constructor. + Qed. + + Lemma eval_correct_shl' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.shl a (Values.Vint n)) (Int.shl a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try destruct_match; now constructor. + Qed. + + Lemma eval_correct_shr : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.shr a b) (Int.shr a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try destruct_match; now constructor. + Qed. + + Lemma eval_correct_shr' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.shr a (Values.Vint n)) (Int.shr a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try destruct_match; now constructor. + Qed. + + Lemma eval_correct_shru : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.shru a b) (Int.shru a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try destruct_match; now constructor. + Qed. + + Lemma eval_correct_shru' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.shru a (Values.Vint n)) (Int.shru a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try destruct_match; now constructor. + Qed. + + Lemma eval_correct_add : + forall a b a' b', + val_value_lessdef a a' -> + val_value_lessdef b b' -> + val_value_lessdef (Values.Val.add a b) (Int.add a' b'). + Proof. + intros * HPLE HPLE0. + inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; + try destruct_match; constructor; auto; unfold valueToPtr; + unfold Ptrofs.of_int; apply ptrofs_inj; + rewrite Ptrofs.unsigned_repr by auto with int_ptrofs; + [rewrite Int.add_commut|]; apply Ptrofs.agree32_add; auto; + rewrite <- Int.repr_unsigned; now apply Ptrofs.agree32_repr. + Qed. + + Lemma eval_correct_add' : + forall a a' n, + val_value_lessdef a a' -> + val_value_lessdef (Values.Val.add a (Values.Vint n)) (Int.add a' (intToValue n)). + Proof. + intros * HPLE. + inv HPLE; cbn in *; unfold valueToInt; try destruct_match; try constructor; auto. + unfold valueToPtr. apply ptrofs_inj. unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr by auto with int_ptrofs. + apply Ptrofs.agree32_add; auto. rewrite <- Int.repr_unsigned. + apply Ptrofs.agree32_repr; auto. + unfold intToValue. rewrite <- Int.repr_unsigned. + apply Ptrofs.agree32_repr; auto. + Qed. + + Lemma eval_correct : + forall sp op rs m v e asr asa f f' stk pc args res ml st pr, + match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) -> + Forall (fun x => (Ple x (max_reg_function f))) args -> + Op.eval_operation ge sp op + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> + translate_instr op args = OK e -> + exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. + Proof. + intros * MSTATE INSTR EVAL TR_INSTR. + pose proof MSTATE as MSTATE_2. inv MSTATE. + inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; + unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL; + repeat (simplify; eval_correct_tac; unfold valueToInt in *); + repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR)); + try (apply H in HPLE); try (apply H in HPLE0). + - do 2 econstructor; eauto. repeat econstructor. + - do 2 econstructor; eauto. repeat econstructor. cbn. + inv HPLE; cbn; try solve [constructor]; unfold valueToInt in *. + constructor; unfold valueToInt; auto. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_sub. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul'. + - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + do 2 econstructor; eauto. repeat econstructor. unfold binop_run. + rewrite Heqb. auto. constructor; auto. + - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + do 2 econstructor; eauto. repeat econstructor. unfold binop_run. + rewrite Heqb. auto. constructor; auto. + - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + do 2 econstructor; eauto. repeat econstructor. unfold binop_run. + rewrite Heqb. auto. constructor; auto. + - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *. + do 2 econstructor; eauto. repeat econstructor. unfold binop_run. + rewrite Heqb. auto. constructor; auto. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_and. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_and'. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_or. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_or'. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_xor. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_xor'. + - do 2 econstructor; eauto. repeat econstructor. cbn. inv HPLE; now constructor. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl'. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr'. + - inv H1. rewrite Heqv0 in HPLE. inv HPLE. + assert (0 <= 31 <= Int.max_unsigned). + { pose proof Int.two_wordsize_max_unsigned as Y. + unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize in Y. lia. } + assert (Int.unsigned n <= 30). + { unfold Int.ltu in Heqb. destruct_match; try discriminate. + clear Heqs. rewrite Int.unsigned_repr in l by auto. lia. } + rewrite IntExtra.shrx_shrx_alt_equiv by auto. + case_eq (Int.lt (asr # p) (ZToValue 0)); intros HLT. + + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = true). + { destruct_match; auto; unfold valueToInt in *. exfalso. + assert (Int.signed asr # p < 0 -> False) by auto. apply H2. unfold Int.lt in HLT. + destruct_match; try discriminate. auto. } + destruct_match; try discriminate. + do 2 econstructor; eauto. repeat econstructor. now rewrite HLT. + constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto. + + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = false). + { destruct_match; auto; unfold valueToInt in *. exfalso. + assert (Int.signed asr # p >= 0 -> False) by auto. apply H2. unfold Int.lt in HLT. + destruct_match; try discriminate. auto. } + destruct_match; try discriminate. + do 2 econstructor; eauto. eapply erun_Vternary_false; repeat econstructor. + now rewrite HLT. + constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru. + - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru'. + - unfold translate_eff_addressing in H1. + repeat (destruct_match; try discriminate); unfold boplitz in *; simplify; + repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR)); + try (apply H in HPLE); try (apply H in HPLE0). + + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + now apply eval_correct_add'. + + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + apply eval_correct_add; auto. apply eval_correct_add; auto. + constructor; auto. + + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + apply eval_correct_add; try constructor; auto. + apply eval_correct_mul; try constructor; auto. + + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + apply eval_correct_add; try constructor; auto. + apply eval_correct_add; try constructor; auto. + apply eval_correct_mul; try constructor; auto. + + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + assert (X: Archi.ptr64 = false) by auto. + rewrite X in H2. inv H2. + constructor. unfold valueToPtr. unfold Ptrofs.of_int. + rewrite Int.unsigned_repr by auto with int_ptrofs. + rewrite Ptrofs.repr_unsigned. apply Ptrofs.add_zero_l. + - remember (Op.eval_condition cond (List.map (fun r : positive => rs !! r) args) m). + destruct o. cbn. symmetry in Heqo. + exploit eval_cond_correct; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto. + intros. econstructor. split. eauto. destruct b; constructor; auto. + exploit eval_cond_correct'; eauto. + intros. apply Forall_forall with (x := v) in INSTR; auto. + - assert (HARCHI: Archi.ptr64 = false) by auto. + unfold Errors.bind in *. destruct_match; try discriminate; []. inv H1. + remember (Op.eval_condition c (List.map (fun r : positive => rs !! r) l0) m). + destruct o; cbn; symmetry in Heqo. + + exploit eval_cond_correct; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto. + intros. destruct b. + * intros. econstructor. split. econstructor. eauto. econstructor; auto. auto. + unfold Values.Val.normalize. rewrite HARCHI. destruct_match; auto; constructor. + * intros. econstructor. split. eapply erun_Vternary_false; repeat econstructor. eauto. auto. + unfold Values.Val.normalize. rewrite HARCHI. destruct_match; auto; constructor. + + exploit eval_cond_correct'; eauto. + intros. apply Forall_forall with (x := v) in INSTR; auto. simplify. + case_eq (valueToBool x); intros HVALU. + * econstructor. econstructor. econstructor. eauto. constructor. eauto. auto. constructor. + * econstructor. econstructor. eapply erun_Vternary_false. eauto. constructor. eauto. auto. constructor. + Qed. diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index d4bc80a..7786c5d 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -161,6 +161,8 @@ Section PRED_DEFINITION. End PRED_DEFINITION. +Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p. + Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op. Notation "A ∨ B" := (Por A B) (at level 25) : pred_op. Notation "⟂" := (Pfalse) : pred_op. |