diff options
Diffstat (limited to 'src/hls/DHTLgenproof0.v')
| -rw-r--r-- | src/hls/DHTLgenproof0.v | 2016 |
1 files changed, 2016 insertions, 0 deletions
diff --git a/src/hls/DHTLgenproof0.v b/src/hls/DHTLgenproof0.v new file mode 100644 index 0000000..fa467eb --- /dev/null +++ b/src/hls/DHTLgenproof0.v @@ -0,0 +1,2016 @@ +(* + * 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.GibleSubPar. +Require Import vericert.hls.DHTLgen. +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 Opaque Int.max_unsigned. + +#[export] Hint Resolve AssocMap.gss : htlproof. +#[export] Hint Resolve AssocMap.gso : htlproof. + +#[export] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. + +Definition get_mem n r := + Option.default (NToValue 0) (Option.join (array_get_error n r)). + +Inductive match_assocmaps : positive -> positive -> Gible.regset -> Gible.predset -> assocmap -> Prop := + match_assocmap : forall rs pr am max_reg max_pred, + (forall r, Ple r max_reg -> + val_value_lessdef (Registers.Regmap.get r rs) (find_assocmap 32 (reg_enc r) am)) -> + (forall r, Ple r max_pred -> + find_assocmap 1 (pred_enc r) am = boolToValue (PMap.get r pr)) -> + match_assocmaps max_reg max_pred rs pr am. +#[export] Hint Constructors match_assocmaps : htlproof. + +Inductive match_arrs (stack_size: Z) (stk: positive) (stk_len: nat) (sp : Values.val) (mem : mem) : + Verilog.assocmap_arr -> Prop := +| match_arr : forall asa stack, + asa ! stk = Some stack /\ + stack.(arr_length) = Z.to_nat (stack_size / 4) /\ + stack.(arr_length) = stk_len /\ + (forall ptr, + 0 <= ptr < Z.of_nat stack.(arr_length) -> + opt_val_value_lessdef (Mem.loadv AST.Mint32 mem + (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr)))) + (get_mem (Z.to_nat ptr) stack)) -> + match_arrs stack_size stk stk_len 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 GibleSubPar.stackframe -> list DHTL.stackframe -> Prop := +| match_frames_nil : + match_frames nil nil. + +Inductive match_constants (rst fin: reg) (asr: assocmap) : Prop := + match_constant : + asr!rst = Some (ZToValue 0) -> + asr!fin = Some (ZToValue 0) -> + match_constants rst fin asr. + +Definition state_st_wf (asr: assocmap) (st_reg: reg) (st: positive) := + asr!st_reg = Some (posToValue st). +#[export] Hint Unfold state_st_wf : htlproof. + +Inductive match_states : GibleSubPar.state -> DHTL.state -> Prop := +| match_state : forall asa asr sf f sp sp' rs mem m st res ps + (MASSOC : match_assocmaps (max_reg_function f) (max_pred_function f) rs ps asr) + (TF : transl_module f = Errors.OK m) + (WF : state_st_wf asr m.(DHTL.mod_st) st) + (MF : match_frames sf res) + (MARR : match_arrs f.(fn_stacksize) m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) 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.(GibleSubPar.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(GibleSubPar.fn_stacksize)) mem) + (CONST : match_constants m.(DHTL.mod_reset) m.(DHTL.mod_finish) asr), + (* Add a relation about ps compared with the state register. *) + match_states (GibleSubPar.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 (GibleSubPar.Returnstate stack v mem) (DHTL.Returnstate res v') +| match_initial_call : + forall f m m0 + (TF : transl_module f = Errors.OK m), + match_states (GibleSubPar.Callstate nil (AST.Internal f) nil m0) (DHTL.Callstate nil m nil). +#[export] Hint Constructors match_states : htlproof. + +Inductive match_states_reduced : nat -> GibleSubPar.state -> DHTL.state -> Prop := +| match_states_reduced_intro : forall asa asr sf f sp sp' rs mem m st res ps n + (MASSOC : match_assocmaps (max_reg_function f) (max_pred_function f) rs ps asr) + (TF : transl_module f = Errors.OK m) + (WF : state_st_wf asr m.(DHTL.mod_st) (Pos.of_nat (Pos.to_nat st - n)%nat)) + (MF : match_frames sf res) + (MARR : match_arrs f.(fn_stacksize) m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) 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.(GibleSubPar.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(GibleSubPar.fn_stacksize)) mem) + (CONST : match_constants m.(DHTL.mod_reset) m.(DHTL.mod_finish) asr), + (* Add a relation about ps compared with the state register. *) + match_states_reduced n (GibleSubPar.State sf f sp st rs ps mem) + (DHTL.State res m (Pos.of_nat (Pos.to_nat st - n)%nat) asr asa). + +Definition match_prog (p: GibleSubPar.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: GibleSubPar.program -> Errors.res DHTL.program): + TransfLink (fun (p1: GibleSubPar.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: GibleSubPar.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, 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 max_reg_lt_resource : + forall f n, + Plt (max_resource_function f) n -> + Plt (reg_enc (max_reg_function f)) n. +Proof. + unfold max_resource_function, Plt, reg_enc, pred_enc in *; intros. lia. +Qed. + +Lemma max_pred_lt_resource : + forall f n, + Plt (max_resource_function f) n -> + Plt (pred_enc (max_pred_function f)) n. +Proof. + unfold max_resource_function, Plt, reg_enc, pred_enc in *; intros. lia. +Qed. + +Lemma plt_reg_enc : + forall a b, Ple a b -> Ple (reg_enc a) (reg_enc b). +Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed. + +Lemma plt_pred_enc : + forall a b, Ple a b -> Ple (pred_enc a) (pred_enc b). +Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed. + +Lemma reg_enc_inj : + forall a b, reg_enc a = reg_enc b -> a = b. +Proof. unfold reg_enc; intros; lia. Qed. + +Lemma pred_enc_inj : + forall a b, pred_enc a = pred_enc b -> a = b. +Proof. unfold pred_enc; intros; lia. Qed. + +(* Lemma regs_lessdef_add_greater : *) +(* forall n m rs1 ps1 rs2 n v, *) +(* Plt (max_resource_function f) n -> *) +(* match_assocmaps n m rs1 ps1 rs2 -> *) +(* match_assocmaps n m rs1 ps1 (AssocMap.set n v rs2). *) +(* Proof. *) +(* inversion 2; subst. *) +(* intros. constructor. *) +(* - apply max_reg_lt_resource in H. intros. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gso. eauto. apply plt_reg_enc in H3. unfold Ple, Plt in *. lia. *) +(* - apply max_pred_lt_resource in H. intros. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite AssocMap.gso. eauto. apply plt_pred_enc in H3. unfold Ple, Plt in *. lia. *) +(* Qed. *) +(* #[export] Hint Resolve regs_lessdef_add_greater : htlproof. *) + +Lemma pred_enc_reg_enc_ne : + forall a b, pred_enc a <> reg_enc b. +Proof. unfold not, pred_enc, reg_enc; lia. Qed. + +Lemma regs_lessdef_add_match : + forall m n rs ps am r v v', + val_value_lessdef v v' -> + match_assocmaps m n rs ps am -> + match_assocmaps m n (Registers.Regmap.set r v rs) ps (AssocMap.set (reg_enc 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. unfold not in *; intros; apply n0. apply reg_enc_inj; auto. + + intros. pose proof (pred_enc_reg_enc_ne r0 r) as HNE. + rewrite assocmap_gso by auto. now apply H2. +Qed. +#[export] 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 n m l, + match_assocmaps n m (Gible.init_regs nil l) (PMap.init false) (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. + + - 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. +#[export] Hint Resolve arr_lookup_some : htlproof. + +Lemma regs_lessdef_add_greater : + forall f rs1 rs2 ps n v, + Plt (max_resource_function f) n -> + match_assocmaps (max_reg_function f) (max_pred_function f) rs1 ps rs2 -> + match_assocmaps (max_reg_function f) (max_pred_function f) rs1 ps (AssocMap.set n v rs2). +Proof. + inversion 2; subst. + intros. constructor. + intros. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso. eauto. + eapply plt_reg_enc in H3. unfold Plt, Ple, max_resource_function in *. lia. + intros. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso. eauto. + eapply plt_pred_enc in H3. unfold Plt, Ple, max_resource_function in *. lia. +Qed. +#[export] Hint Resolve regs_lessdef_add_greater : htlproof. + +Ltac destr := destruct_match; try discriminate; []. + +Lemma pred_in_pred_uses: + forall A (p: A) pop, + PredIn p pop -> + In p (predicate_use pop). +Proof. + induction pop; crush. + - destr. inv Heqp1. inv H. now constructor. + - inv H. + - inv H. + - apply in_or_app. inv H. inv H1; intuition. + - apply in_or_app. inv H. inv H1; intuition. +Qed. + +Lemma le_max_pred : + forall p max_pred, + Forall (fun x : positive => Ple x max_pred) (predicate_use p) -> + Ple (max_predicate p) max_pred. +Proof. + induction p; intros. + - intros; cbn. destruct_match. inv Heqp0. cbn in *. now inv H. + - cbn. unfold Ple. lia. + - cbn. unfold Ple. lia. + - cbn in *. eapply Forall_app in H. inv H. unfold Ple in *. eapply IHp1 in H0. + eapply IHp2 in H1. lia. + - cbn in *. eapply Forall_app in H. inv H. unfold Ple in *. eapply IHp1 in H0. + eapply IHp2 in H1. lia. +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. + +Lemma all_le_max_predicate_instr : + forall n ctrl bb curr_p stmnt next_p stmnt' max, + transf_instr n ctrl (curr_p, stmnt) bb = OK (next_p, stmnt') -> + Forall (fun x : positive => Ple x max) (pred_uses bb) -> + Ple (max_predicate curr_p) max -> + Ple (max_predicate next_p) max. +Proof. Admitted. + +Lemma all_le_max_predicate : + forall n ctrl bb curr_p stmnt next_p stmnt' max, + mfold_left (transf_instr n ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') -> + Forall (fun i0 : instr => Forall (fun x : positive => Ple x max) (pred_uses i0)) bb -> + Ple (max_predicate curr_p) max -> + Ple (max_predicate next_p) max. +Proof. Admitted. + +Lemma ple_max_resource_function: + forall f r, + Ple r (max_reg_function f) -> + Ple (reg_enc r) (max_resource_function f). +Proof. + intros * Hple. + unfold max_resource_function, reg_enc, Ple in *. lia. +Qed. + +Lemma ple_pred_max_resource_function: + forall f r, + Ple r (max_pred_function f) -> + Ple (pred_enc r) (max_resource_function f). +Proof. + intros * Hple. + unfold max_resource_function, pred_enc, Ple in *. lia. +Qed. + +Lemma mfold_left_error: + forall A B f l m, @mfold_left A B f l (Error m) = Error m. +Proof. now induction l. Qed. + +Lemma mfold_left_cons: + forall A B f a l x y, + @mfold_left A B f (a :: l) x = OK y -> + exists x' y', @mfold_left A B f l (OK y') = OK y /\ f x' a = OK y' /\ x = OK x'. +Proof. + intros. + destruct x; [|now rewrite mfold_left_error in H]. + cbn in H. + replace (fold_left (fun (a : mon A) (b : B) => bind (fun a' : A => f a' b) a) l (f a0 a) = OK y) with + (mfold_left f l (f a0 a) = OK y) in H by auto. + destruct (f a0 a) eqn:?; [|now rewrite mfold_left_error in H]. + eauto. +Qed. + +Lemma mfold_left_app: + forall A B f a l x y, + @mfold_left A B f (a ++ l) x = OK y -> + exists y', @mfold_left A B f a x = OK y' /\ @mfold_left A B f l (OK y') = OK y. +Proof. + induction a. + - intros. destruct x; [|now rewrite mfold_left_error in H]. exists a. eauto. + - intros. destruct x; [|now rewrite mfold_left_error in H]. rewrite <- app_comm_cons in H. + exploit mfold_left_cons; eauto. +Qed. + +Section CORRECTNESS. + + Variable prog : GibleSubPar.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 : GibleSubPar.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: GibleSubPar.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: GibleSubPar.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 (GibleSubPar.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 (GibleSubPar.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 (GibleSubPar.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 H2. clear H2. + 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 H3 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 H5. rewrite H4 in H5. + inv H5. clear H6. + 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 H6. apply H in H5. rewrite H4 in H5. inv H5. auto. + - econstructor; econstructor; [eapply Verilog.erun_Vternary_false|idtac]; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue; + repeat (simplify; eval_correct_tac). + inv INSTR. clear H6. apply H in H5. rewrite H4 in H5. + inv H5. + 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 H5. unfold valueToInt in *. rewrite H4 in H5. inv H5. auto. + 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 (GibleSubPar.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 H2. 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 H2. 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 H2. 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 H2. 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 H2. 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 (find_assocmap 32 (reg_enc p) asr) (ZToValue 0)); intros HLT. + + assert ((if zlt (Int.signed (valueToInt (find_assocmap 32 (reg_enc p) asr))) 0 then true else false) = true). + { destruct_match; auto; unfold valueToInt in *. exfalso. + assert (Int.signed (find_assocmap 32 (reg_enc p) asr) < 0 -> False) by auto. apply H3. 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 (find_assocmap 32 (reg_enc p) asr))) 0 then true else false) = false). + { destruct_match; auto; unfold valueToInt in *. exfalso. + assert (Int.signed (find_assocmap 32 (reg_enc p) asr) >= 0 -> False) by auto. apply H3. 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 H2. + 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 H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + now apply eval_correct_add'. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + apply eval_correct_add; auto. apply eval_correct_add; auto. + constructor; auto. + + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + apply eval_correct_add; try constructor; auto. + apply eval_correct_mul; try constructor; auto. + + inv H2. 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 H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue. + assert (X: Archi.ptr64 = false) by auto. + rewrite X in H3. inv H3. + 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 H2. + 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. + +Ltac name_goal name := refine ?[name]. + +Ltac unfold_merge := + unfold merge_assocmap; repeat (rewrite AssocMapExt.merge_add_assoc); + try (rewrite AssocMapExt.merge_base_1). + + Lemma match_assocmaps_merge_empty: + forall n m rs ps ars, + match_assocmaps n m rs ps ars -> + match_assocmaps n m rs ps (AssocMapExt.merge value empty_assocmap ars). + Proof. + inversion 1; subst; clear H. + constructor; intros. + rewrite merge_get_default2 by auto. auto. + rewrite merge_get_default2 by auto. auto. + Qed. + + Lemma match_constants_merge_empty: + forall n m ars, + match_constants n m ars -> + match_constants n m (AssocMapExt.merge value empty_assocmap ars). + Proof. + inversion 1. constructor; unfold AssocMapExt.merge. + - rewrite PTree.gcombine; auto. + - rewrite PTree.gcombine; auto. + Qed. + + Lemma match_state_st_wf_empty: + forall asr st pc, + state_st_wf asr st pc -> + state_st_wf (AssocMapExt.merge value empty_assocmap asr) st pc. + Proof. + unfold state_st_wf; intros. + unfold AssocMapExt.merge. rewrite AssocMap.gcombine by auto. rewrite H. + rewrite AssocMap.gempty. auto. + Qed. + + Lemma match_arrs_merge_empty: + forall sz stk stk_len sp mem asa, + match_arrs sz stk stk_len sp mem asa -> + match_arrs sz stk stk_len sp mem (merge_arrs (DHTL.empty_stack stk stk_len) asa). + Proof. + inversion 1. inv H0. inv H3. inv H1. destruct stack. econstructor; unfold AssocMapExt.merge. + split; [|split]; [| |split]; cbn in *. + - unfold merge_arrs in *. rewrite AssocMap.gcombine by auto. + setoid_rewrite H2. unfold DHTL.empty_stack. rewrite AssocMap.gss. + cbn in *. eauto. + - cbn. rewrite list_combine_length. rewrite list_repeat_len. lia. + - cbn. rewrite list_combine_length. rewrite list_repeat_len. lia. + - cbn; intros. + assert ((Datatypes.length (list_combine merge_cell (list_repeat None arr_length) arr_contents)) = arr_length). + { rewrite list_combine_length. rewrite list_repeat_len. lia. } + rewrite H3 in H1. apply H4 in H1. + inv H1; try constructor. + assert (array_get_error (Z.to_nat ptr) + {| arr_contents := arr_contents; arr_length := Datatypes.length arr_contents; arr_wf := eq_refl |} = + (array_get_error (Z.to_nat ptr) + (combine merge_cell (arr_repeat None (Datatypes.length arr_contents)) + {| arr_contents := arr_contents; arr_length := Datatypes.length arr_contents; arr_wf := eq_refl |}))). + { apply array_get_error_equal; auto. cbn. now rewrite list_combine_none. } + unfold get_mem in *. + rewrite <- H1. auto. + Qed. + + Lemma match_states_merge_empty : + forall st f sp pc rs ps m st' modle asr asa, + match_states (GibleSubPar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr asa) -> + match_states (GibleSubPar.State st f sp pc rs ps m) (DHTL.State st' modle pc (AssocMapExt.merge value empty_assocmap asr) asa). + Proof. + inversion 1; econstructor; eauto using match_assocmaps_merge_empty, + match_constants_merge_empty, match_state_st_wf_empty. + Qed. + + Lemma match_states_merge_empty_arr : + forall st f sp pc rs ps m st' modle asr asa, + match_states (GibleSubPar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr asa) -> + match_states (GibleSubPar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr (merge_arrs (DHTL.empty_stack modle.(DHTL.mod_stk) modle.(DHTL.mod_stk_len)) asa)). + Proof. inversion 1; econstructor; eauto using match_arrs_merge_empty. Qed. + + Lemma match_states_merge_empty_all : + forall st f sp pc rs ps m st' modle asr asa, + match_states (GibleSubPar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr asa) -> + match_states (GibleSubPar.State st f sp pc rs ps m) (DHTL.State st' modle pc (AssocMapExt.merge value empty_assocmap asr) (merge_arrs (DHTL.empty_stack modle.(DHTL.mod_stk) modle.(DHTL.mod_stk_len)) asa)). + Proof. eauto using match_states_merge_empty, match_states_merge_empty_arr. Qed. + + Opaque AssocMap.get. + Opaque AssocMap.set. + Opaque AssocMapExt.merge. + Opaque Verilog.merge_arr. + + Lemma match_assocmaps_ext : + forall n m rs ps ars1 ars2, + (forall x, Ple x n -> ars1 ! (reg_enc x) = ars2 ! (reg_enc x)) -> + (forall x, Ple x m -> ars1 ! (pred_enc x) = ars2 ! (pred_enc x)) -> + match_assocmaps n m rs ps ars1 -> + match_assocmaps n m rs ps ars2. + Proof. + intros * YFRL YFRL2 YMATCH. + inv YMATCH. constructor; intros x' YPLE. + unfold "#", AssocMapExt.get_default in *. + rewrite <- YFRL by auto. eauto. + unfold "#", AssocMapExt.get_default. rewrite <- YFRL2 by auto. eauto. + Qed. + + Definition e_assoc asr : reg_associations := mkassociations asr (AssocMap.empty _). + Definition e_assoc_arr stk stk_len asr : arr_associations := mkassociations asr (DHTL.empty_stack stk stk_len). + + Lemma option_inv : + forall A x y, + @Some A x = Some y -> x = y. + Proof. intros. inversion H. trivial. Qed. + + Lemma main_tprog_internal : + forall b, + Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> + exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). + Proof. + intros. + destruct TRANSL. unfold main_is_internal in H1. + repeat (unfold_match H1). replace b with b0. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. + unfold_match B. inv B. econstructor. apply A. + + apply option_inv. rewrite <- Heqo. rewrite <- H. + rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). + trivial. symmetry; eapply Linking.match_program_main; eauto. + Qed. + + Lemma transl_initial_states : + forall s1 : Smallstep.state (GibleSubPar.semantics prog), + Smallstep.initial_state (GibleSubPar.semantics prog) s1 -> + exists s2 : Smallstep.state (DHTL.semantics tprog), + Smallstep.initial_state (DHTL.semantics tprog) s2 /\ match_states s1 s2. + Proof. + induction 1. + destruct TRANSL. unfold main_is_internal in H4. + repeat (unfold_match H4). + assert (f = AST.Internal f1). apply option_inv. + rewrite <- Heqo0. rewrite <- H1. replace b with b0. + auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. + trivial. + exploit function_ptr_translated; eauto. + intros [tf [A B]]. + unfold transl_fundef, Errors.bind in B. + unfold AST.transf_partial_fundef, Errors.bind in B. + repeat (unfold_match B). inversion B. subst. + exploit main_tprog_internal; eauto; intros. + rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). + apply Heqo. symmetry; eapply Linking.match_program_main; eauto. + inversion H5. + econstructor; split. econstructor. + apply (Genv.init_mem_transf_partial TRANSL'); eauto. + replace (AST.prog_main tprog) with (AST.prog_main prog). + rewrite symbols_preserved; eauto. + symmetry; eapply Linking.match_program_main; eauto. + apply H6. + + constructor. inv B. + assert (Some (AST.Internal x) = Some (AST.Internal m)). + replace (AST.fundef DHTL.module) with (DHTL.fundef). + rewrite <- H6. setoid_rewrite <- A. trivial. + trivial. inv H7. assumption. + Qed. + #[local] Hint Resolve transl_initial_states : htlproof. + + Lemma transl_final_states : + forall (s1 : Smallstep.state (GibleSubPar.semantics prog)) + (s2 : Smallstep.state (DHTL.semantics tprog)) + (r : Integers.Int.int), + match_states s1 s2 -> + Smallstep.final_state (GibleSubPar.semantics prog) s1 r -> + Smallstep.final_state (DHTL.semantics tprog) s2 r. + Proof. + intros. inv H0. inv H. inv H4. inv MF. constructor. reflexivity. + Qed. + #[local] Hint Resolve transl_final_states : htlproof. + + Lemma stack_correct_inv : + forall s, + stack_correct s = true -> + (0 <= s) /\ (s < Ptrofs.modulus) /\ (s mod 4 = 0). + Proof. + unfold stack_correct; intros. + crush. + Qed. + + Lemma init_regs_empty: + forall l, init_regs nil l = (Registers.Regmap.init Values.Vundef). + Proof. destruct l; auto. Qed. + + Lemma dhtl_init_regs_empty: + forall l, DHTL.init_regs nil l = (AssocMap.empty _). + Proof. destruct l; auto. Qed. + +Lemma assocmap_gempty : + forall n a, + find_assocmap n a (AssocMap.empty _) = ZToValue 0. +Proof. + intros. unfold find_assocmap, AssocMapExt.get_default. + now rewrite AssocMap.gempty. +Qed. + + Definition mk_ctrl f := {| + ctrl_st := Pos.succ (max_resource_function f); + ctrl_stack := Pos.succ (Pos.succ (Pos.succ (Pos.succ (max_resource_function f)))); + ctrl_fin := Pos.succ (Pos.succ (max_resource_function f)); + ctrl_return := Pos.succ (Pos.succ (Pos.succ (max_resource_function f))) + |}. + +Transparent Mem.load. +Transparent Mem.store. +Transparent Mem.alloc. + Lemma transl_callstate_correct: + forall (s : list GibleSubPar.stackframe) (f : GibleSubPar.function) (args : list Values.val) + (m : mem) (m' : Mem.mem') (stk : Values.block), + Mem.alloc m 0 (GibleSubPar.fn_stacksize f) = (m', stk) -> + forall R1 : DHTL.state, + match_states (GibleSubPar.Callstate s (AST.Internal f) args m) R1 -> + exists R2 : DHTL.state, + Smallstep.plus DHTL.step tge R1 Events.E0 R2 /\ + match_states + (GibleSubPar.State s f (Values.Vptr stk Integers.Ptrofs.zero) (GibleSubPar.fn_entrypoint f) + (Gible.init_regs args (GibleSubPar.fn_params f)) (PMap.init false) m') R2. + Proof. + intros * H R1 MSTATE. + + inversion MSTATE; subst. inversion TF; subst. + econstructor. split. apply Smallstep.plus_one. + eapply DHTL.step_call. + + unfold transl_module, Errors.bind, Errors.bind2, ret in *. + repeat (destruct_match; try discriminate; []). inv TF. cbn. + econstructor; eauto; inv MSTATE; inv H1; eauto. + + - constructor; intros. + + pose proof (ple_max_resource_function f r H0) as Hple. + unfold Ple in *. repeat rewrite assocmap_gso by lia. rewrite init_regs_empty. + rewrite dhtl_init_regs_empty. rewrite assocmap_gempty. rewrite Registers.Regmap.gi. + constructor. + + pose proof (ple_pred_max_resource_function f r H0) as Hple. + unfold Ple in *. repeat rewrite assocmap_gso by lia. + rewrite dhtl_init_regs_empty. rewrite assocmap_gempty. rewrite PMap.gi. + auto. + - cbn in *. unfold state_st_wf. repeat rewrite AssocMap.gso by lia. + now rewrite AssocMap.gss. + - constructor. + - unfold DHTL.empty_stack. cbn in *. econstructor. repeat split; intros. + + now rewrite AssocMap.gss. + + cbn. now rewrite list_repeat_len. + + cbn. now rewrite list_repeat_len. + + destruct (Mem.loadv Mint32 m' (Values.Val.offset_ptr (Values.Vptr stk Ptrofs.zero) (Ptrofs.repr (4 * ptr)))) eqn:Heqn; constructor. + unfold Mem.loadv in Heqn. destruct_match; try discriminate. cbn in Heqv0. + symmetry in Heqv0. inv Heqv0. + pose proof Mem.load_alloc_same as LOAD_ALLOC. + pose proof H as ALLOC. + eapply LOAD_ALLOC in ALLOC; eauto; subst. constructor. + - unfold reg_stack_based_pointers; intros. unfold stack_based. + unfold init_regs; + destruct (GibleSubPar.fn_params f); + rewrite Registers.Regmap.gi; constructor. + - unfold arr_stack_based_pointers; intros. unfold stack_based. + destruct (Mem.loadv Mint32 m' (Values.Val.offset_ptr (Values.Vptr stk Ptrofs.zero) (Ptrofs.repr (4 * ptr)))) eqn:LOAD; cbn; auto. + pose proof Mem.load_alloc_same as LOAD_ALLOC. + pose proof H as ALLOC. + eapply LOAD_ALLOC in ALLOC. now rewrite ALLOC. + exact LOAD. + - unfold stack_bounds; intros. split. + + unfold Mem.loadv. destruct_match; auto. + unfold Mem.load, Mem.alloc in *. inv H. cbn -[Ptrofs.max_unsigned] in *. + destruct_match; auto. unfold Mem.valid_access, Mem.range_perm, Mem.perm, Mem.perm_order' in *. + clear Heqs2. inv v0. cbn -[Ptrofs.max_unsigned] in *. inv Heqv0. exfalso. + specialize (H ptr). rewrite ! Ptrofs.add_zero_l in H. rewrite ! Ptrofs.unsigned_repr in H. + specialize (H ltac:(lia)). destruct_match; auto. rewrite PMap.gss in Heqo. + destruct_match; try discriminate. simplify. apply proj_sumbool_true in H5. lia. + apply stack_correct_inv in Heqb. lia. + + unfold Mem.storev. destruct_match; auto. + unfold Mem.store, Mem.alloc in *. inv H. cbn -[Ptrofs.max_unsigned] in *. + destruct_match; auto. unfold Mem.valid_access, Mem.range_perm, Mem.perm, Mem.perm_order' in *. + clear Heqs2. inv v0. cbn -[Ptrofs.max_unsigned] in *. inv Heqv0. exfalso. + specialize (H ptr). rewrite ! Ptrofs.add_zero_l in H. rewrite ! Ptrofs.unsigned_repr in H. + specialize (H ltac:(lia)). destruct_match; auto. rewrite PMap.gss in Heqo. + destruct_match; try discriminate. simplify. apply proj_sumbool_true in H5. lia. + apply stack_correct_inv in Heqb. lia. + - cbn; constructor; repeat rewrite PTree.gso by lia; now rewrite PTree.gss. + Qed. +Opaque Mem.load. +Opaque Mem.store. +Opaque Mem.alloc. + + Lemma transl_returnstate_correct: + forall (res0 : Registers.reg) (f : GibleSubPar.function) (sp : Values.val) (pc : Gible.node) + (rs : Gible.regset) (s : list GibleSubPar.stackframe) (vres : Values.val) (m : mem) ps + (R1 : DHTL.state), + match_states (GibleSubPar.Returnstate (GibleSubPar.Stackframe res0 f sp pc rs ps :: s) vres m) R1 -> + exists R2 : DHTL.state, + Smallstep.plus DHTL.step tge R1 Events.E0 R2 /\ + match_states (GibleSubPar.State s f sp pc (Registers.Regmap.set res0 vres rs) ps m) R2. + Proof. + intros * MSTATE. + inversion MSTATE. inversion MF. + Qed. + #[local] Hint Resolve transl_returnstate_correct : htlproof. + + Lemma step_cf_instr_pc_ind : + forall s f sp rs' pr' m' pc pc' cf t state, + step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf t state -> + step_cf_instr ge (GibleSubPar.State s f sp pc' rs' pr' m') cf t state. + Proof. destruct cf; intros; inv H; econstructor; eauto. Qed. + + Lemma step_list_inter_not_term : + forall A step_i sp i cf l i' cf', + @step_list_inter A step_i sp (Iterm i cf) l (Iterm i' cf') -> + i = i' /\ cf = cf'. + Proof. now inversion 1. Qed. + + Lemma step_instr_finish : + forall sp i l i' cf', + step_instr ge sp (Iexec i) l (Iterm i' cf') -> + i = i'. + Proof. now inversion 1. Qed. + + Lemma step_exec_concat2' : + forall sp i c a l cf, + SubParBB.step_instr_list ge sp (Iexec a) i (Iterm c cf) -> + SubParBB.step_instr_list ge sp (Iexec a) (i ++ l) (Iterm c cf). + Proof. + induction i. + - inversion 1. + - inversion 1; subst; clear H; cbn. + destruct i1. econstructor; eauto. eapply IHi; eauto. + exploit step_list_inter_not_term; eauto; intros. inv H. + eapply exec_term_RBcons; eauto. eapply exec_term_RBcons_term. + Qed. + + Lemma step_exec_concat' : + forall sp i c a b l, + SubParBB.step_instr_list ge sp (Iexec a) i (Iexec c) -> + SubParBB.step_instr_list ge sp (Iexec c) l b -> + SubParBB.step_instr_list ge sp (Iexec a) (i ++ l) b. + Proof. + induction i. + - inversion 1. eauto. + - inversion 1; subst. clear H. cbn. intros. econstructor; eauto. + destruct i1; [|inversion H6]. + eapply IHi; eauto. + Qed. + + Lemma step_exec_concat: + forall sp bb a b, + SubParBB.step ge sp a bb b -> + SubParBB.step_instr_list ge sp a (concat bb) b. + Proof. + induction bb. + - inversion 1. + - inversion 1; subst; clear H. + + cbn. eapply step_exec_concat'; eauto. + + cbn in *. eapply step_exec_concat2'; eauto. + Qed. + + Lemma one_ne_zero: + Int.repr 1 <> Int.repr 0. + Proof. + unfold not; intros. + assert (Int.unsigned (Int.repr 1) = Int.unsigned (Int.repr 0)) by (now rewrite H). + rewrite ! Int.unsigned_repr in H0 by crush. lia. + Qed. + + Lemma int_and_boolToValue : + forall b1 b2, + Int.and (boolToValue b1) (boolToValue b2) = boolToValue (b1 && b2). + Proof. + destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue; + replace (Z.of_nat 1) with 1 by auto; + replace (Z.of_nat 0) with 0 by auto. + - apply Int.and_idem. + - apply Int.and_zero. + - apply Int.and_zero_l. + - apply Int.and_zero. + Qed. + + Lemma int_or_boolToValue : + forall b1 b2, + Int.or (boolToValue b1) (boolToValue b2) = boolToValue (b1 || b2). + Proof. + destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue; + replace (Z.of_nat 1) with 1 by auto; + replace (Z.of_nat 0) with 0 by auto. + - apply Int.or_idem. + - apply Int.or_zero. + - apply Int.or_zero_l. + - apply Int.or_zero_l. + Qed. + + Lemma pred_expr_correct : + forall curr_p pr asr asa, + (forall r, Ple r (max_predicate curr_p) -> + find_assocmap 1 (pred_enc r) asr = boolToValue (PMap.get r pr)) -> + expr_runp tt asr asa (pred_expr curr_p) (boolToValue (eval_predf pr curr_p)). + Proof. + induction curr_p. + - intros * HFRL. cbn. destruct p as [b p']. destruct b. + + constructor. eapply HFRL. cbn. unfold Ple. lia. + + econstructor. constructor. eapply HFRL. cbn. unfold Ple; lia. + econstructor. cbn. f_equal. unfold boolToValue. + f_equal. destruct pr !! p' eqn:?. cbn. + rewrite Int.eq_false; auto. unfold natToValue. + replace (Z.of_nat 1) with 1 by auto. unfold Int.zero. + apply one_ne_zero. + cbn. rewrite Int.eq_true; auto. + - intros. cbn. constructor. + - intros. cbn. constructor. + - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H. + unfold Ple in *. lia. + eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia. + cbn -[eval_predf]. f_equal. symmetry. apply int_and_boolToValue. + - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H. + unfold Ple in *. lia. + eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia. + cbn -[eval_predf]. f_equal. symmetry. apply int_or_boolToValue. + Qed. + + Local Opaque deep_simplify. + + Lemma valueToBool_correct: + forall b, + valueToBool (boolToValue b) = b. + Proof. + unfold valueToBool, boolToValue; intros. + unfold uvalueToZ, natToValue. destruct b; cbn; + rewrite Int.unsigned_repr; crush. + Qed. + + Lemma negb_inj': + forall a b, a = b -> negb a = negb b. + Proof. intros. destruct a, b; auto. Qed. + + Lemma transl_predicate_correct : + forall asr asa a b asr' asa' p r e max_pred max_reg rs ps, + stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvar r) e) (e_assoc asr') (e_assoc_arr a b asa') -> + Ple (max_predicate p) max_pred -> + match_assocmaps max_reg max_pred rs ps asr -> + eval_predf ps p = false -> + (forall x, asr # x = asr' # x) /\ asa = asa'. + Proof. + intros * HSTMNT HPLE HMATCH HEVAL *. + pose proof HEVAL as HEVAL_DEEP. + erewrite <- eval_predf_deep_simplify in HEVAL_DEEP. + cbn in *. destruct_match. + - inv HSTMNT; inv H6. split; auto. intros. + exploit pred_expr_correct. inv HMATCH; eauto. intros. eapply H0. instantiate (1 := deep_simplify peq p) in H1. + eapply max_predicate_deep_simplify in H1. unfold Ple in *. lia. + intros. inv H7. unfold e_assoc in *; cbn in *. + pose proof H as H'. eapply expr_runp_determinate in H6; eauto. rewrite HEVAL_DEEP in H6. + rewrite H6 in H10. now rewrite valueToBool_correct in H10. + unfold e_assoc_arr, e_assoc in *; cbn in *. inv H9. + destruct (peq r0 x); subst; [now rewrite assocmap_gss|now rewrite assocmap_gso by auto]. + - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate). + unfold eval_predf in HEVAL_DEEP. + apply negb_inj' in HEVAL_DEEP. + rewrite <- negate_correct in HEVAL_DEEP. rewrite e0 in HEVAL_DEEP. discriminate. + Qed. + + Inductive lessdef_memory: option value -> option value -> Prop := + | lessdef_memory_none: + lessdef_memory None (Some (ZToValue 0)) + | lessdef_memory_eq: forall a, + lessdef_memory a a. + + Lemma transl_predicate_correct_arr : + forall asr asa a b asr' asa' p r e max_pred max_reg rs ps e1, + stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvari r e1) e) (e_assoc asr') (e_assoc_arr a b asa') -> + Ple (max_predicate p) max_pred -> + match_assocmaps max_reg max_pred rs ps asr -> + eval_predf ps p = false -> + asr = asr' /\ (forall x a, asa ! x = Some a -> exists a', asa' ! x = Some a' + /\ (forall y, (y < arr_length a)%nat -> exists av av', array_get_error y a = Some av /\ array_get_error y a' = Some av' /\ lessdef_memory av av')). + Proof. + intros * HSTMNT HPLE HMATCH HEVAL *. + pose proof HEVAL as HEVAL_DEEP. + erewrite <- eval_predf_deep_simplify in HEVAL_DEEP. + cbn in *. destruct_match. + - inv HSTMNT; inv H6; split; auto; intros. + exploit pred_expr_correct. inv HMATCH; eauto. intros. eapply H1. instantiate (1 := deep_simplify peq p) in H2. + eapply max_predicate_deep_simplify in H2. unfold Ple in *. lia. + intros. inv H7. unfold e_assoc in *; cbn in *. + pose proof H0 as H'. eapply expr_runp_determinate in H9; eauto. rewrite HEVAL_DEEP in H9. + rewrite H9 in H12. now rewrite valueToBool_correct in H12. + unfold e_assoc_arr, e_assoc in *; cbn in *. inv H11. + destruct (peq r0 x); subst. + + unfold arr_assocmap_set. rewrite H. + rewrite AssocMap.gss. eexists. split; eauto. unfold arr_assocmap_lookup in H10. + rewrite H in H10. inv H10. eapply expr_runp_determinate in H3; eauto. subst. + intros. + destruct (Nat.eq_dec y (valueToNat i)); subst. + * rewrite array_get_error_set_bound by auto. + destruct (array_get_error (valueToNat i) a1) eqn:?. + -- do 2 eexists. split; eauto. split. eauto. + destruct o; cbn; constructor. + -- exploit (@array_get_error_bound (option value)); eauto. simplify. + rewrite H3 in Heqo0. discriminate. + * rewrite array_gso by auto. + exploit (@array_get_error_bound (option value)); eauto. simplify. + rewrite H3. do 2 eexists; repeat split; constructor. + + unfold arr_assocmap_set. destruct_match. + * rewrite PTree.gso by auto. setoid_rewrite H. eexists. split; eauto. + intros. exploit (@array_get_error_bound (option value)); eauto. simplify. + rewrite H4. do 2 eexists; repeat split; constructor. + * eexists. split; eauto. intros. exploit (@array_get_error_bound (option value)); eauto. simplify. + rewrite H4. do 2 eexists; repeat split; constructor. + - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate). + unfold eval_predf in HEVAL_DEEP. + apply negb_inj' in HEVAL_DEEP. + rewrite <- negate_correct in HEVAL_DEEP. rewrite e0 in HEVAL_DEEP. discriminate. + Qed. + + Lemma transl_predicate_correct2 : + forall asr asa a b p r e max_pred max_reg rs ps, + Ple (max_predicate p) max_pred -> + match_assocmaps max_reg max_pred rs ps asr -> + eval_predf ps p = false -> + exists asr', stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvar r) e) (e_assoc asr') (e_assoc_arr a b asa) /\ (forall x n, asr # (x, n) = asr' # (x, n)) /\ (forall x y, asr ! x = Some y -> asr' ! x = Some y). + Proof. + intros * HPLE HMATCH HEVAL. pose proof HEVAL as HEVAL_DEEP. + unfold translate_predicate. erewrite <- eval_predf_deep_simplify in HEVAL_DEEP. + destruct_match. + - econstructor; split; [|split]. + + econstructor; [econstructor|]. eapply erun_Vternary_false. + * eapply pred_expr_correct. intros. eapply max_predicate_deep_simplify in H. + inv HMATCH. eapply H1; unfold Ple in *. lia. + * now econstructor. + * rewrite HEVAL_DEEP. auto. + + intros. destruct (peq x r); subst. + * now rewrite assocmap_gss. + * now rewrite assocmap_gso. + + intros. unfold e_assoc in *; simpl in *. destruct (peq x r); subst. + * unfold find_assocmap, AssocMapExt.get_default. rewrite H. now rewrite AssocMap.gss. + * unfold find_assocmap, AssocMapExt.get_default. + destruct (asr ! r) eqn:HE; now rewrite AssocMap.gso by auto. + - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate). + apply negb_inj' in HEVAL_DEEP. unfold eval_predf in *. rewrite <- negate_correct in HEVAL_DEEP. + now rewrite e0 in HEVAL_DEEP. + Qed. + + Lemma transl_predicate_correct2_true : + forall asr asa a b p r e max_pred max_reg rs ps v, + Ple (max_predicate p) max_pred -> + match_assocmaps max_reg max_pred rs ps asr -> + eval_predf ps p = true -> + expr_runp tt asr asa e v -> + stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvar r) e) (e_assoc (asr # r <- v)) (e_assoc_arr a b asa). + Proof. + intros * HPLE HMATCH HEVAL HEXPR. pose proof HEVAL as HEVAL_DEEP. + unfold translate_predicate. erewrite <- eval_predf_deep_simplify in HEVAL_DEEP. + destruct_match. + - econstructor. econstructor. econstructor. eapply pred_expr_correct. + intros. eapply max_predicate_deep_simplify in H. inv HMATCH. eapply H1. unfold Ple in *. lia. + eauto. rewrite HEVAL_DEEP. eauto. + - econstructor. econstructor. auto. + Qed. + + Lemma arr_assocmap_set_gss : + forall r i v asa ar, + asa ! r = Some ar -> + (arr_assocmap_set r i v asa) ! r = Some (array_set i (Some v) ar). + Proof. + unfold arr_assocmap_set. + intros. rewrite H. rewrite PTree.gss. auto. + Qed. + + Lemma arr_assocmap_set_gso : + forall r x i v asa ar, + asa ! x = Some ar -> + r <> x -> + (arr_assocmap_set r i v asa) ! x = asa ! x. + Proof. + unfold arr_assocmap_set. intros. + destruct (asa!r) eqn:?; auto; now rewrite PTree.gso by auto. + Qed. + + Lemma arr_assocmap_set_gs2 : + forall r x i v asa, + asa ! x = None -> + (arr_assocmap_set r i v asa) ! x = None. + Proof. + unfold arr_assocmap_set. intros. + destruct (peq r x); subst; [now rewrite H|]. + destruct (asa!r) eqn:?; auto. + now rewrite PTree.gso by auto. + Qed. + + Lemma get_mem_set_array_gss : + forall y a x, + (y < arr_length a)%nat -> + get_mem y (array_set y (Some x) a) = x. + Proof. + unfold get_mem; intros. + rewrite array_get_error_set_bound by eauto; auto. + Qed. + + Lemma get_mem_set_array_gss2 : + forall y a, + (y < arr_length a)%nat -> + get_mem y (array_set y None a) = ZToValue 0. + Proof. + unfold get_mem; intros. + rewrite array_get_error_set_bound by eauto; auto. + Qed. + + Lemma get_mem_set_array_gso : + forall y a x z, + y <> z -> + get_mem y (array_set z x a) = get_mem y a. + Proof. unfold get_mem; intros. now rewrite array_gso by auto. Qed. + + Lemma get_mem_set_array_gso2 : + forall y a x z, + (y >= arr_length a)%nat -> + get_mem y (array_set z x a) = ZToValue 0. + Proof. + intros; unfold get_mem. unfold array_get_error. + erewrite array_set_len with (i:=z) (x:=x) in H. + remember (array_set z x a). destruct a0. cbn in *. rewrite <- arr_wf in H. + assert (Datatypes.length arr_contents <= y)%nat by lia. + apply nth_error_None in H0. rewrite H0. auto. + Qed. + + Lemma get_mem_set_array_gss3 : + forall y a, + get_mem y (array_set y None a) = ZToValue 0. + Proof. + intros. + assert (y < arr_length a \/ y >= arr_length a)%nat by lia. + inv H. + - now rewrite get_mem_set_array_gss2. + - now rewrite get_mem_set_array_gso2. + Qed. + + Lemma arr_assocmap_lookup_get_mem: + forall asa r i v, + arr_assocmap_lookup asa r i = Some v -> + exists ar, asa ! r = Some ar /\ get_mem i ar = v. + Proof. + unfold arr_assocmap_lookup in *; intros. + repeat (destruct_match; try discriminate). inv H. + eexists; eauto. + Qed. + + Lemma transl_predicate_correct_arr2 : + forall asr asa a b p r e max_pred max_reg rs ps e1 v1 ar, + Ple (max_predicate p) max_pred -> + match_assocmaps max_reg max_pred rs ps asr -> + eval_predf ps p = false -> + expr_runp tt (assoc_blocking (e_assoc asr)) (assoc_blocking (e_assoc_arr a b asa)) e1 v1 -> + arr_assocmap_lookup (assoc_blocking (e_assoc_arr a b asa)) r (valueToNat v1) = Some ar -> + exists asa', stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvari r e1) e) (e_assoc asr) (e_assoc_arr a b asa') + /\ (forall x a, asa ! x = Some a -> + exists a', asa' ! x = Some a' + /\ (forall y, (y < arr_length a)%nat -> get_mem y a = get_mem y a') + /\ (arr_length a = arr_length a')). + Proof. + intros * HPLE HMATCH HEVAL HEXPRRUN HLOOKUP. pose proof HEVAL as HEVAL_DEEP. + unfold translate_predicate. erewrite <- eval_predf_deep_simplify in HEVAL_DEEP. + destruct_match. + - econstructor; split. + + econstructor; [econstructor|]; eauto. eapply erun_Vternary_false. + * eapply pred_expr_correct. intros. eapply max_predicate_deep_simplify in H. + inv HMATCH. eapply H1; unfold Ple in *. lia. + * econstructor; eauto. + * rewrite HEVAL_DEEP. auto. + + intros. destruct (peq x r); subst. + * erewrite arr_assocmap_set_gss by eauto. + eexists; repeat split; eauto; intros. + destruct (Nat.eq_dec y (valueToNat v1)); subst. + -- rewrite get_mem_set_array_gss by auto. + exploit arr_assocmap_lookup_get_mem; eauto. intros (ar' & HASSOC & HGET). + unfold e_assoc_arr in HASSOC. cbn in *. rewrite HASSOC in H. inv H. auto. + -- now rewrite get_mem_set_array_gso by auto. + * erewrite arr_assocmap_set_gso by eauto. unfold e_assoc_arr; cbn. eexists; split; eauto. + - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate). + apply negb_inj' in HEVAL_DEEP. unfold eval_predf in *. rewrite <- negate_correct in HEVAL_DEEP. + now rewrite e0 in HEVAL_DEEP. + Qed. + + Lemma transl_predicate_cond_correct_arr2 : + forall asr asa a b p max_pred max_reg rs ps s, + Ple (max_predicate p) max_pred -> + match_assocmaps max_reg max_pred rs ps asr -> + eval_predf ps p = false -> + stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate_cond (Some p) s) (e_assoc asr) (e_assoc_arr a b asa). + Proof. + intros * HPLE HMATCH HEVAL. + unfold translate_predicate_cond. inv HMATCH. + exploit pred_expr_correct. intros; eapply H0. unfold Ple in *. instantiate (1:=p) in H1. lia. + intros. rewrite HEVAL in H1. unfold boolToValue, natToValue in H1. cbn in H1. + eapply stmnt_runp_Vcond_false; eauto. constructor. + Qed. + + Definition unchanged (asr : assocmap) asa asr' asa' := + (forall x n, asr # (x, n) = asr' # (x, n)) + /\ (forall x y, asr ! x = Some y -> asr' ! x = Some y) + /\ (forall x a, asa ! x = Some a -> + exists a', asa' ! x = Some a' + /\ (forall y, (y < arr_length a)%nat -> get_mem y a = get_mem y a') + /\ arr_length a = arr_length a'). + + Lemma unchanged_refl : + forall a b, unchanged a b a b. + Proof. + unfold unchanged; split; intros. eauto. + eexists; eauto. + Qed. + + Lemma unchanged_trans : + forall a b a' b' a'' b'', unchanged a b a' b' -> unchanged a' b' a'' b'' -> unchanged a b a'' b''. + Proof. + unfold unchanged; simplify; intros. + congruence. + eauto. + pose proof H4 as H'. apply H5 in H'. simplify. pose proof H7 as H5'. + apply H3 in H5'. simplify. eexists; eauto; simplify; eauto; try congruence. + intros. rewrite H6 by auto. now rewrite <- H8 by lia. + Qed. + + Opaque translate_predicate. + Opaque translate_predicate_cond. + + Lemma calc_predicate_lt_max_function : + forall m next_p p, + Ple (max_predicate next_p) m -> + Forall (fun x : positive => Ple x m) + match p with + | Some p => predicate_use p + | None => nil + end -> + Ple (max_predicate (Pand next_p (dfltp p))) m. + Proof. + intros. destruct p. + - eapply le_max_pred in H0. + cbn. unfold Ple in *; lia. + - cbn. unfold Ple in *; lia. + Qed. + +Lemma truthy_dflt : + forall ps p, + truthy ps p -> eval_predf ps (dfltp p) = true. +Proof. intros. destruct p; cbn; inv H; auto. Qed. + + Lemma state_st_wf_write : + forall asr v st pc dst, + state_st_wf asr st pc -> + reg_enc dst <> st -> + state_st_wf (AssocMap.set (reg_enc dst) v asr) st pc. + Proof. + unfold state_st_wf; intros. + rewrite PTree.gso by auto; auto. + Qed. + + Lemma mk_ctrl_correct : + forall f m, + OK m = transl_module f -> + (mk_ctrl f).(ctrl_st) = m.(DHTL.mod_st) + /\ (mk_ctrl f).(ctrl_stack) = m.(DHTL.mod_stk) + /\ (mk_ctrl f).(ctrl_fin) = m.(DHTL.mod_finish) + /\ (mk_ctrl f).(ctrl_return) = m.(DHTL.mod_return). + Proof. + intros. unfold transl_module, Errors.bind in *. repeat destr. inv H. auto. + Qed. + + Lemma transl_iop_correct: + forall f s s' pc sp m_ d d' curr_p next_p rs ps m rs' p op args dst asr arr asr' arr' stk stk_len n, + transf_instr n (mk_ctrl f) (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') -> + step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) -> + stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d (e_assoc asr') (e_assoc_arr stk stk_len arr') -> + eval_predf ps curr_p = true -> + truthy ps p -> + Ple (max_predicate curr_p) (max_pred_function f) -> + Forall (fun x => Ple x (max_pred_function f)) (pred_uses (RBop p op args dst)) -> + match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr' arr') -> + Forall (fun x : positive => Ple x (max_reg_function f)) args -> + Ple dst (max_reg_function f) -> + exists asr'', stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d' (e_assoc asr'') (e_assoc_arr stk stk_len arr') + /\ match_states (GibleSubPar.State s f sp pc rs' ps m) (DHTL.State s' m_ pc asr'' arr'). + Proof. + cbn in *; unfold Errors.bind; cbn in *; intros * ? HTRANSF HSTEP HSTMNT HEVAL_PRED HTRUTHY HPLE HFRL1 HMATCH HFRL HREG. + move HTRANSF after HFRL1. repeat destr. inv HTRANSF. inv HSTEP. + 2: { inv H3. cbn in *. inv HTRUTHY. rewrite H1 in H0. discriminate. } + exploit eval_correct. 3: { eauto. } 3: { eauto. } eauto. eauto. intros (v' & HEXPR & HVAL). + eexists. split. + - inv HMATCH. econstructor; eauto. eapply transl_predicate_correct2_true; eauto. + eapply calc_predicate_lt_max_function; eauto. + rewrite eval_predf_Pand; rewrite HEVAL_PRED; rewrite truthy_dflt; auto. + - inv HMATCH. econstructor; eauto. eapply regs_lessdef_add_match; auto. + eapply state_st_wf_write; eauto. + { symmetry in TF; eapply mk_ctrl_correct in TF. inv TF. rewrite <- H. cbn. + eapply ple_max_resource_function in HREG. unfold Ple in *. lia. } + { exploit op_stack_based; eauto. intros. + unfold reg_stack_based_pointers. intros. + destruct (peq dst r); subst. now rewrite PMap.gss. + rewrite PMap.gso by auto. eauto. } + unfold transl_module, Errors.bind, ret in TF; repeat destr. inv TF; cbn in *. + eapply ple_max_resource_function in HREG. unfold Ple in *. + econstructor. + { inv CONST. rewrite AssocMap.gso by lia. eauto. } + { inv CONST. rewrite AssocMap.gso by lia. eauto. } + Qed. + + Lemma fold_left_max : + forall l r n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n). + Proof. + induction l; simpl; intros. + tauto. + apply IHl. destruct H as [[A|A]|A]. right; subst; extlia. auto. right; extlia. + Qed. + + Lemma unchanged_implies_match : + forall s f sp rs ps m s' m_ pc asr' asa' asa asr, + unchanged asr asa asr' asa' -> + match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr asa) -> + match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr' asa'). + Proof. + intros * HUNCH HMATCH; unfold unchanged in *; simplify. + rename H into HFINDEQ, H1 into HDEF, H2 into HARR. + inv HMATCH. + econstructor; auto. + - econstructor; intros; inv MASSOC; rewrite <- HFINDEQ; eauto. + - unfold state_st_wf in *. eauto. + - inv MARR. simplify. + rename H0 into HSTACK, H into HARRLEN, H1 into HARRLEN', H3 into HEQ. + exploit HARR; eauto. intros (a' & HASA & HEQ' & HARRLEN''). + econstructor. simplify; eauto; try congruence. + intros. rewrite <- HARRLEN'' in H. pose proof H as H'. apply HEQ in H. + inv H; econstructor. + rewrite <- HEQ'; eauto. lia. + - inv CONST. constructor; eauto. + Qed. + +Lemma eval_predf_negate : + forall ps p, + eval_predf ps (negate p) = negb (eval_predf ps p). +Proof. + unfold eval_predf; intros. rewrite negate_correct. auto. +Qed. + + Lemma unchanged_match_assocmaps : + forall a b a' b' m1 m2 rs ps, + unchanged a b a' b' -> + match_assocmaps m1 m2 rs ps a -> + match_assocmaps m1 m2 rs ps a'. + Proof. + unfold unchanged; inversion 2; subst. clear H0. + inv H. inv H3. econstructor; intros. rewrite <- H0. eauto. + rewrite <- H0. eauto. + Qed. + +End CORRECTNESS. |