diff options
Diffstat (limited to 'src/translation')
| -rw-r--r-- | src/translation/HTLgen.v | 264 | ||||
| -rw-r--r-- | src/translation/HTLgenproof.v | 3830 | ||||
| -rw-r--r-- | src/translation/HTLgenspec.v | 284 | ||||
| -rw-r--r-- | src/translation/Veriloggen.v | 36 | ||||
| -rw-r--r-- | src/translation/Veriloggenproof.v | 303 | ||||
| -rw-r--r-- | src/translation/Veriloggenspec.v | 17 |
6 files changed, 2702 insertions, 2032 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 9a82aa8..db24a1d 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -19,7 +19,7 @@ From compcert Require Import Maps. From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. -From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. +From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. @@ -88,10 +88,10 @@ Import HTLMonadExtra. Export MonadNotation. Definition state_goto (st : reg) (n : node) : stmnt := - Vnonblock (Vvar st) (Vlit (posToValue 32 n)). + Vnonblock (Vvar st) (Vlit (posToValue n)). Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := - Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). + Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. @@ -244,7 +244,7 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := Vbinop op (Vvar r) (Vlit (intToValue l)). Definition boplitz (op: binop) (r: reg) (l: Z) : expr := - Vbinop op (Vvar r) (Vlit (ZToValue 32%nat l)). + Vbinop op (Vvar r) (Vlit (ZToValue l)). Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := match c, args with @@ -269,14 +269,37 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") end. +Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr := + match c, args with + | 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 Vltu r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2) + | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int) + : mon expr := + match c, args with + | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) + | Integers.Cne, r1::nil => ret (boplit Vne r1 i) + | Integers.Clt, r1::nil => ret (boplit Vltu r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i) + | Integers.Cle, r1::nil => ret (boplit Vleu r1 i) + | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i) + | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + end. + Definition translate_condition (c : Op.condition) (args : list reg) : mon expr := match c, args with | Op.Ccomp c, _ => translate_comparison c args - | Op.Ccompu c, _ => translate_comparison c args + | Op.Ccompu c, _ => translate_comparisonu c args | Op.Ccompimm c i, _ => translate_comparison_imm c args i - | Op.Ccompuimm c i, _ => translate_comparison_imm c args i - | Op.Cmaskzero n, r::nil => ret (Vbinop Veq (boplit Vand r n) (Vlit (ZToValue 32 0))) - | Op.Cmasknotzero n, r::nil => ret (Vbinop Vne (boplit Vand r n) (Vlit (ZToValue 32 0))) + | Op.Ccompuimm c i, _ => translate_comparison_immu c args i + | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. @@ -292,26 +315,16 @@ Definition check_address_parameter_unsigned (p : Z) : bool := Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Op.Aindexed off, r1::nil => - if (check_address_parameter_signed off) - then ret (boplitz Vadd r1 off) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") + ret (boplitz Vadd r1 off) | Op.Ascaled scale offset, r1::nil => - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") + ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) | Op.Aindexed2 offset, r1::r2::nil => - if (check_address_parameter_signed offset) - then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") + ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") + ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in - if (check_address_parameter_unsigned a) - then ret (Vlit (ZToValue 32 a)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") + ret (Vlit (ZToValue a)) | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. @@ -341,20 +354,19 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) - | Op.Oshrximm n, r::nil => ret (Vbinop Vdiv (Vvar r) - (Vbinop Vshl (Vlit (ZToValue 32 1)) - (Vlit (intToValue n)))) + | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm") + (*ret (Vbinop Vdiv (Vvar r) + (Vbinop Vshl (Vlit (ZToValue 1)) + (Vlit (intToValue n))))*) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => ret (Vbinop Vor (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n))) + | Op.Ororimm n, r::nil => ret (boplit Vror r n) | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => do tc <- translate_condition c rl; ret (Vternary tc (Vvar r1) (Vvar r2)) | Op.Olea a, _ => translate_eff_addressing a args - | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *) - | Op.Ocast32signed, r::nil => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *) | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. @@ -392,26 +404,38 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") end. -Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) - (args : list reg) (stack : reg) : mon expr := - match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Mint32, Op.Aindexed off, r1::nil => - if (check_address_parameter_signed off) - then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address misaligned") - | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vvari stack - (Vbinop Vdivu - (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (ZToValue 32 4))) - else error (Errors.msg "HTLgen: translate_arr_access address misaligned") - | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) +(* Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) *) +(* (args : list reg) (stack : reg) : mon expr := *) +(* match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) *) +(* | Mint32, Op.Aindexed off, r1::nil => *) +(* if (check_address_parameter_signed off) *) +(* then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) *) +(* else error (Errors.msg "HTLgen: translate_arr_access address misaligned") *) +(* | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) *) +(* if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) *) +(* then ret (Vvari stack *) +(* (Vbinop Vdivu *) +(* (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) *) +(* (Vlit (ZToValue 4)))) *) +(* else error (Errors.msg "HTLgen: translate_arr_access address misaligned") *) +(* | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) *) +(* let a := Integers.Ptrofs.unsigned a in *) +(* if (check_address_parameter_unsigned a) *) +(* then ret (Vvari stack (Vlit (ZToValue (a / 4)))) *) +(* else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") *) +(* | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") *) +(* end. *) + +Definition translate_arr_addressing (a: Op.addressing) (args: list reg) : mon expr := + match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Op.Aindexed off, r1::nil => + ret (boplitz Vadd r1 off) + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in - if (check_address_parameter_unsigned a) - then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") - | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") + ret (Vlit (ZToValue a)) + | _, _ => error (Errors.msg "Veriloggen: translate_arr_addressing unsuported addressing") end. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := @@ -422,41 +446,70 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := List.map (fun a => match a with - (i, n) => (Vlit (natToValue 32 i), Vnonblock (Vvar st) (Vlit (posToValue 32 n))) + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) end) (enumerate 0 ns). +Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt := + Vnonblock (Vvar dst) (Vload stack addr). + +Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt := + let l0 := Vnonblock (Vvari stack addr) (Vvarb0 src) in + let l1 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in + let l2 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in + let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 3)) (Vvarb3 src) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. + Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => match i with - | Inop n' => add_instr n n' Vskip + | Inop n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + add_instr n n' Vskip + else error (Errors.msg "State is larger than 2^32.") | Iop op args dst n' => - do instr <- translate_instr op args; - do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst instr) - | Iload mem addr args dst n' => - do src <- translate_arr_access mem addr args stack; - do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) - | Istore mem addr args src n' => - do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst instr) + else error (Errors.msg "State is larger than 2^32.") + | Iload chunk addr args dst n' => + match chunk with + | Mint32 => + if Z.leb (Z.pos n') Integers.Int.max_unsigned + then do addr' <- translate_arr_addressing addr args; + do _ <- declare_reg None dst 32; + add_instr n n' $ create_single_cycle_load stack addr' dst + else error (Errors.msg "State is larger than 2^32.") + | _ => error (Errors.msg "Iload invalid chunk size.") + end + | Istore chunk addr args src n' => + match chunk with + | Mint32 => + if Z.leb (Z.pos n') Integers.Int.max_unsigned + then do addr' <- translate_arr_addressing addr args; + add_instr n n' $ create_single_cycle_store stack addr' src + else error (Errors.msg "State is larger than 2^32.") + | _ => error (Errors.msg "Istore invalid chunk size.") + end | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") | Icond cond args n1 n2 => - do e <- translate_condition cond args; - add_branch_instr e n n1 n2 + if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then + do e <- translate_condition cond args; + add_branch_instr e n n1 n2 + else error (Errors.msg "State is larger than 2^32.") | Ijumptable r tbl => do s <- get; add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip)) | Ireturn r => match r with | Some r' => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) | None => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) end end end. @@ -512,32 +565,67 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). +Definition max_pc_map (m : Maps.PTree.t stmnt) := + PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. + +Lemma max_pc_map_sound: + forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). +Proof. + intros until i. unfold max_pc_function. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. xomega. + apply Ple_trans with a. auto. xomega. +Qed. + +Lemma max_pc_wf : + forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + map_well_formed m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + Definition transf_module (f: function) : mon 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 _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); - do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); - do start <- create_reg (Some Vinput) 1; - do rst <- create_reg (Some Vinput) 1; - do clk <- create_reg (Some Vinput) 1; - do current_state <- get; - ret (mkmodule - f.(RTL.fn_params) - current_state.(st_datapath) - current_state.(st_controllogic) - f.(fn_entrypoint) - current_state.(st_st) - stack - stack_len - fin - rtrn - start - rst - clk - current_state.(st_scldecls) - current_state.(st_arrdecls)) + do fin <- create_reg (Some Voutput) 1; + do rtrn <- create_reg (Some Voutput) 32; + do (stack, stack_len) <- create_arr None 8 (Z.to_nat f.(fn_stacksize)); + do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); + do start <- create_reg (Some Vinput) 1; + do rst <- create_reg (Some Vinput) 1; + do clk <- create_reg (Some Vinput) 1; + do current_state <- get; + match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end else error (Errors.msg "Stack size misalignment."). Definition max_state (f: function) : state := diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 6e470d5..813a94b 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -16,9 +16,9 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require RTL Registers AST Integers. -From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. +From compcert Require RTL Registers AST. +From compcert Require Import Integers Globalenvs Memory Linking. +From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -41,7 +41,7 @@ Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := forall st asa asr res, s = HTL.State res m st asa asr -> - asa!(m.(HTL.mod_st)) = Some (posToValue 32 st). + asa!(m.(HTL.mod_st)) = Some (posToValue st). Hint Unfold state_st_wf : htlproof. Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : @@ -53,7 +53,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> opt_val_value_lessdef (Mem.loadv AST.Mint32 mem (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) - (Option.default (NToValue 32 0) + (Option.default (NToValue 0) (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> match_arrs m f sp mem asa. @@ -86,18 +86,13 @@ Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_frames_nil : match_frames nil nil. -(* | match_frames_cons : *) -(* forall cs lr r f sp sp' pc rs m asr asa *) -(* (TF : tr_module f m) *) -(* (ST: match_frames mem cs lr) *) -(* (MA: match_assocmaps f rs asr) *) -(* (MARR : match_arrs m f sp mem asa) *) -(* (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) *) -(* (RSBP: reg_stack_based_pointers sp' rs) *) -(* (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) *) -(* (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), *) -(* match_frames mem (RTL.Stackframe r f sp pc rs :: cs) *) -(* (HTL.Stackframe r m pc asr asa :: lr). *) + +Inductive match_constants : HTL.module -> assocmap -> Prop := + match_constant : + forall m asr, + asr!(HTL.mod_reset m) = Some (ZToValue 0) -> + asr!(HTL.mod_finish m) = Some (ZToValue 0) -> + match_constants m asr. Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem m st res @@ -109,7 +104,8 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) (RSBP : reg_stack_based_pointers sp' rs) (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) - (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), + (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) + (CONST : match_constants m asr), match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa) | match_returnstate : @@ -128,11 +124,30 @@ Definition match_prog (p: RTL.program) (tp: HTL.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ main_is_internal p = true. -Definition match_prog_matches : - forall p tp, - match_prog p tp -> - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. - Proof. intros. unfold match_prog in H. tauto. Qed. +Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): + TransfLink (fun (p1: RTL.program) (p2: HTL.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: RTL.program) (tp: HTL.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, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. @@ -266,32 +281,6 @@ Proof. assumption. Qed. -(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) -Lemma assumption_32bit : - forall v, - valueToPos (posToValue 32 v) = v. -Admitted. - -Lemma st_greater_than_res : - forall m res : positive, - m <> res. -Admitted. - -Lemma finish_not_return : - forall r f : positive, - r <> f. -Admitted. - -Lemma finish_not_res : - forall f r : positive, - f <> r. -Admitted. - -Lemma greater_than_max_func : - forall f st, - Plt (RTL.max_reg_function f) st. -Proof. Admitted. - Ltac inv_state := match goal with MSTATE : match_states _ _ |- _ => @@ -353,1818 +342,1943 @@ Section CORRECTNESS. 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 : RTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : HTL.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: RTL.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: RTL.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'). - Hint Resolve senv_preserved : htlproof. - - Lemma eval_correct : - forall sp op rs args m v v' e asr asa f s s' i, - 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 s = OK e s' i -> - val_value_lessdef v v' -> - Verilog.expr_runp f asr asa e v'. - Admitted. - - Lemma eval_cond_correct : - forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, - translate_condition cond args s1 = OK c s' i -> - Op.eval_condition - cond - (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) - m = Some b -> - Verilog.expr_runp f asr asa c (boolToValue 32 b). - Admitted. - - (** The proof of semantic preservation for the translation of instructions - is a simulation argument based on diagrams of the following form: -<< - match_states - code st rs ---------------- State m st assoc - || | - || | - || | - \/ v - code st rs' --------------- State m st assoc' - match_states ->> - where [tr_code c data control fin rtrn st] is assumed to hold. - - The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. - *) - - Definition transl_instr_prop (instr : RTL.instruction) : Prop := - forall m asr asa fin rtrn st stmt trans res, - tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> - exists asr' asa', - HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). - - Opaque combine. - - Ltac tac0 := - match goal with - | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit - - | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs - | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr - | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge - | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros - | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set - - | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack - - | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss - | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso - | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty - - | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => - rewrite combine_lookup_first - - | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 - | [ |- context[match_states _ _] ] => econstructor; auto - | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto - | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] => - apply regs_lessdef_add_greater; [> apply greater_than_max_func | assumption] - - | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => - unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal - | [ |- context[(AssocMap.combine _ _ _) ! _] ] => - try (rewrite AssocMap.gcombine; [> | reflexivity]) - - | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => - rewrite Registers.Regmap.gss - | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => - destruct (Pos.eq_dec s d) as [EQ|EQ]; - [> rewrite EQ | rewrite Registers.Regmap.gso; auto] - - | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H - | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] - | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H - end. - - Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. - Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. - - Lemma transl_inop_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : RTL.regset) (m : mem) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m pc' H R1 MSTATE. - inv_state. - - unfold match_prog in TRANSL. - econstructor. - split. - apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - (* processing of state *) - econstructor. - crush. - econstructor. - econstructor. - econstructor. - - all: invert MARR; big_tac. - Unshelve. - constructor. - Qed. - Hint Resolve transl_inop_correct : htlproof. - - Lemma transl_iop_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) - (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), - (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> - Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. - Proof. - intros s f sp pc rs m op args res0 pc' v H H0. - - (* Iop *) - (* destruct v eqn:?; *) - (* try ( *) - (* destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); *) - (* inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); *) - (* try (unfold_func H6); *) - (* try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; *) - (* unfold_func H3); *) - - (* inversion Heql; inversion MASSOC; subst; *) - (* assert (HPle : Ple r (RTL.max_reg_function f)) *) - (* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) - (* apply H1 in HPle; inversion HPle; *) - (* rewrite H2 in *; discriminate *) - (* ). *) - - (* + econstructor. split. *) - (* apply Smallstep.plus_one. *) - (* eapply HTL.step_module; eauto. *) - (* econstructor; simpl; trivial. *) - (* constructor; trivial. *) - (* econstructor; simpl; eauto. *) - (* eapply eval_correct; eauto. constructor. *) - (* unfold_merge. simpl. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - - (* (* match_states *) *) - (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *) - (* rewrite <- H1. *) - (* constructor; auto. *) - (* unfold_merge. *) - (* apply regs_lessdef_add_match. *) - (* constructor. *) - (* apply regs_lessdef_add_greater. *) - (* apply greater_than_max_func. *) - (* assumption. *) - - (* unfold state_st_wf. intros. inversion H2. subst. *) - (* unfold_merge. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - - (* + econstructor. split. *) - (* apply Smallstep.plus_one. *) - (* eapply HTL.step_module; eauto. *) - (* econstructor; simpl; trivial. *) - (* constructor; trivial. *) - (* econstructor; simpl; eauto. *) - (* eapply eval_correct; eauto. *) - (* constructor. rewrite valueToInt_intToValue. trivial. *) - (* unfold_merge. simpl. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - - (* (* match_states *) *) - (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *) - (* rewrite <- H1. *) - (* constructor. *) - (* unfold_merge. *) - (* apply regs_lessdef_add_match. *) - (* constructor. *) - (* symmetry. apply valueToInt_intToValue. *) - (* apply regs_lessdef_add_greater. *) - (* apply greater_than_max_func. *) - (* assumption. assumption. *) - - (* unfold state_st_wf. intros. inversion H2. subst. *) - (* unfold_merge. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - (* assumption. *) - Admitted. - Hint Resolve transl_iop_correct : htlproof. - - Ltac tac := - repeat match goal with - | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate - | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => - let EQ1 := fresh "EQ" in - let EQ2 := fresh "EQ" in - destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * - | [ _ : context[if ?x then _ else _] |- _ ] => - let EQ := fresh "EQ" in - destruct x eqn:EQ; simpl in * - | [ H : ret _ _ = _ |- _ ] => invert H - | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x - end. - - Ltac inv_arr_access := - match goal with - | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => - destruct c, chunk, addr, args; crush; tac; crush - end. - - Lemma transl_iload_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) - (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) - (pc' : RTL.node) (a v : Values.val), - (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> - Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> - Mem.loadv chunk m a = Some v -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. - Proof. - intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. - inv_state. inv_arr_access. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - - rewrite ARCHI in H1. crush. - subst. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H6 in HPler0. - invert HPler0; try congruence. - rewrite EQr0 in H8. - invert H8. - clear H0. clear H6. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - rewrite Integers.Ptrofs.signed_repr; try assumption. - admit. (* FIXME: Register bounds. *) - apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.signed_repr; crush. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - small_tac. } - - (** Normalisation proof *) - assert (Integers.Ptrofs.repr - (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) - as NORMALISE. - { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. - rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divu; crush; auto. } - - (** Normalised bounds proof *) - assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) - < (RTL.fn_stacksize f / 4)) - as NORMALISE_BOUND. - { split. - apply Integers.Ptrofs.unsigned_range_2. - assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. - unfold Integers.Ptrofs.divu at 2 in H0. - rewrite H0. clear H0. - rewrite Integers.Ptrofs.unsigned_repr; crush. - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; small_tac. - apply Z.div_le_upper_bound; small_tac. } - - inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; - clear NORMALISE_BOUND. - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - - all: big_tac. - - 1: { apply st_greater_than_res. } - 2: { apply st_greater_than_res. } - - (** Match assocmaps *) - apply regs_lessdef_add_match; big_tac. - - (** Equality proof *) - match goal with - | [ |- context [valueToNat ?x] ] => - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - rewrite <- EXPR_OK. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H7; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - pose proof (RSBP r1) as RSBPr1. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. - - rewrite ARCHI in H1. crush. - subst. - clear RSBPr1. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - pose proof (H0 r1). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - assert (HPler1 : Ple r1 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H6 in HPler0. - apply H8 in HPler1. - invert HPler0; invert HPler1; try congruence. - rewrite EQr0 in H10. - rewrite EQr1 in H12. - invert H10. invert H12. - clear H0. clear H6. clear H8. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) - (Integers.Int.repr z0)))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - rewrite Integers.Ptrofs.signed_repr; try assumption. - admit. (* FIXME: Register bounds. *) - apply PtrofsExtra.of_int_mod. - apply IntExtra.add_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - apply IntExtra.mul_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - admit. (* FIXME: Register bounds. *) - rewrite Integers.Int.signed_repr; crush. - rewrite Integers.Int.signed_repr; crush. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - small_tac. } - - (** Normalisation proof *) - assert (Integers.Ptrofs.repr - (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) - as NORMALISE. - { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. - rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divu; crush. } - - (** Normalised bounds proof *) - assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) - < (RTL.fn_stacksize f / 4)) - as NORMALISE_BOUND. - { split. - apply Integers.Ptrofs.unsigned_range_2. - assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. - unfold Integers.Ptrofs.divu at 2 in H0. - rewrite H0. clear H0. - rewrite Integers.Ptrofs.unsigned_repr; crush. - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; small_tac. - apply Z.div_le_upper_bound; lia. } - - inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; - clear NORMALISE_BOUND. - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. - - all: big_tac. - - 1: { apply st_greater_than_res. } - 2: { apply st_greater_than_res. } - - (** Match assocmaps *) - apply regs_lessdef_add_match; big_tac. - - (** Equality proof *) - match goal with - | [ |- context [valueToNat ?x] ] => - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - rewrite <- EXPR_OK. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H7; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - - + invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - rewrite ARCHI in H0. crush. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H1. clear ZERO. - rewrite Integers.Ptrofs.add_zero_l in H1. - - remember i0 as OFFSET. - - (** Modular preservation proof *) - rename H0 into MOD_PRESERVE. - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } - - (** Normalisation proof *) - assert (Integers.Ptrofs.repr - (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) - as NORMALISE. - { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. - rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divu; crush. } - - (** Normalised bounds proof *) - assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) - < (RTL.fn_stacksize f / 4)) - as NORMALISE_BOUND. - { split. - apply Integers.Ptrofs.unsigned_range_2. - assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. - unfold Integers.Ptrofs.divu at 2 in H0. - rewrite H0. clear H0. - rewrite Integers.Ptrofs.unsigned_repr; crush. - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; small_tac. - apply Z.div_le_upper_bound; lia. } - - inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; - clear NORMALISE_BOUND. - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. econstructor. econstructor. crush. - - all: big_tac. - - 1: { apply st_greater_than_res. } - 2: { apply st_greater_than_res. } - - (** Match assocmaps *) - apply regs_lessdef_add_match; big_tac. - - (** Equality proof *) - match goal with - | [ |- context [valueToNat ?x] ] => - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - rewrite <- EXPR_OK. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H7; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - Admitted. - Hint Resolve transl_iload_correct : htlproof. - - Lemma transl_istore_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) - (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg) - (pc' : RTL.node) (a : Values.val) (m' : mem), - (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> - Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> - Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. - Proof. - intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. - inv_state. inv_arr_access. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - - rewrite ARCHI in H1. crush. - subst. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H6 in HPler0. - invert HPler0; try congruence. - rewrite EQr0 in H8. - invert H8. - clear H0. clear H6. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - rewrite Integers.Ptrofs.signed_repr; try assumption. - admit. (* FIXME: Register bounds. *) - apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.signed_repr; crush. } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. - apply Integers.Ptrofs.unsigned_range_2. } - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. crush. - econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). - econstructor. - econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - - all: crush. - - (** State Lookup *) - unfold Verilog.merge_regs. - crush. - unfold_merge. - apply AssocMap.gss. - - (** Match states *) - rewrite assumption_32bit. - econstructor; eauto. - - (** Match assocmaps *) - unfold Verilog.merge_regs. crush. unfold_merge. - apply regs_lessdef_add_greater. apply greater_than_max_func. - assumption. - - (** States well formed *) - unfold state_st_wf. inversion 1. crush. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - (** Equality proof *) - match goal with - | [ |- context [valueToNat ?x] ] => - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine. - 2: { reflexivity. } - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - rewrite AssocMap.gss. - setoid_rewrite H5. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - constructor. - erewrite combine_lookup_second. - simpl. - assert (Ple src (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H13. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H13. - rewrite Z_div_mult in H13; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. - rewrite H13. rewrite EXPR_OK. - rewrite array_get_error_set_bound. - reflexivity. - unfold arr_length, arr_repeat. simpl. - rewrite list_repeat_len. lia. - - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H19; try lia. - apply Zmult_lt_compat_r with (p := 4) in H19; try lia. - rewrite ZLib.div_mul_undo in H19; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- EXPR_OK. - rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). - destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). - apply Z.mul_cancel_r with (p := 4) in e; try lia. - rewrite ZLib.div_mul_undo in e; try lia. - rewrite combine_lookup_first. - eapply H7; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - apply Z2Nat.inj_iff in H13; try lia. - apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - unfold arr_stack_based_pointers. - intros. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - crush. - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - crush. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. - destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H0. - assumption. - - simpl. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - invert H0. - apply Zmult_lt_compat_r with (p := 4) in H14; try lia. - rewrite ZLib.div_mul_undo in H14; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - invert H0. - match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. - - + (** Preamble *) - invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - pose proof (RSBP r1) as RSBPr1. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. - - rewrite ARCHI in H1. crush. - subst. - clear RSBPr1. - - pose proof MASSOC as MASSOC'. - invert MASSOC'. - pose proof (H0 r0). - pose proof (H0 r1). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - assert (HPler1 : Ple r1 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto). - apply H6 in HPler0. - apply H8 in HPler1. - invert HPler0; invert HPler1; try congruence. - rewrite EQr0 in H10. - rewrite EQr1 in H12. - invert H10. invert H12. - clear H0. clear H6. clear H8. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) - (Integers.Int.repr z0)))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - rewrite Integers.Ptrofs.signed_repr; try assumption. - admit. (* FIXME: Register bounds. *) - apply PtrofsExtra.of_int_mod. - apply IntExtra.add_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - apply IntExtra.mul_mod; crush; try lia. - exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - admit. (* FIXME: Register bounds. *) - rewrite Integers.Int.signed_repr; crush; try split; try assumption. - rewrite Integers.Int.signed_repr; crush; try split; try assumption. - } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - small_tac. } - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. crush. - econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]). - econstructor. econstructor. econstructor. econstructor. - econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]). - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - - all: crush. - - (** State Lookup *) - unfold Verilog.merge_regs. - crush. - unfold_merge. - apply AssocMap.gss. - - (** Match states *) - rewrite assumption_32bit. - econstructor; eauto. - - (** Match assocmaps *) - unfold Verilog.merge_regs. crush. unfold_merge. - apply regs_lessdef_add_greater. apply greater_than_max_func. - assumption. - - (** States well formed *) - unfold state_st_wf. inversion 1. crush. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - (** Equality proof *) - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat (vdiv - (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12) - ?EQ10) (ZToValue 32 4) ?EQ9)) - as EXPR_OK by admit. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine. - 2: { reflexivity. } - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - rewrite AssocMap.gss. - setoid_rewrite H5. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) - (Integers.Int.repr z0)))) as OFFSET. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - constructor. - erewrite combine_lookup_second. - simpl. - assert (Ple src (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H20. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H20; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H20. - rewrite Z_div_mult in H20; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H20 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H20; unfold_constants; try lia. - rewrite H20. rewrite EXPR_OK. - rewrite array_get_error_set_bound. - reflexivity. - unfold arr_length, arr_repeat. simpl. - rewrite list_repeat_len. lia. - - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H22; try lia. - apply Zmult_lt_compat_r with (p := 4) in H22; try lia. - rewrite ZLib.div_mul_undo in H22; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- EXPR_OK. - rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). - destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). - apply Z.mul_cancel_r with (p := 4) in e; try lia. - rewrite ZLib.div_mul_undo in e; try lia. - rewrite combine_lookup_first. - eapply H7; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - apply Z2Nat.inj_iff in H20; try lia. - apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - unfold arr_stack_based_pointers. - intros. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - crush. - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - crush. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. - destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H0. - assumption. - - simpl. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - invert H0. - apply Zmult_lt_compat_r with (p := 4) in H21; try lia. - rewrite ZLib.div_mul_undo in H21; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - invert H0. - match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. - - + invert MARR. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - rewrite ARCHI in H0. crush. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H1. clear ZERO. - rewrite Integers.Ptrofs.add_zero_l in H1. - - remember i0 as OFFSET. - - (** Modular preservation proof *) - rename H0 into MOD_PRESERVE. - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. - crush. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - small_tac. } - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. crush. - econstructor. econstructor. econstructor. econstructor. - - all: crush. - - (** State Lookup *) - unfold Verilog.merge_regs. - crush. - unfold_merge. - apply AssocMap.gss. - - (** Match states *) - rewrite assumption_32bit. - econstructor; eauto. - - (** Match assocmaps *) - unfold Verilog.merge_regs. crush. unfold_merge. - apply regs_lessdef_add_greater. apply greater_than_max_func. - assumption. - - (** States well formed *) - unfold state_st_wf. inversion 1. crush. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - (** Equality proof *) - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) - as EXPR_OK by admit. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine. - 2: { reflexivity. } - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - rewrite AssocMap.gss. - setoid_rewrite H5. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. - - remember i0 as OFFSET. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - constructor. - erewrite combine_lookup_second. - simpl. - assert (Ple src (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H8. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H8. - rewrite Z_div_mult in H8; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. - rewrite H8. rewrite EXPR_OK. - rewrite array_get_error_set_bound. - reflexivity. - unfold arr_length, arr_repeat. simpl. - rewrite list_repeat_len. lia. - - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H12; try lia. - apply Zmult_lt_compat_r with (p := 4) in H12; try lia. - rewrite ZLib.div_mul_undo in H12; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- EXPR_OK. - rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). - destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). - apply Z.mul_cancel_r with (p := 4) in e; try lia. - rewrite ZLib.div_mul_undo in e; try lia. - rewrite combine_lookup_first. - eapply H7; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - apply Z2Nat.inj_iff in H8; try lia. - apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - unfold arr_stack_based_pointers. - intros. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - crush. - erewrite Mem.load_store_same. - 2: { rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - crush. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. - destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H0. - assumption. - - simpl. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. - simpl. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - invert H0. - apply Zmult_lt_compat_r with (p := 4) in H10; try lia. - rewrite ZLib.div_mul_undo in H10; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - invert H0. - match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. - Admitted. - Hint Resolve transl_istore_correct : htlproof. - - Lemma transl_icond_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) - (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> - Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> - pc' = (if b then ifso else ifnot) -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. - inv_state. - - eexists. split. apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - apply assumption_32bit. - eapply Verilog.stmnt_runp_Vnonblock_reg with - (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). - constructor. - - simpl. - destruct b. - eapply Verilog.erun_Vternary_true. - eapply eval_cond_correct; eauto. - constructor. - apply boolToValue_ValueToBool. - eapply Verilog.erun_Vternary_false. - eapply eval_cond_correct; eauto. - constructor. - apply boolToValue_ValueToBool. - constructor. - - big_tac. - - invert MARR. - destruct b; rewrite assumption_32bit; big_tac. - - Unshelve. - constructor. - Qed. - Hint Resolve transl_icond_correct : htlproof. - - Lemma transl_ijumptable_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) - (n : Integers.Int.int) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> - Registers.Regmap.get arg rs = Values.Vint n -> - list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - Admitted. - Hint Resolve transl_ijumptable_correct : htlproof. - - Lemma transl_ireturn_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) - (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) - (m' : mem), - (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> - Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> - forall R1 : HTL.state, - match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. - Proof. - intros s f stk pc rs m or m' H H0 R1 MSTATE. - inv_state. - - - econstructor. split. - eapply Smallstep.plus_two. - - eapply HTL.step_module; eauto. - apply assumption_32bit. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. - econstructor; simpl; trivial. - constructor. - - constructor. constructor. - - unfold state_st_wf in WF; big_tac; eauto. - apply st_greater_than_res. - apply st_greater_than_res. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge; simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply finish_not_return. - apply AssocMap.gss. - rewrite Events.E0_left. reflexivity. - - constructor; auto. - constructor. - - (* FIXME: Duplication *) - - econstructor. split. - eapply Smallstep.plus_two. - eapply HTL.step_module; eauto. - apply assumption_32bit. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. constructor. constructor. - constructor. constructor. constructor. - - unfold state_st_wf in WF; big_tac; eauto. - apply st_greater_than_res. - apply st_greater_than_res. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. - apply finish_not_return. - apply AssocMap.gss. - rewrite Events.E0_left. trivial. - - constructor; auto. - - simpl. inversion MASSOC. subst. - unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. - apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. - apply st_greater_than_res. - - Unshelve. - all: constructor. - Qed. - Hint Resolve transl_ireturn_correct : htlproof. - - Lemma transl_callstate_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) - (m : mem) (m' : Mem.mem') (stk : Values.block), - Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> - forall R1 : HTL.state, - match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states - (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) - (RTL.init_regs args (RTL.fn_params f)) m') R2. - Proof. - intros s f args m m' stk H R1 MSTATE. - - inversion MSTATE; subst. inversion TF; subst. - econstructor. split. apply Smallstep.plus_one. - eapply HTL.step_call. crush. - - apply match_state with (sp' := stk); eauto. - - all: big_tac. - - apply regs_lessdef_add_greater. - apply greater_than_max_func. - apply init_reg_assoc_empty. - - constructor. - - destruct (Mem.load AST.Mint32 m' stk - (Integers.Ptrofs.unsigned (Integers.Ptrofs.add - Integers.Ptrofs.zero - (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. - pose proof Mem.load_alloc_same as LOAD_ALLOC. - pose proof H as ALLOC. - eapply LOAD_ALLOC in ALLOC. - 2: { exact LOAD. } - ptrofs. rewrite LOAD. - rewrite ALLOC. - repeat constructor. - - ptrofs. rewrite LOAD. - repeat constructor. - - unfold reg_stack_based_pointers. intros. - unfold RTL.init_regs; crush. - destruct (RTL.fn_params f); - rewrite Registers.Regmap.gi; constructor. - - unfold arr_stack_based_pointers. intros. - crush. - destruct (Mem.load AST.Mint32 m' stk - (Integers.Ptrofs.unsigned (Integers.Ptrofs.add - Integers.Ptrofs.zero - (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. - pose proof Mem.load_alloc_same as LOAD_ALLOC. - pose proof H as ALLOC. - eapply LOAD_ALLOC in ALLOC. - 2: { exact LOAD. } - rewrite ALLOC. - repeat constructor. - constructor. - - Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) - Transparent Mem.load. - Transparent Mem.store. - unfold stack_bounds. - split. - - unfold Mem.alloc in H. - invert H. - crush. - unfold Mem.load. - intros. - match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. crush. - unfold Mem.perm_order' in H3. - small_tac. - exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. - rewrite Maps.PMap.gss in H8. - match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - crush. - apply proj_sumbool_true in H10. lia. - - unfold Mem.alloc in H. - invert H. - crush. - unfold Mem.store. - intros. - match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. crush. - unfold Mem.perm_order' in H3. - small_tac. - exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. - rewrite Maps.PMap.gss in H8. - match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - crush. - apply proj_sumbool_true in H10. lia. - Opaque Mem.alloc. - Opaque Mem.load. - Opaque Mem.store. - Qed. - Hint Resolve transl_callstate_correct : htlproof. - - Lemma transl_returnstate_correct: - forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) - (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) - (R1 : HTL.state), - match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. - Proof. - intros res0 f sp pc rs s vres m R1 MSTATE. - inversion MSTATE. inversion MF. - Qed. - Hint Resolve transl_returnstate_correct : htlproof. - - 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. - - (* Had to admit proof because currently there is no way to force main to be Internal. *) - Lemma transl_initial_states : - forall s1 : Smallstep.state (RTL.semantics prog), - Smallstep.initial_state (RTL.semantics prog) s1 -> - exists s2 : Smallstep.state (HTL.semantics tprog), - Smallstep.initial_state (HTL.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. - apply transl_module_correct. - assert (Some (AST.Internal x) = Some (AST.Internal m)). - replace (AST.fundef HTL.module) with (HTL.fundef). - rewrite <- H6. setoid_rewrite <- A. trivial. - trivial. inv H7. assumption. - Qed. - Hint Resolve transl_initial_states : htlproof. - - Lemma transl_final_states : - forall (s1 : Smallstep.state (RTL.semantics prog)) - (s2 : Smallstep.state (HTL.semantics tprog)) - (r : Integers.Int.int), - match_states s1 s2 -> - Smallstep.final_state (RTL.semantics prog) s1 r -> - Smallstep.final_state (HTL.semantics tprog) s2 r. - Proof. - intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. - Qed. - Hint Resolve transl_final_states : htlproof. - - Theorem transl_step_correct: - forall (S1 : RTL.state) t S2, - RTL.step ge S1 t S2 -> - forall (R1 : HTL.state), - match_states S1 R1 -> - exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. - Proof. - induction 1; eauto with htlproof; (intros; inv_state). - Qed. - Hint Resolve transl_step_correct : htlproof. +(* 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 : RTL.genv := Globalenvs.Genv.globalenv prog. *) +(* Let tge : HTL.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: RTL.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: RTL.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'). *) +(* 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 pc' res0 pc f e fin rtrn st stk, *) +(* tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') *) +(* (Verilog.Vnonblock (Verilog.Vvar res0) e) *) +(* (state_goto st pc') -> *) +(* reg_stack_based_pointers sp rs -> *) +(* (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *) +(* @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op *) +(* (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) *) +(* | |- context[match ?g with _ => _ end] => destruct g; try discriminate *) +(* | |- _ => simplify; solve [auto] *) +(* end. *) +(* intros F V sp v m args rs op g pc' res0 pc f e fin rtrn st stk INSTR RSBP SEL EVAL. *) +(* inv INSTR. unfold translate_instr in H5. *) +(* unfold_match H5; repeat (unfold_match H5); repeat (simplify; 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 eval_correct : *) +(* forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, *) +(* match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> *) +(* (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *) +(* 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 s = OK e s' i -> *) +(* exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. *) +(* Proof. *) +(* Ltac eval_correct_tac := *) +(* match goal with *) +(* | |- context[valueToPtr] => unfold valueToPtr *) +(* | |- context[valueToInt] => unfold valueToInt *) +(* | |- context[bop] => unfold bop *) +(* | |- context[boplit] => unfold boplit *) +(* | |- 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 : context[RTL.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 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* apply H in HPle1; apply H in HPle2; eexists; split; *) +(* [econstructor; eauto; constructor; trivial | inv HPle1; inv HPle2; try (constructor; auto)] *) +(* | H : context[RTL.max_reg_function ?f] *) +(* |- context[_ (Registers.Regmap.get ?r ?rs) _] => *) +(* let HPle1 := fresh "HPle" in *) +(* assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; 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 *) +(* | |- Verilog.expr_runp _ _ _ _ _ => econstructor *) +(* | |- 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[RTL.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 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* apply H in HPle1; apply H in HPle2; eexists; split; try constructor; eauto *) +(* | H : context[RTL.max_reg_function ?f] |- context[Verilog.Vvar ?r] => *) +(* let HPle := fresh "H" in *) +(* assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* apply H in HPle; eexists; split; try constructor; eauto *) +(* | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate *) +(* end. *) +(* intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. *) +(* 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 *) +(* - pose proof Integers.Ptrofs.agree32_sub as H2; unfold Integers.Ptrofs.agree32 in H2. *) +(* unfold Ptrofs.of_int. simpl. *) +(* apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H2 in H3. *) +(* rewrite Ptrofs.unsigned_repr. apply H3. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *) +(* apply Int.unsigned_range_2. *) +(* auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *) +(* apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. *) +(* replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *) +(* apply Int.unsigned_range_2. *) +(* - pose proof Integers.Ptrofs.agree32_sub as AGR; unfold Integers.Ptrofs.agree32 in AGR. *) +(* assert (ARCH: Archi.ptr64 = false) by auto. eapply AGR in ARCH. *) +(* apply int_inj. unfold Ptrofs.to_int. rewrite Int.unsigned_repr. *) +(* apply ARCH. Search Ptrofs.unsigned. pose proof Ptrofs.unsigned_range_2. *) +(* replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *) +(* pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. *) +(* eapply H2 in ARCH. apply ARCH. *) +(* pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. *) +(* eapply H2 in ARCH. apply ARCH. *) +(* - admit. (* mulhs *) *) +(* - admit. (* mulhu *) *) +(* - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. *) +(* - rewrite Heqb in Heqb0. discriminate. *) +(* - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. *) +(* - rewrite Heqb in Heqb0. discriminate. *) +(* - admit. *) +(* - admit. (* ror *) *) +(* - admit. (* addressing *) *) +(* - admit. (* eval_condition *) *) +(* - admit. (* select *) *) +(* Admitted. *) + +(* Lemma eval_cond_correct : *) +(* forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, *) +(* translate_condition cond args s1 = OK c s' i -> *) +(* Op.eval_condition *) +(* cond *) +(* (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) *) +(* m = Some b -> *) +(* Verilog.expr_runp f asr asa c (boolToValue b). *) +(* Admitted. *) + +(* (** The proof of semantic preservation for the translation of instructions *) +(* is a simulation argument based on diagrams of the following form: *) +(* << *) +(* match_states *) +(* code st rs ---------------- State m st assoc *) +(* || | *) +(* || | *) +(* || | *) +(* \/ v *) +(* code st rs' --------------- State m st assoc' *) +(* match_states *) +(* >> *) +(* where [tr_code c data control fin rtrn st] is assumed to hold. *) + +(* The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. *) +(* *) *) + +(* Definition transl_instr_prop (instr : RTL.instruction) : Prop := *) +(* forall m asr asa fin rtrn st stmt trans res, *) +(* tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> *) +(* exists asr' asa', *) +(* HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). *) + +(* Opaque combine. *) + +(* Ltac tac0 := *) +(* match goal with *) +(* | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs *) +(* | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr *) +(* | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge *) +(* | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros *) +(* | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set *) + +(* | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack *) + +(* | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss *) +(* | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso *) +(* | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty *) + +(* | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => *) +(* rewrite combine_lookup_first *) + +(* | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 *) +(* | [ |- context[match_states _ _] ] => econstructor; auto *) +(* | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto *) +(* | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => *) +(* apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] *) + +(* | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => *) +(* unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal *) +(* | [ |- context[(AssocMap.combine _ _ _) ! _] ] => *) +(* try (rewrite AssocMap.gcombine; [> | reflexivity]) *) + +(* | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => *) +(* rewrite Registers.Regmap.gss *) +(* | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => *) +(* destruct (Pos.eq_dec s d) as [EQ|EQ]; *) +(* [> rewrite EQ | rewrite Registers.Regmap.gso; auto] *) + +(* | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H *) +(* | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] *) +(* | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H *) +(* end. *) + +(* Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. *) +(* Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. *) + +(* Lemma transl_inop_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) +(* (rs : RTL.regset) (m : mem) (pc' : RTL.node), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f sp pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) +(* Proof. *) +(* intros s f sp pc rs m pc' H R1 MSTATE. *) +(* inv_state. *) + +(* unfold match_prog in TRANSL. *) +(* econstructor. *) +(* split. *) +(* apply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* inv CONST; assumption. *) +(* inv CONST; assumption. *) +(* (* processing of state *) *) +(* econstructor. *) +(* crush. *) +(* econstructor. *) +(* econstructor. *) +(* econstructor. *) + +(* all: invert MARR; big_tac. *) + +(* inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. *) + +(* Unshelve. auto. *) +(* Qed. *) +(* Hint Resolve transl_inop_correct : htlproof. *) + +(* Lemma transl_iop_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) +(* (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) *) +(* (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *) +(* Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f sp pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) +(* match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. *) +(* Proof. *) +(* intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. *) +(* inv_state. inv MARR. *) +(* exploit eval_correct; eauto. intros. inversion H1. inversion H2. *) +(* econstructor. split. *) +(* apply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* inv CONST. assumption. *) +(* inv CONST. assumption. *) +(* econstructor; simpl; trivial. *) +(* constructor; trivial. *) +(* econstructor; simpl; eauto. *) +(* simpl. econstructor. econstructor. *) +(* apply H5. simplify. *) + +(* all: big_tac. *) + +(* assert (HPle: Ple res0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + +(* unfold Ple in HPle. lia. *) +(* apply regs_lessdef_add_match. assumption. *) +(* apply regs_lessdef_add_greater. unfold Plt; lia. assumption. *) +(* assert (HPle: Ple res0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) +(* unfold Ple in HPle; lia. *) +(* eapply op_stack_based; eauto. *) +(* inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *) +(* assumption. lia. *) +(* assert (HPle: Ple res0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) +(* unfold Ple in HPle. lia. *) +(* rewrite AssocMap.gso. rewrite AssocMap.gso. *) +(* assumption. lia. *) +(* assert (HPle: Ple res0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) +(* unfold Ple in HPle. lia. *) +(* Unshelve. trivial. *) +(* Qed. *) +(* Hint Resolve transl_iop_correct : htlproof. *) + +(* Ltac tac := *) +(* repeat match goal with *) +(* | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate *) +(* | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => *) +(* let EQ1 := fresh "EQ" in *) +(* let EQ2 := fresh "EQ" in *) +(* destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * *) +(* | [ _ : context[if ?x then _ else _] |- _ ] => *) +(* let EQ := fresh "EQ" in *) +(* destruct x eqn:EQ; simpl in * *) +(* | [ H : ret _ _ = _ |- _ ] => invert H *) +(* | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x *) +(* end. *) + +(* Ltac inv_arr_access := *) +(* match goal with *) +(* | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => *) +(* destruct c, chunk, addr, args; crush; tac; crush *) +(* end. *) + +(* Lemma transl_iload_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) +(* (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *) +(* (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) *) +(* (pc' : RTL.node) (a v : Values.val), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> *) +(* Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *) +(* Mem.loadv chunk m a = Some v -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f sp pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) +(* match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. *) +(* Proof. *) +(* intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. *) +(* inv_state. inv_arr_access. *) + +(* + (** Preamble *) *) +(* invert MARR. crush. *) + +(* unfold Op.eval_addressing in H0. *) +(* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + +(* unfold reg_stack_based_pointers in RSBP. *) +(* pose proof (RSBP r0) as RSBPr0. *) + +(* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *) + +(* rewrite ARCHI in H1. crush. *) +(* subst. *) + +(* pose proof MASSOC as MASSOC'. *) +(* invert MASSOC'. *) +(* pose proof (H0 r0). *) +(* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) +(* apply H6 in HPler0. *) +(* invert HPler0; try congruence. *) +(* rewrite EQr0 in H8. *) +(* invert H8. *) +(* clear H0. clear H6. *) + +(* unfold check_address_parameter_signed in *; *) +(* unfold check_address_parameter_unsigned in *; crush. *) + +(* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) +(* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + +(* (** Modular preservation proof *) *) +(* (*assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) +(* { rewrite HeqOFFSET. *) +(* apply PtrofsExtra.add_mod; crush. *) +(* rewrite Integers.Ptrofs.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. *) +(* apply PtrofsExtra.of_int_mod. *) +(* rewrite Integers.Int.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. } *) + +(* (** Read bounds proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) +(* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) +(* unfold stack_bounds in BOUNDS. *) +(* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *) +(* split; try lia; apply Integers.Ptrofs.unsigned_range_2. *) +(* small_tac. } *) + +(* (** Normalisation proof *) *) +(* assert (Integers.Ptrofs.repr *) +(* (4 * Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *) +(* as NORMALISE. *) +(* { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *) +(* rewrite <- PtrofsExtra.mul_unsigned. *) +(* apply PtrofsExtra.mul_divu; crush; auto. } *) + +(* (** Normalised bounds proof *) *) +(* assert (0 <= *) +(* Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *) +(* < (RTL.fn_stacksize f / 4)) *) +(* as NORMALISE_BOUND. *) +(* { split. *) +(* apply Integers.Ptrofs.unsigned_range_2. *) +(* assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *) +(* unfold Integers.Ptrofs.divu at 2 in H0. *) +(* rewrite H0. clear H0. *) +(* rewrite Integers.Ptrofs.unsigned_repr; crush. *) +(* apply Zmult_lt_reg_r with (p := 4); try lia. *) +(* repeat rewrite ZLib.div_mul_undo; try lia. *) +(* apply Z.div_pos; small_tac. *) +(* apply Z.div_le_upper_bound; small_tac. } *) + +(* inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *) +(* clear NORMALISE_BOUND. *) + +(* (** Start of proof proper *) *) +(* eexists. split. *) +(* eapply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* apply assumption_32bit. *) +(* econstructor. econstructor. econstructor. crush. *) +(* econstructor. econstructor. econstructor. crush. *) +(* econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) + +(* all: big_tac. *) + +(* 1: { *) +(* assert (HPle : Ple dst (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_def. eassumption. auto. *) +(* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) +(* } *) + +(* 2: { *) +(* assert (HPle : Ple dst (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_def. eassumption. auto. *) +(* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) +(* } *) + +(* (** Match assocmaps *) *) +(* apply regs_lessdef_add_match; big_tac. *) + +(* (** Equality proof *) *) +(* match goal with *) +(* | [ |- context [valueToNat ?x] ] => *) +(* assert (Z.to_nat *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4))) *) +(* = *) +(* valueToNat x) *) +(* as EXPR_OK by admit *) +(* end. *) +(* rewrite <- EXPR_OK. *) + +(* specialize (H7 (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4)))). *) +(* exploit H7; big_tac. *) + +(* (** RSBP preservation *) *) +(* unfold arr_stack_based_pointers in ASBP. *) +(* specialize (ASBP (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) +(* exploit ASBP; big_tac. *) +(* rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *) + +(* + (** Preamble *) *) +(* invert MARR. crush. *) + +(* unfold Op.eval_addressing in H0. *) +(* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + +(* unfold reg_stack_based_pointers in RSBP. *) +(* pose proof (RSBP r0) as RSBPr0. *) +(* pose proof (RSBP r1) as RSBPr1. *) + +(* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *) +(* destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *) + +(* rewrite ARCHI in H1. crush. *) +(* subst. *) +(* clear RSBPr1. *) + +(* pose proof MASSOC as MASSOC'. *) +(* invert MASSOC'. *) +(* pose proof (H0 r0). *) +(* pose proof (H0 r1). *) +(* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) +(* assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *) +(* apply H6 in HPler0. *) +(* apply H8 in HPler1. *) +(* invert HPler0; invert HPler1; try congruence. *) +(* rewrite EQr0 in H9. *) +(* rewrite EQr1 in H11. *) +(* invert H9. invert H11. *) +(* clear H0. clear H6. clear H8. *) + +(* unfold check_address_parameter_signed in *; *) +(* unfold check_address_parameter_unsigned in *; crush. *) + +(* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) +(* (Integers.Ptrofs.of_int *) +(* (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *) +(* (Integers.Int.repr z0)))) as OFFSET. *) + +(* (** Modular preservation proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) +(* { rewrite HeqOFFSET. *) +(* apply PtrofsExtra.add_mod; crush; try lia. *) +(* rewrite Integers.Ptrofs.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. *) +(* apply PtrofsExtra.of_int_mod. *) +(* apply IntExtra.add_mod; crush. *) +(* apply IntExtra.mul_mod2; crush. *) +(* rewrite Integers.Int.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. *) +(* rewrite Integers.Int.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. } *) + +(* (** Read bounds proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) +(* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) +(* unfold stack_bounds in BOUNDS. *) +(* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *) +(* split; try lia; apply Integers.Ptrofs.unsigned_range_2. *) +(* small_tac. } *) + +(* (** Normalisation proof *) *) +(* assert (Integers.Ptrofs.repr *) +(* (4 * Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *) +(* as NORMALISE. *) +(* { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *) +(* rewrite <- PtrofsExtra.mul_unsigned. *) +(* apply PtrofsExtra.mul_divu; crush. } *) + +(* (** Normalised bounds proof *) *) +(* assert (0 <= *) +(* Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *) +(* < (RTL.fn_stacksize f / 4)) *) +(* as NORMALISE_BOUND. *) +(* { split. *) +(* apply Integers.Ptrofs.unsigned_range_2. *) +(* assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *) +(* unfold Integers.Ptrofs.divu at 2 in H0. *) +(* rewrite H0. clear H0. *) +(* rewrite Integers.Ptrofs.unsigned_repr; crush. *) +(* apply Zmult_lt_reg_r with (p := 4); try lia. *) +(* repeat rewrite ZLib.div_mul_undo; try lia. *) +(* apply Z.div_pos; small_tac. *) +(* apply Z.div_le_upper_bound; lia. } *) + +(* inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *) +(* clear NORMALISE_BOUND. *) + +(* (** Start of proof proper *) *) +(* eexists. split. *) +(* eapply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* apply assumption_32bit. *) +(* econstructor. econstructor. econstructor. crush. *) +(* econstructor. econstructor. econstructor. crush. *) +(* econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. *) + +(* all: big_tac. *) + +(* 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_def. eassumption. auto. *) +(* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + +(* 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_def. eassumption. auto. *) +(* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + +(* (** Match assocmaps *) *) +(* apply regs_lessdef_add_match; big_tac. *) + +(* (** Equality proof *) *) +(* match goal with *) +(* | [ |- context [valueToNat ?x] ] => *) +(* assert (Z.to_nat *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4))) *) +(* = *) +(* valueToNat x) *) +(* as EXPR_OK by admit *) +(* end. *) +(* rewrite <- EXPR_OK. *) + +(* specialize (H7 (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4)))). *) +(* exploit H7; big_tac. *) + +(* (** RSBP preservation *) *) +(* unfold arr_stack_based_pointers in ASBP. *) +(* specialize (ASBP (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) +(* exploit ASBP; big_tac. *) +(* rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *) + +(* + invert MARR. crush. *) + +(* unfold Op.eval_addressing in H0. *) +(* destruct (Archi.ptr64) eqn:ARCHI; crush. *) +(* rewrite ARCHI in H0. crush. *) + +(* unfold check_address_parameter_unsigned in *; *) +(* unfold check_address_parameter_signed in *; crush. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* rewrite ZERO in H1. clear ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l in H1. *) + +(* remember i0 as OFFSET. *) + +(* (** Modular preservation proof *) *) +(* rename H0 into MOD_PRESERVE. *) + +(* (** Read bounds proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) +(* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) +(* unfold stack_bounds in BOUNDS. *) +(* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } *) + +(* (** Normalisation proof *) *) +(* assert (Integers.Ptrofs.repr *) +(* (4 * Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *) +(* as NORMALISE. *) +(* { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *) +(* rewrite <- PtrofsExtra.mul_unsigned. *) +(* apply PtrofsExtra.mul_divu; crush. } *) + +(* (** Normalised bounds proof *) *) +(* assert (0 <= *) +(* Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *) +(* < (RTL.fn_stacksize f / 4)) *) +(* as NORMALISE_BOUND. *) +(* { split. *) +(* apply Integers.Ptrofs.unsigned_range_2. *) +(* assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *) +(* unfold Integers.Ptrofs.divu at 2 in H0. *) +(* rewrite H0. clear H0. *) +(* rewrite Integers.Ptrofs.unsigned_repr; crush. *) +(* apply Zmult_lt_reg_r with (p := 4); try lia. *) +(* repeat rewrite ZLib.div_mul_undo; try lia. *) +(* apply Z.div_pos; small_tac. *) +(* apply Z.div_le_upper_bound; lia. } *) + +(* inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *) +(* clear NORMALISE_BOUND. *) + +(* (** Start of proof proper *) *) +(* eexists. split. *) +(* eapply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* apply assumption_32bit. *) +(* econstructor. econstructor. econstructor. crush. *) +(* econstructor. econstructor. econstructor. econstructor. crush. *) + +(* all: big_tac. *) + +(* 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_def. eassumption. auto. *) +(* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + +(* 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_def. eassumption. auto. *) +(* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + +(* (** Match assocmaps *) *) +(* apply regs_lessdef_add_match; big_tac. *) + +(* (** Equality proof *) *) +(* match goal with (* Prevents issues with evars *) *) +(* | [ |- context [valueToNat ?x] ] => *) +(* assert (Z.to_nat *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4))) *) +(* = *) +(* valueToNat x) *) +(* as EXPR_OK by admit *) +(* end. *) +(* rewrite <- EXPR_OK. *) + +(* specialize (H7 (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4)))). *) +(* exploit H7; big_tac. *) + +(* (** RSBP preservation *) *) +(* unfold arr_stack_based_pointers in ASBP. *) +(* specialize (ASBP (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) +(* exploit ASBP; big_tac. *) +(* rewrite NORMALISE in H0. rewrite H1 in H0. assumption.*) *) +(* Admitted. *) +(* Hint Resolve transl_iload_correct : htlproof. *) + +(* Lemma transl_istore_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) +(* (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *) +(* (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg) *) +(* (pc' : RTL.node) (a : Values.val) (m' : mem), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> *) +(* Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *) +(* Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f sp pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. *) +(* Proof. *) +(* (* intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. *) +(* inv_state. inv_arr_access. *) + +(* + (** Preamble *) *) +(* invert MARR. crush. *) + +(* unfold Op.eval_addressing in H0. *) +(* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + +(* unfold reg_stack_based_pointers in RSBP. *) +(* pose proof (RSBP r0) as RSBPr0. *) + +(* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *) + +(* rewrite ARCHI in H1. crush. *) +(* subst. *) + +(* pose proof MASSOC as MASSOC'. *) +(* invert MASSOC'. *) +(* pose proof (H0 r0). *) +(* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) +(* apply H6 in HPler0. *) +(* invert HPler0; try congruence. *) +(* rewrite EQr0 in H8. *) +(* invert H8. *) +(* clear H0. clear H6. *) + +(* unfold check_address_parameter_unsigned in *; *) +(* unfold check_address_parameter_signed in *; crush. *) + +(* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) +(* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + +(* (** Modular preservation proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) +(* { rewrite HeqOFFSET. *) +(* apply PtrofsExtra.add_mod; crush; try lia. *) +(* rewrite Integers.Ptrofs.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. *) +(* apply PtrofsExtra.of_int_mod. *) +(* rewrite Integers.Int.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. } *) + +(* (** Write bounds proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) +(* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) +(* unfold stack_bounds in BOUNDS. *) +(* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) + +(* (** Start of proof proper *) *) +(* eexists. split. *) +(* eapply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* apply assumption_32bit. *) +(* econstructor. econstructor. econstructor. *) +(* eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *) +(* econstructor. *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). *) +(* econstructor. *) +(* econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) + +(* all: crush. *) + +(* (** State Lookup *) *) +(* unfold Verilog.merge_regs. *) +(* crush. *) +(* unfold_merge. *) +(* apply AssocMap.gss. *) + +(* (** Match states *) *) +(* rewrite assumption_32bit. *) +(* econstructor; eauto. *) + +(* (** Match assocmaps *) *) +(* unfold Verilog.merge_regs. crush. unfold_merge. *) +(* apply regs_lessdef_add_greater. *) +(* unfold Plt; lia. *) +(* assumption. *) + +(* (** States well formed *) *) +(* unfold state_st_wf. inversion 1. crush. *) +(* unfold Verilog.merge_regs. *) +(* unfold_merge. *) +(* apply AssocMap.gss. *) + +(* (** Equality proof *) *) +(* match goal with *) +(* | [ |- context [valueToNat ?x] ] => *) +(* assert (Z.to_nat *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4))) *) +(* = *) +(* valueToNat x) *) +(* as EXPR_OK by admit *) +(* end. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + +(* econstructor. *) +(* repeat split; crush. *) +(* unfold HTL.empty_stack. *) +(* crush. *) +(* unfold Verilog.merge_arrs. *) + +(* rewrite AssocMap.gcombine. *) +(* 2: { reflexivity. } *) +(* unfold Verilog.arr_assocmap_set. *) +(* rewrite AssocMap.gss. *) +(* unfold Verilog.merge_arr. *) +(* rewrite AssocMap.gss. *) +(* setoid_rewrite H5. *) +(* reflexivity. *) + +(* rewrite combine_length. *) +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* apply list_repeat_len. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. *) +(* rewrite H4. reflexivity. *) + +(* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) +(* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + +(* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + +(* erewrite Mem.load_store_same. *) +(* 2: { rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite e. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* exact H1. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) +(* constructor. *) +(* erewrite combine_lookup_second. *) +(* simpl. *) +(* assert (Ple src (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* apply H0 in H13. *) +(* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. auto. *) + +(* assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) +(* rewrite Z.mul_comm in H13. *) +(* rewrite Z_div_mult in H13; try lia. *) +(* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. *) +(* rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. *) +(* rewrite H13. rewrite EXPR_OK. *) +(* rewrite array_get_error_set_bound. *) +(* reflexivity. *) +(* unfold arr_length, arr_repeat. simpl. *) +(* rewrite list_repeat_len. lia. *) + +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* simpl. *) +(* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) +(* right. *) +(* apply ZExtra.mod_0_bounds; try lia. *) +(* apply ZLib.Z_mod_mult'. *) +(* rewrite Z2Nat.id in H15; try lia. *) +(* apply Zmult_lt_compat_r with (p := 4) in H15; try lia. *) +(* rewrite ZLib.div_mul_undo in H15; try lia. *) +(* split; try lia. *) +(* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) +(* } *) + +(* rewrite <- EXPR_OK. *) +(* rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *) +(* destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *) +(* apply Z.mul_cancel_r with (p := 4) in e; try lia. *) +(* rewrite ZLib.div_mul_undo in e; try lia. *) +(* rewrite combine_lookup_first. *) +(* eapply H7; eauto. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. auto. *) +(* rewrite array_gso. *) +(* unfold array_get_error. *) +(* unfold arr_repeat. *) +(* crush. *) +(* apply list_repeat_lookup. *) +(* lia. *) +(* unfold_constants. *) +(* intro. *) +(* apply Z2Nat.inj_iff in H13; try lia. *) +(* apply Z.div_pos; try lia. *) +(* apply Integers.Ptrofs.unsigned_range. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* unfold arr_stack_based_pointers. *) +(* intros. *) +(* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + +(* crush. *) +(* erewrite Mem.load_store_same. *) +(* 2: { rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite e. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* exact H1. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) +(* crush. *) +(* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *) +(* destruct (Archi.ptr64); try discriminate. *) +(* pose proof (RSBP src). rewrite EQ_SRC in H0. *) +(* assumption. *) + +(* simpl. *) +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* simpl. *) +(* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) +(* right. *) +(* apply ZExtra.mod_0_bounds; try lia. *) +(* apply ZLib.Z_mod_mult'. *) +(* invert H0. *) +(* apply Zmult_lt_compat_r with (p := 4) in H14; try lia. *) +(* rewrite ZLib.div_mul_undo in H14; try lia. *) +(* split; try lia. *) +(* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) +(* } *) +(* apply ASBP; assumption. *) + +(* unfold stack_bounds in *. intros. *) +(* simpl. *) +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. right. simpl. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) +(* apply ZExtra.mod_0_bounds; crush; try lia. } *) +(* crush. *) +(* exploit (BOUNDS ptr); try lia. intros. crush. *) +(* exploit (BOUNDS ptr v); try lia. intros. *) +(* invert H0. *) +(* match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *) +(* assert (Mem.valid_access m AST.Mint32 sp' *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) +(* (Integers.Ptrofs.repr ptr))) Writable). *) +(* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) +(* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) +(* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) +(* (Integers.Ptrofs.repr ptr))) v). *) +(* apply X in H0. invert H0. congruence. *) + +(* + (** Preamble *) *) +(* invert MARR. crush. *) + +(* unfold Op.eval_addressing in H0. *) +(* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + +(* unfold reg_stack_based_pointers in RSBP. *) +(* pose proof (RSBP r0) as RSBPr0. *) +(* pose proof (RSBP r1) as RSBPr1. *) + +(* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *) +(* destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *) + +(* rewrite ARCHI in H1. crush. *) +(* subst. *) +(* clear RSBPr1. *) + +(* pose proof MASSOC as MASSOC'. *) +(* invert MASSOC'. *) +(* pose proof (H0 r0). *) +(* pose proof (H0 r1). *) +(* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) +(* assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *) +(* apply H6 in HPler0. *) +(* apply H8 in HPler1. *) +(* invert HPler0; invert HPler1; try congruence. *) +(* rewrite EQr0 in H9. *) +(* rewrite EQr1 in H11. *) +(* invert H9. invert H11. *) +(* clear H0. clear H6. clear H8. *) + +(* unfold check_address_parameter_signed in *; *) +(* unfold check_address_parameter_unsigned in *; crush. *) + +(* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) +(* (Integers.Ptrofs.of_int *) +(* (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *) +(* (Integers.Int.repr z0)))) as OFFSET. *) + +(* (** Modular preservation proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) +(* { rewrite HeqOFFSET. *) +(* apply PtrofsExtra.add_mod; crush; try lia. *) +(* rewrite Integers.Ptrofs.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. *) +(* apply PtrofsExtra.of_int_mod. *) +(* apply IntExtra.add_mod; crush. *) +(* apply IntExtra.mul_mod2; crush. *) +(* rewrite Integers.Int.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. *) +(* rewrite Integers.Int.unsigned_repr_eq. *) +(* rewrite <- Zmod_div_mod; crush. } *) + +(* (** Write bounds proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) +(* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) +(* unfold stack_bounds in BOUNDS. *) +(* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *) +(* split; try lia; apply Integers.Ptrofs.unsigned_range_2. *) +(* small_tac. } *) + +(* (** Start of proof proper *) *) +(* eexists. split. *) +(* eapply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* apply assumption_32bit. *) +(* econstructor. econstructor. econstructor. *) +(* eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *) +(* econstructor. *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]). *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]). *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]). *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. *) +(* eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]). *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) +(* econstructor. econstructor. econstructor. econstructor. *) + +(* all: crush. *) + +(* (** State Lookup *) *) +(* unfold Verilog.merge_regs. *) +(* crush. *) +(* unfold_merge. *) +(* apply AssocMap.gss. *) + +(* (** Match states *) *) +(* rewrite assumption_32bit. *) +(* econstructor; eauto. *) + +(* (** Match assocmaps *) *) +(* unfold Verilog.merge_regs. crush. unfold_merge. *) +(* apply regs_lessdef_add_greater. *) +(* unfold Plt; lia. *) +(* assumption. *) + +(* (** States well formed *) *) +(* unfold state_st_wf. inversion 1. crush. *) +(* unfold Verilog.merge_regs. *) +(* unfold_merge. *) +(* apply AssocMap.gss. *) + +(* (** Equality proof *) *) +(* assert (Z.to_nat *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4))) *) +(* = *) +(* valueToNat (vdiv *) +(* (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12) *) +(* ?EQ10) (ZToValue 32 4) ?EQ9)) *) +(* as EXPR_OK by admit. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + +(* econstructor. *) +(* repeat split; crush. *) +(* unfold HTL.empty_stack. *) +(* crush. *) +(* unfold Verilog.merge_arrs. *) + +(* rewrite AssocMap.gcombine. *) +(* 2: { reflexivity. } *) +(* unfold Verilog.arr_assocmap_set. *) +(* rewrite AssocMap.gss. *) +(* unfold Verilog.merge_arr. *) +(* rewrite AssocMap.gss. *) +(* setoid_rewrite H5. *) +(* reflexivity. *) + +(* rewrite combine_length. *) +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* apply list_repeat_len. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. *) +(* rewrite H4. reflexivity. *) + +(* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) +(* (Integers.Ptrofs.of_int *) +(* (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *) +(* (Integers.Int.repr z0)))) as OFFSET. *) +(* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + +(* erewrite Mem.load_store_same. *) +(* 2: { rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite e. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* exact H1. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) +(* constructor. *) +(* erewrite combine_lookup_second. *) +(* simpl. *) +(* assert (Ple src (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* apply H0 in H16. *) +(* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H16; eauto. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. auto. *) + +(* assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) +(* rewrite Z.mul_comm in H16. *) +(* rewrite Z_div_mult in H16; try lia. *) +(* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H16 by reflexivity. *) +(* rewrite <- PtrofsExtra.divu_unsigned in H16; unfold_constants; try lia. *) +(* rewrite H16. rewrite EXPR_OK. *) +(* rewrite array_get_error_set_bound. *) +(* reflexivity. *) +(* unfold arr_length, arr_repeat. simpl. *) +(* rewrite list_repeat_len. lia. *) + +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* simpl. *) +(* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) +(* right. *) +(* apply ZExtra.mod_0_bounds; try lia. *) +(* apply ZLib.Z_mod_mult'. *) +(* rewrite Z2Nat.id in H18; try lia. *) +(* apply Zmult_lt_compat_r with (p := 4) in H18; try lia. *) +(* rewrite ZLib.div_mul_undo in H18; try lia. *) +(* split; try lia. *) +(* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) +(* } *) + +(* rewrite <- EXPR_OK. *) +(* rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *) +(* destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *) +(* apply Z.mul_cancel_r with (p := 4) in e; try lia. *) +(* rewrite ZLib.div_mul_undo in e; try lia. *) +(* rewrite combine_lookup_first. *) +(* eapply H7; eauto. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. auto. *) +(* rewrite array_gso. *) +(* unfold array_get_error. *) +(* unfold arr_repeat. *) +(* crush. *) +(* apply list_repeat_lookup. *) +(* lia. *) +(* unfold_constants. *) +(* intro. *) +(* apply Z2Nat.inj_iff in H16; try lia. *) +(* apply Z.div_pos; try lia. *) +(* apply Integers.Ptrofs.unsigned_range. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* unfold arr_stack_based_pointers. *) +(* intros. *) +(* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + +(* crush. *) +(* erewrite Mem.load_store_same. *) +(* 2: { rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite e. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* exact H1. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) +(* crush. *) +(* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *) +(* destruct (Archi.ptr64); try discriminate. *) +(* pose proof (RSBP src). rewrite EQ_SRC in H0. *) +(* assumption. *) + +(* simpl. *) +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* simpl. *) +(* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) +(* right. *) +(* apply ZExtra.mod_0_bounds; try lia. *) +(* apply ZLib.Z_mod_mult'. *) +(* invert H0. *) +(* apply Zmult_lt_compat_r with (p := 4) in H17; try lia. *) +(* rewrite ZLib.div_mul_undo in H17; try lia. *) +(* split; try lia. *) +(* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) +(* } *) +(* apply ASBP; assumption. *) + +(* unfold stack_bounds in *. intros. *) +(* simpl. *) +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. right. simpl. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) +(* apply ZExtra.mod_0_bounds; crush; try lia. } *) +(* crush. *) +(* exploit (BOUNDS ptr); try lia. intros. crush. *) +(* exploit (BOUNDS ptr v); try lia. intros. *) +(* invert H0. *) +(* match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *) +(* assert (Mem.valid_access m AST.Mint32 sp' *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) +(* (Integers.Ptrofs.repr ptr))) Writable). *) +(* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) +(* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) +(* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) +(* (Integers.Ptrofs.repr ptr))) v). *) +(* apply X in H0. invert H0. congruence. *) + +(* + invert MARR. crush. *) + +(* unfold Op.eval_addressing in H0. *) +(* destruct (Archi.ptr64) eqn:ARCHI; crush. *) +(* rewrite ARCHI in H0. crush. *) + +(* unfold check_address_parameter_unsigned in *; *) +(* unfold check_address_parameter_signed in *; crush. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* rewrite ZERO in H1. clear ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l in H1. *) + +(* remember i0 as OFFSET. *) + +(* (** Modular preservation proof *) *) +(* rename H0 into MOD_PRESERVE. *) + +(* (** Write bounds proof *) *) +(* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) +(* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) +(* unfold stack_bounds in BOUNDS. *) +(* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *) +(* crush. *) +(* replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. *) +(* small_tac. } *) + +(* (** Start of proof proper *) *) +(* eexists. split. *) +(* eapply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* apply assumption_32bit. *) +(* econstructor. econstructor. econstructor. *) +(* eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *) +(* econstructor. econstructor. econstructor. econstructor. *) + +(* all: crush. *) + +(* (** State Lookup *) *) +(* unfold Verilog.merge_regs. *) +(* crush. *) +(* unfold_merge. *) +(* apply AssocMap.gss. *) + +(* (** Match states *) *) +(* rewrite assumption_32bit. *) +(* econstructor; eauto. *) + +(* (** Match assocmaps *) *) +(* unfold Verilog.merge_regs. crush. unfold_merge. *) +(* apply regs_lessdef_add_greater. *) +(* unfold Plt; lia. *) +(* assumption. *) + +(* (** States well formed *) *) +(* unfold state_st_wf. inversion 1. crush. *) +(* unfold Verilog.merge_regs. *) +(* unfold_merge. *) +(* apply AssocMap.gss. *) + +(* (** Equality proof *) *) +(* assert (Z.to_nat *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.divu *) +(* OFFSET *) +(* (Integers.Ptrofs.repr 4))) *) +(* = *) +(* valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) *) +(* as EXPR_OK by admit. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + +(* econstructor. *) +(* repeat split; crush. *) +(* unfold HTL.empty_stack. *) +(* crush. *) +(* unfold Verilog.merge_arrs. *) + +(* rewrite AssocMap.gcombine. *) +(* 2: { reflexivity. } *) +(* unfold Verilog.arr_assocmap_set. *) +(* rewrite AssocMap.gss. *) +(* unfold Verilog.merge_arr. *) +(* rewrite AssocMap.gss. *) +(* setoid_rewrite H5. *) +(* reflexivity. *) + +(* rewrite combine_length. *) +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* apply list_repeat_len. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. *) +(* rewrite H4. reflexivity. *) + +(* remember i0 as OFFSET. *) +(* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + +(* erewrite Mem.load_store_same. *) +(* 2: { rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite e. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* exact H1. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) +(* constructor. *) +(* erewrite combine_lookup_second. *) +(* simpl. *) +(* assert (Ple src (RTL.max_reg_function f)) *) +(* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) +(* apply H0 in H8. *) +(* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. auto. *) + +(* assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) +(* rewrite Z.mul_comm in H8. *) +(* rewrite Z_div_mult in H8; try lia. *) +(* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. *) +(* rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. *) +(* rewrite H8. rewrite EXPR_OK. *) +(* rewrite array_get_error_set_bound. *) +(* reflexivity. *) +(* unfold arr_length, arr_repeat. simpl. *) +(* rewrite list_repeat_len. lia. *) + +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* simpl. *) +(* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) +(* right. *) +(* apply ZExtra.mod_0_bounds; try lia. *) +(* apply ZLib.Z_mod_mult'. *) +(* rewrite Z2Nat.id in H11; try lia. *) +(* apply Zmult_lt_compat_r with (p := 4) in H11; try lia. *) +(* rewrite ZLib.div_mul_undo in H11; try lia. *) +(* split; try lia. *) +(* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) +(* } *) + +(* rewrite <- EXPR_OK. *) +(* rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *) +(* destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *) +(* apply Z.mul_cancel_r with (p := 4) in e; try lia. *) +(* rewrite ZLib.div_mul_undo in e; try lia. *) +(* rewrite combine_lookup_first. *) +(* eapply H7; eauto. *) + +(* rewrite <- array_set_len. *) +(* unfold arr_repeat. crush. *) +(* rewrite list_repeat_len. auto. *) +(* rewrite array_gso. *) +(* unfold array_get_error. *) +(* unfold arr_repeat. *) +(* crush. *) +(* apply list_repeat_lookup. *) +(* lia. *) +(* unfold_constants. *) +(* intro. *) +(* apply Z2Nat.inj_iff in H8; try lia. *) +(* apply Z.div_pos; try lia. *) +(* apply Integers.Ptrofs.unsigned_range. *) + +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* unfold arr_stack_based_pointers. *) +(* intros. *) +(* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + +(* crush. *) +(* erewrite Mem.load_store_same. *) +(* 2: { rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite e. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* exact H1. *) +(* apply Integers.Ptrofs.unsigned_range_2. } *) +(* crush. *) +(* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *) +(* destruct (Archi.ptr64); try discriminate. *) +(* pose proof (RSBP src). rewrite EQ_SRC in H0. *) +(* assumption. *) + +(* simpl. *) +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr. *) +(* simpl. *) +(* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) +(* right. *) +(* apply ZExtra.mod_0_bounds; try lia. *) +(* apply ZLib.Z_mod_mult'. *) +(* invert H0. *) +(* apply Zmult_lt_compat_r with (p := 4) in H9; try lia. *) +(* rewrite ZLib.div_mul_undo in H9; try lia. *) +(* split; try lia. *) +(* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) +(* } *) +(* apply ASBP; assumption. *) + +(* unfold stack_bounds in *. intros. *) +(* simpl. *) +(* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) +(* erewrite Mem.load_store_other with (m1 := m). *) +(* 2: { exact H1. } *) +(* 2: { right. right. simpl. *) +(* rewrite ZERO. *) +(* rewrite Integers.Ptrofs.add_zero_l. *) +(* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) +(* apply ZExtra.mod_0_bounds; crush; try lia. } *) +(* crush. *) +(* exploit (BOUNDS ptr); try lia. intros. crush. *) +(* exploit (BOUNDS ptr v); try lia. intros. *) +(* invert H0. *) +(* match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *) +(* assert (Mem.valid_access m AST.Mint32 sp' *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) +(* (Integers.Ptrofs.repr ptr))) Writable). *) +(* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) +(* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) +(* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) +(* (Integers.Ptrofs.unsigned *) +(* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) +(* (Integers.Ptrofs.repr ptr))) v). *) +(* apply X in H0. invert H0. congruence.*) *) +(* Admitted. *) +(* Hint Resolve transl_istore_correct : htlproof. *) + +(* Lemma transl_icond_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) +(* (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) *) +(* (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> *) +(* Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> *) +(* pc' = (if b then ifso else ifnot) -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f sp pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) +(* Proof. *) +(* intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. *) +(* inv_state. *) + +(* eexists. split. apply Smallstep.plus_one. *) +(* eapply HTL.step_module; eauto. *) +(* inv CONST; assumption. *) +(* inv CONST; assumption. *) +(* (* eapply Verilog.stmnt_runp_Vnonblock_reg with *) +(* (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). *) +(* constructor. *) + +(* simpl. *) +(* destruct b. *) +(* eapply Verilog.erun_Vternary_true. *) +(* eapply eval_cond_correct; eauto. *) +(* constructor. *) +(* apply boolToValue_ValueToBool. *) +(* eapply Verilog.erun_Vternary_false. *) +(* eapply eval_cond_correct; eauto. *) +(* constructor. *) +(* apply boolToValue_ValueToBool. *) +(* constructor. *) + +(* big_tac. *) + +(* invert MARR. *) +(* destruct b; rewrite assumption_32bit; big_tac. *) + +(* Unshelve. *) +(* constructor. *) +(* Qed.*) *) +(* Admitted. *) +(* Hint Resolve transl_icond_correct : htlproof. *) + +(* Lemma transl_ijumptable_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) +(* (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) *) +(* (n : Integers.Int.int) (pc' : RTL.node), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> *) +(* Registers.Regmap.get arg rs = Values.Vint n -> *) +(* list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f sp pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) +(* Proof. *) +(* intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. *) +(* Admitted. *) +(* Hint Resolve transl_ijumptable_correct : htlproof. *) + +(* Lemma transl_ireturn_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) *) +(* (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) *) +(* (m' : mem), *) +(* (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> *) +(* Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) +(* match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. *) +(* Proof. *) +(* intros s f stk pc rs m or m' H H0 R1 MSTATE. *) +(* inv_state. *) + +(* - econstructor. split. *) +(* eapply Smallstep.plus_two. *) + +(* eapply HTL.step_module; eauto. *) +(* inv CONST; assumption. *) +(* inv CONST; assumption. *) +(* constructor. *) +(* econstructor; simpl; trivial. *) +(* econstructor; simpl; trivial. *) +(* constructor. *) +(* econstructor; simpl; trivial. *) +(* constructor. *) + +(* constructor. constructor. *) + +(* unfold state_st_wf in WF; big_tac; eauto. *) +(* destruct wf as [HCTRL HDATA]. apply HCTRL. *) +(* apply AssocMapExt.elements_iff. eexists. *) +(* match goal with H: control ! pc = Some _ |- _ => apply H end. *) + +(* apply HTL.step_finish. *) +(* unfold Verilog.merge_regs. *) +(* unfold_merge; simpl. *) +(* rewrite AssocMap.gso. *) +(* apply AssocMap.gss. lia. *) +(* apply AssocMap.gss. *) +(* rewrite Events.E0_left. reflexivity. *) + +(* constructor; auto. *) +(* constructor. *) + +(* (* FIXME: Duplication *) *) +(* - econstructor. split. *) +(* eapply Smallstep.plus_two. *) +(* eapply HTL.step_module; eauto. *) +(* inv CONST; assumption. *) +(* inv CONST; assumption. *) +(* constructor. *) +(* econstructor; simpl; trivial. *) +(* econstructor; simpl; trivial. *) +(* constructor. constructor. constructor. *) +(* constructor. constructor. constructor. *) + +(* unfold state_st_wf in WF; big_tac; eauto. *) + +(* destruct wf as [HCTRL HDATA]. apply HCTRL. *) +(* apply AssocMapExt.elements_iff. eexists. *) +(* match goal with H: control ! pc = Some _ |- _ => apply H end. *) + +(* apply HTL.step_finish. *) +(* unfold Verilog.merge_regs. *) +(* unfold_merge. *) +(* rewrite AssocMap.gso. *) +(* apply AssocMap.gss. simpl; lia. *) +(* apply AssocMap.gss. *) +(* rewrite Events.E0_left. trivial. *) + +(* constructor; auto. *) + +(* simpl. inversion MASSOC. subst. *) +(* unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. *) +(* apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. *) +(* assert (HPle : Ple r (RTL.max_reg_function f)). *) +(* eapply RTL.max_reg_function_use. eassumption. simpl; auto. *) +(* apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) + +(* Unshelve. *) +(* all: constructor. *) +(* Qed. *) +(* Hint Resolve transl_ireturn_correct : htlproof. *) + +(* Lemma transl_callstate_correct: *) +(* forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) *) +(* (m : mem) (m' : Mem.mem') (stk : Values.block), *) +(* Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> *) +(* forall R1 : HTL.state, *) +(* match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) +(* match_states *) +(* (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) *) +(* (RTL.init_regs args (RTL.fn_params f)) m') R2. *) +(* Proof. *) +(* intros s f args m m' stk H R1 MSTATE. *) + +(* inversion MSTATE; subst. inversion TF; subst. *) +(* econstructor. split. apply Smallstep.plus_one. *) +(* eapply HTL.step_call. crush. *) + +(* apply match_state with (sp' := stk); eauto. *) + +(* all: big_tac. *) + +(* apply regs_lessdef_add_greater. unfold Plt; lia. *) +(* apply regs_lessdef_add_greater. unfold Plt; lia. *) +(* apply regs_lessdef_add_greater. unfold Plt; lia. *) +(* apply init_reg_assoc_empty. *) + +(* constructor. *) + +(* destruct (Mem.load AST.Mint32 m' stk *) +(* (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *) +(* Integers.Ptrofs.zero *) +(* (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *) +(* pose proof Mem.load_alloc_same as LOAD_ALLOC. *) +(* pose proof H as ALLOC. *) +(* eapply LOAD_ALLOC in ALLOC. *) +(* 2: { exact LOAD. } *) +(* ptrofs. rewrite LOAD. *) +(* rewrite ALLOC. *) +(* repeat constructor. *) + +(* ptrofs. rewrite LOAD. *) +(* repeat constructor. *) + +(* unfold reg_stack_based_pointers. intros. *) +(* unfold RTL.init_regs; crush. *) +(* destruct (RTL.fn_params f); *) +(* rewrite Registers.Regmap.gi; constructor. *) + +(* unfold arr_stack_based_pointers. intros. *) +(* crush. *) +(* destruct (Mem.load AST.Mint32 m' stk *) +(* (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *) +(* Integers.Ptrofs.zero *) +(* (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *) +(* pose proof Mem.load_alloc_same as LOAD_ALLOC. *) +(* pose proof H as ALLOC. *) +(* eapply LOAD_ALLOC in ALLOC. *) +(* 2: { exact LOAD. } *) +(* rewrite ALLOC. *) +(* repeat constructor. *) +(* constructor. *) + +(* Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) *) +(* Transparent Mem.load. *) +(* Transparent Mem.store. *) +(* unfold stack_bounds. *) +(* split. *) + +(* unfold Mem.alloc in H. *) +(* invert H. *) +(* crush. *) +(* unfold Mem.load. *) +(* intros. *) +(* match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *) +(* invert v0. unfold Mem.range_perm in H4. *) +(* unfold Mem.perm in H4. crush. *) +(* unfold Mem.perm_order' in H4. *) +(* small_tac. *) +(* exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *) +(* rewrite Maps.PMap.gss in H8. *) +(* match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *) +(* crush. *) +(* apply proj_sumbool_true in H10. lia. *) + +(* unfold Mem.alloc in H. *) +(* invert H. *) +(* crush. *) +(* unfold Mem.store. *) +(* intros. *) +(* match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *) +(* invert v0. unfold Mem.range_perm in H4. *) +(* unfold Mem.perm in H4. crush. *) +(* unfold Mem.perm_order' in H4. *) +(* small_tac. *) +(* exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *) +(* rewrite Maps.PMap.gss in H8. *) +(* match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *) +(* crush. *) +(* apply proj_sumbool_true in H10. lia. *) +(* constructor. simplify. rewrite AssocMap.gss. *) +(* simplify. rewrite AssocMap.gso. apply AssocMap.gss. simplify. lia. *) +(* Opaque Mem.alloc. *) +(* Opaque Mem.load. *) +(* Opaque Mem.store. *) +(* Qed. *) +(* Hint Resolve transl_callstate_correct : htlproof. *) + +(* Lemma transl_returnstate_correct: *) +(* forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) *) +(* (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) *) +(* (R1 : HTL.state), *) +(* match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> *) +(* exists R2 : HTL.state, *) +(* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *) +(* match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. *) +(* Proof. *) +(* intros res0 f sp pc rs s vres m R1 MSTATE. *) +(* inversion MSTATE. inversion MF. *) +(* Qed. *) +(* Hint Resolve transl_returnstate_correct : htlproof. *) + +(* 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 (RTL.semantics prog), *) +(* Smallstep.initial_state (RTL.semantics prog) s1 -> *) +(* exists s2 : Smallstep.state (HTL.semantics tprog), *) +(* Smallstep.initial_state (HTL.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. *) +(* apply transl_module_correct. *) +(* assert (Some (AST.Internal x) = Some (AST.Internal m)). *) +(* replace (AST.fundef HTL.module) with (HTL.fundef). *) +(* rewrite <- H6. setoid_rewrite <- A. trivial. *) +(* trivial. inv H7. assumption. *) +(* Qed. *) +(* Hint Resolve transl_initial_states : htlproof. *) + +(* Lemma transl_final_states : *) +(* forall (s1 : Smallstep.state (RTL.semantics prog)) *) +(* (s2 : Smallstep.state (HTL.semantics tprog)) *) +(* (r : Integers.Int.int), *) +(* match_states s1 s2 -> *) +(* Smallstep.final_state (RTL.semantics prog) s1 r -> *) +(* Smallstep.final_state (HTL.semantics tprog) s2 r. *) +(* Proof. *) +(* intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. *) +(* Qed. *) +(* Hint Resolve transl_final_states : htlproof. *) + +(* Theorem transl_step_correct: *) +(* forall (S1 : RTL.state) t S2, *) +(* RTL.step ge S1 t S2 -> *) +(* forall (R1 : HTL.state), *) +(* match_states S1 R1 -> *) +(* exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. *) +(* Proof. *) +(* induction 1; eauto with htlproof; (intros; inv_state). *) +(* Qed. *) +(* Hint Resolve transl_step_correct : htlproof. *) Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. - eapply Smallstep.forward_simulation_plus; eauto with htlproof. - apply senv_preserved. - Qed. + (* eapply Smallstep.forward_simulation_plus; eauto with htlproof. *) + (* apply senv_preserved. *) + (* Qed. *) + Admitted. End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 0cdecba..82b6da9 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -17,8 +17,9 @@ *) From compcert Require RTL Op Maps Errors. -From compcert Require Import Maps. -From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. +From compcert Require Import Maps Integers. +From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. +Require Import Lia. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. @@ -116,31 +117,40 @@ translations for each of the elements *) Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := | tr_instr_Inop : forall n, + Z.pos n <= Int.max_unsigned -> tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) | tr_instr_Iop : forall n op args dst s s' e i, + Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, + Z.pos n1 <= Int.max_unsigned -> + Z.pos n2 <= Int.max_unsigned -> translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) | tr_instr_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) - (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip + tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (Vlit (ZToValue 0%Z)))) Vskip | tr_instr_Ireturn_Some : forall r, tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip + (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : - forall mem addr args s s' i c dst n, - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) + forall chunk addr args s s' i e dst n, + Z.pos n <= Int.max_unsigned -> + chunk = AST.Mint32 -> + translate_arr_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iload chunk addr args dst n) + (create_single_cycle_load stk e dst) (state_goto st n) | tr_instr_Istore : - forall mem addr args s s' i c src n, - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n) + forall chunk addr args s s' i e src n, + Z.pos n <= Int.max_unsigned -> + chunk = AST.Mint32 -> + translate_arr_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Istore chunk addr args src n) + (create_single_cycle_store stk e src) (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> @@ -160,17 +170,24 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, - (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat f.(RTL.fn_stacksize) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + st = ((RTL.max_reg_function f) + 1)%positive -> + fin = ((RTL.max_reg_function f) + 2)%positive -> + rtrn = ((RTL.max_reg_function f) + 3)%positive -> + stk = ((RTL.max_reg_function f) + 4)%positive -> + start = ((RTL.max_reg_function f) + 5)%positive -> + rst = ((RTL.max_reg_function f) + 6)%positive -> + clk = ((RTL.max_reg_function f) + 7)%positive -> tr_module f m. Hint Constructors tr_module : htlspec. @@ -202,6 +219,13 @@ Lemma declare_reg_controllogic_trans : Proof. intros. monadInv H. trivial. Qed. Hint Resolve create_reg_controllogic_trans : htlspec. +Lemma declare_reg_freshreg_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. inversion 1; auto. Qed. +Hint Resolve declare_reg_freshreg_trans : htlspec. + Lemma create_arr_datapath_trans : forall sz ln s s' x i iop, create_arr iop sz ln s = OK x s' i -> @@ -268,6 +292,16 @@ Proof. - apply H in EQ. rewrite EQ. eauto. Qed. +Lemma collect_freshreg_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + Lemma collect_declare_controllogic_trans : forall io n l s s' i, HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> @@ -286,6 +320,153 @@ Proof. intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. Qed. +Lemma collect_declare_freshreg_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + inversion 1. auto. +Qed. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + +Lemma translate_eff_addressing_freshreg_trans : + forall op args s r s' i, + translate_eff_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + +Lemma translate_arr_addressing_freshreg_trans : + forall op args s r s' i, + translate_arr_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + +Lemma translate_comparison_freshreg_trans : + forall op args s r s' i, + translate_comparison op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_freshreg_trans : htlspec. + +Lemma translate_comparisonu_freshreg_trans : + forall op args s r s' i, + translate_comparisonu op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparisonu_freshreg_trans : htlspec. + +Lemma translate_comparison_imm_freshreg_trans : + forall op args s r s' i n, + translate_comparison_imm op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. + +Lemma translate_comparison_immu_freshreg_trans : + forall op args s r s' i n, + translate_comparison_immu op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. + +Lemma translate_condition_freshreg_trans : + forall op args s r s' i, + translate_condition op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_condition_freshreg_trans : htlspec. + +Lemma translate_instr_freshreg_trans : + forall op args s r s' i, + translate_instr op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. + monadInv H1. eauto with htlspec. +Qed. +Hint Resolve translate_instr_freshreg_trans : htlspec. + +Lemma add_instr_freshreg_trans : + forall n n' st s r s' i, + add_instr n n' st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_freshreg_trans : htlspec. + +Lemma add_branch_instr_freshreg_trans : + forall n n0 n1 e s r s' i, + add_branch_instr e n n0 n1 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_branch_instr_freshreg_trans : htlspec. + +Lemma add_node_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_node_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_node_skip_freshreg_trans : htlspec. + +Lemma add_instr_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_instr_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_skip_freshreg_trans : htlspec. + +Lemma transf_instr_freshreg_trans : + forall fin ret st instr s v s' i, + transf_instr fin ret st instr s = OK v s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. destruct instr eqn:?. subst. unfold transf_instr in H. + destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate. + monadInv H. apply add_instr_freshreg_trans in EQ2. + apply translate_arr_addressing_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - destruct (Z.pos n0 <=? Int.max_unsigned); try discriminate. + monadInv H. apply add_instr_freshreg_trans in EQ0. + apply translate_arr_addressing_freshreg_trans in EQ. congruence. + - monadInv H. apply translate_condition_freshreg_trans in EQ. + apply add_branch_instr_freshreg_trans in EQ0. + congruence. + - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. +Qed. +Hint Resolve transf_instr_freshreg_trans : htlspec. + +Lemma collect_trans_instr_freshreg_trans : + forall fin ret st l s s' i, + HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + eauto with htlspec. +Qed. + Ltac rewrite_states := match goal with | [ H: ?x ?s = ?x ?s' |- _ ] => @@ -294,20 +475,18 @@ Ltac rewrite_states := remember (?x ?s) as c1; remember (?x ?s') as c2; try subst end. -Ltac unfold_match H := - match type of H with - | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate - end. - Ltac inv_add_instr' H := match type of H with + | ?f _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ _ = OK _ _ _ => unfold f in H | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H end; repeat unfold_match H; inversion H. Ltac inv_add_instr := - lazymatch goal with + match goal with + | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr | H: context[add_instr_skip _ _ _] |- _ => inv_add_instr' H | H: context[add_instr_skip _ _] |- _ => @@ -343,28 +522,34 @@ Proof. destruct (peq pc pc1). - subst. destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. + try destruct_optional; try (destruct m; try discriminate); + inv_add_instr; econstructor; try assumption. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + apply Z.leb_le. assumption. eapply in_map with (f := fst) in H9. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + econstructor. apply Z.leb_le; assumption. + reflexivity. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct H2. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. + econstructor. apply Z.leb_le; assumption. + eauto with htlspec. eassumption. * apply in_map with (f := fst) in H2. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. @@ -372,6 +557,7 @@ Proof. + destruct H2. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. + econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN). eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. @@ -405,9 +591,17 @@ Qed. Hint Resolve iter_expand_instr_spec : htlspec. Lemma create_arr_inv : forall w x y z a b c d, - create_arr w x y z = OK (a, b) c d -> y = b. + create_arr w x y z = OK (a, b) c d -> + y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Proof. + inversion 1; split; auto. +Qed. + +Lemma create_reg_inv : forall a b s r s' i, + create_reg a b s = OK r s' i -> + r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). Proof. - inversion 1. reflexivity. + inversion 1; auto. Qed. Theorem transl_module_correct : @@ -429,21 +623,29 @@ Proof. crush; monadInv Heqr. - (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. - rewrite <- STK_LEN. + repeat unfold_match EQ9. monadInv EQ9. - econstructor; simpl; auto. - intros. + (* TODO: We should be able to fold this into the automation. *) + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. + pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. + pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL. + destruct x3. destruct x4. + pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR. + pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. + pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. + pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. + pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. + rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. + rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. inv_incr. + econstructor; simpl; auto; try lia. + intros. assert (EQ3D := EQ3). - destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. - assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. - assert (STD: st_datapath s10 = st_datapath s3) by congruence. - assert (STST: st_st s10 = st_st s3) by congruence. - rewrite STC. rewrite STD. rewrite STST. + replace (st_controllogic s10) with (st_controllogic s3) by congruence. + replace (st_datapath s10) with (st_datapath s3) by congruence. + replace (st_st s10) with (st_st s3) by congruence. eapply iter_expand_instr_spec; eauto with htlspec. apply PTree.elements_complete. Qed. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index b550ff9..f5d5fa7 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -19,35 +19,33 @@ From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST. -From coqup Require Import Verilog HTL Coquplib AssocMap Value. +From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt. -Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr * Verilog.stmnt) := - match st with - | (n, stmt) :: ls => (Vlit (posToValue 32 n), stmt) :: transl_list ls - | nil => nil - end. +Definition transl_list_fun (a : node * Verilog.stmnt) := + let (n, stmnt) := a in + (Vlit (posToValue n), stmnt). -Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := - match scldecl with - | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' - | nil => nil - end. +Definition transl_list st := map transl_list_fun st. -Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := - match arrdecl with - | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' - | nil => nil - end. +Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := + match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. + +Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. + +Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := + match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. + +Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in let body := - Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1)) - (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint))) + Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) - :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(mod_start) m.(mod_reset) diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index ca4ecab..5b467a7 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -16,9 +16,12 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import Smallstep Linking. +From compcert Require Import Smallstep Linking Integers Globalenvs. From coqup Require HTL. -From coqup Require Import Coquplib Veriloggen Verilog. +From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap. +Require Import Lia. + +Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. @@ -52,6 +55,176 @@ Inductive match_states : HTL.state -> state -> Prop := forall m, match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). +Lemma Vlit_inj : + forall a b, Vlit a = Vlit b -> a = b. +Proof. inversion 1. trivial. Qed. + +Lemma posToValue_inj : + forall a b, + 0 <= Z.pos a <= Int.max_unsigned -> + 0 <= Z.pos b <= Int.max_unsigned -> + posToValue a = posToValue b -> + a = b. +Proof. + intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. + rewrite <- Int.unsigned_repr at 1; try assumption. + symmetry. + rewrite <- Int.unsigned_repr at 1; try assumption. + unfold posToValue in *. rewrite H1; auto. +Qed. + +Lemma valueToPos_inj : + forall a b, + 0 < Int.unsigned a -> + 0 < Int.unsigned b -> + valueToPos a = valueToPos b -> + a = b. +Proof. + intros. unfold valueToPos in *. + rewrite <- Int.repr_unsigned at 1. + rewrite <- Int.repr_unsigned. + apply Pos2Z.inj_iff in H1. + rewrite Z2Pos.id in H1; auto. + rewrite Z2Pos.id in H1; auto. + rewrite H1. auto. +Qed. + +Lemma unsigned_posToValue_le : + forall p, + Z.pos p <= Int.max_unsigned -> + 0 < Int.unsigned (posToValue p). +Proof. + intros. unfold posToValue. rewrite Int.unsigned_repr; lia. +Qed. + +Lemma transl_list_fun_fst : + forall p1 p2 a b, + 0 <= Z.pos p1 <= Int.max_unsigned -> + 0 <= Z.pos p2 <= Int.max_unsigned -> + transl_list_fun (p1, a) = transl_list_fun (p2, b) -> + (p1, a) = (p2, b). +Proof. + intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1. + destruct H1. rewrite H2. apply Vlit_inj in H1. + apply posToValue_inj in H1; try assumption. + rewrite H1; auto. +Qed. + +Lemma Zle_relax : + forall p q r, + p < q <= r -> + p <= q <= r. +Proof. lia. Qed. +Hint Resolve Zle_relax : verilogproof. + +Lemma transl_in : + forall l p, + 0 <= Z.pos p <= Int.max_unsigned -> + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> + In p (map fst l). +Proof. + induction l. + - simplify. auto. + - intros. destruct a. simplify. destruct (peq p0 p); auto. + right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. + auto with verilogproof. + apply IHl; auto. +Qed. + +Lemma transl_notin : + forall l p, + 0 <= Z.pos p <= Int.max_unsigned -> + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)). +Proof. + induction l; auto. intros. destruct a. unfold not in *. intros. + simplify. + destruct (peq p0 p). apply H1. auto. apply H1. + unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. + contradiction. + auto with verilogproof. auto. + right. apply transl_in; auto. +Qed. + +Lemma transl_norepet : + forall l, + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)). +Proof. + induction l. + - intros. simpl. apply list_norepet_nil. + - destruct a. intros. simpl. apply list_norepet_cons. + inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. + intros. apply H. destruct (peq p0 p); subst; simplify; auto. + assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. + simplify. inv H0. assumption. +Qed. + +Lemma transl_list_correct : + forall l v ev f asr asa asrn asan asr' asa' asrn' asan', + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + list_norepet (List.map fst l) -> + asr!ev = Some v -> + (forall p s, + In (p, s) l -> + v = posToValue p -> + stmnt_runp f + {| assoc_blocking := asr; assoc_nonblocking := asrn |} + {| assoc_blocking := asa; assoc_nonblocking := asan |} + s + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> + stmnt_runp f + {| assoc_blocking := asr; assoc_nonblocking := asrn |} + {| assoc_blocking := asa; assoc_nonblocking := asan |} + (Vcase (Vvar ev) (transl_list l) (Some Vskip)) + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). +Proof. + induction l as [| a l IHl]. + - contradiction. + - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. + destruct a as [p' s']. simplify. + destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. + constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. + rewrite ASSOC. trivial. constructor. auto. + inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. + inv NOREP. eapply in_map with (f := fst) in INV. contradiction. + + eapply stmnt_runp_Vcase_nomatch. constructor. simplify. + unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. + trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. + apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. + eapply in_map with (f := fst) in H0. auto. + apply Zle_relax. apply BOUND; auto. auto. + + eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. + trivial. assumption. +Qed. +Hint Resolve transl_list_correct : verilogproof. + +Lemma pc_wf : + forall A m p v, + (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + m!p = Some v -> + 0 <= Z.pos p <= Int.max_unsigned. +Proof. + intros A m p v LT S. apply Zle_relax. apply LT. + apply AssocMap.elements_correct in S. remember (p, v) as x. + exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. +Qed. + +Lemma mis_stepp_decl : + forall l asr asa f, + mis_stepp f asr asa (map Vdeclaration l) asr asa. +Proof. + induction l. + - intros. constructor. + - intros. simplify. econstructor. constructor. auto. +Qed. +Hint Resolve mis_stepp_decl : verilogproof. + Section CORRECTNESS. Variable prog: HTL.program. @@ -62,6 +235,40 @@ Section CORRECTNESS. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : 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. + Hint Resolve symbols_preserved : verilogproof. + + Lemma function_ptr_translated: + forall (b: Values.block) (f: HTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. + Proof. + intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + Hint Resolve function_ptr_translated : verilogproof. + + Lemma functions_translated: + forall (v: Values.val) (f: HTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. + Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + Hint Resolve functions_translated : verilogproof. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof. + intros. eapply (Genv.senv_match TRANSL). + Qed. + Hint Resolve senv_preserved : verilogproof. + Theorem transl_step_correct : forall (S1 : HTL.state) t S2, HTL.step ge S1 t S2 -> @@ -69,15 +276,93 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. Proof. -(* induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. - - apply Smallstep.plus_one. econstructor. eassumption. trivial. - * econstructor. econstructor.*) - Admitted. + induction 1; intros R1 MSTATE; inv MSTATE. + - econstructor; split. apply Smallstep.plus_one. econstructor. + assumption. assumption. eassumption. apply valueToPos_posToValue. + split. lia. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. + simpl. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite H. trivial. + + econstructor. simpl. auto. auto. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + econstructor. econstructor. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. + rewrite valueToPos_posToValue. constructor; assumption. lia. + + - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. + constructor; assumption. + - econstructor; split. apply Smallstep.plus_one. constructor. + + constructor. constructor. + - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. + + apply match_state. assumption. + Qed. + Hint Resolve transl_step_correct : verilogproof. + + Lemma transl_initial_states : + forall s1 : Smallstep.state (HTL.semantics prog), + Smallstep.initial_state (HTL.semantics prog) s1 -> + exists s2 : Smallstep.state (Verilog.semantics tprog), + Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. + Proof. + induction 1. + econstructor; split. econstructor. + apply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. + replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. + symmetry; eapply Linking.match_program_main; eauto. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + inv B. eauto. + constructor. + Qed. + Hint Resolve transl_initial_states : verilogproof. + + Lemma transl_final_states : + forall (s1 : Smallstep.state (HTL.semantics prog)) + (s2 : Smallstep.state (Verilog.semantics tprog)) + (r : Integers.Int.int), + match_states s1 s2 -> + Smallstep.final_state (HTL.semantics prog) s1 r -> + Smallstep.final_state (Verilog.semantics tprog) s2 r. + Proof. + intros. inv H0. inv H. inv H3. constructor. reflexivity. + Qed. + Hint Resolve transl_final_states : verilogproof. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). - Admitted. - + Proof. + eapply Smallstep.forward_simulation_plus; eauto with verilogproof. + apply senv_preserved. + Qed. End CORRECTNESS. - diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v deleted file mode 100644 index 7dc632c..0000000 --- a/src/translation/Veriloggenspec.v +++ /dev/null @@ -1,17 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2020 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/>. - *) |