diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compiler.v | 19 | ||||
| -rw-r--r-- | src/CoqupClflags.ml | 2 | ||||
| -rw-r--r-- | src/Simulator.v | 6 | ||||
| -rw-r--r-- | src/common/Coquplib.v | 6 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 38 | ||||
| -rw-r--r-- | src/common/Maps.v | 2 | ||||
| -rw-r--r-- | src/common/Monad.v | 4 | ||||
| -rw-r--r-- | src/common/Show.v | 2 | ||||
| -rw-r--r-- | src/common/Statemonad.v | 2 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 8 | ||||
| -rw-r--r-- | src/translation/HTLgen.v | 116 | ||||
| -rw-r--r-- | src/translation/HTLgenproof.v | 4052 | ||||
| -rw-r--r-- | src/translation/HTLgenspec.v | 58 | ||||
| -rw-r--r-- | src/translation/Veriloggen.v | 4 | ||||
| -rw-r--r-- | src/translation/Veriloggenproof.v | 6 | ||||
| -rw-r--r-- | src/verilog/Array.v | 2 | ||||
| -rw-r--r-- | src/verilog/AssocMap.v | 4 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 6 | ||||
| -rw-r--r-- | src/verilog/PrintHTL.ml | 6 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 29 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.mli | 6 | ||||
| -rw-r--r-- | src/verilog/Value.v | 4 | ||||
| -rw-r--r-- | src/verilog/ValueInt.v | 5 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 90 |
24 files changed, 2284 insertions, 2193 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 8820f14..7b17336 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Import HTLgenproof. +From vericert Require Import HTLgenproof. From compcert.common Require Import Errors @@ -47,7 +47,7 @@ From compcert.cfrontend Require From compcert.driver Require Compiler. -From coqup Require +From vericert Require Verilog Veriloggen Veriloggenproof @@ -82,19 +82,14 @@ Qed. Definition transf_backend (r : RTL.program) : res Verilog.program := OK r - @@ Tailcall.transf_program @@@ Inlining.transf_program - @@ Renumber.transf_program - (* @@ Constprop.transf_program *) - @@ Renumber.transf_program - @@@ CSE.transf_program - @@@ Deadcode.transf_program - @@@ Unusedglob.transform_program @@ print (print_RTL 1) @@@ HTLgen.transl_program @@ print print_HTL @@ Veriloggen.transl_program. +Check mkpass. + Definition transf_hls (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@ -151,8 +146,8 @@ Proof. exists p7; split. apply Inliningproof.transf_program_match; auto. exists p8; split. apply HTLgenproof.transf_program_match; auto. exists p9; split. apply Veriloggenproof.transf_program_match; auto. - (* inv T. reflexivity. *) -Admitted. + inv T. reflexivity. +Qed. Remark forward_simulation_identity: forall sem, forward_simulation sem sem. diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml index 5b40ce6..ca591de 100644 --- a/src/CoqupClflags.ml +++ b/src/CoqupClflags.ml @@ -1,4 +1,4 @@ -(* Coqup flags *) +(* Vericert flags *) let option_simulate = ref false let option_hls = ref true let option_debug_hls = ref false diff --git a/src/Simulator.v b/src/Simulator.v index 83d3e96..3df0c7f 100644 --- a/src/Simulator.v +++ b/src/Simulator.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -20,8 +20,8 @@ From compcert Require Import Errors. -From coqup Require Compiler Verilog Value. -From coqup Require Import Coquplib. +From vericert Require Compiler Verilog Value. +From vericert Require Import Vericertlib. Local Open Scope error_monad_scope. diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 469eddc..d9176db 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -25,7 +25,7 @@ From Coq Require Export Require Import Lia. -From coqup Require Import Show. +From vericert Require Import Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) @@ -235,5 +235,3 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := let unused := debug_print (s ++ show a) in b. - -Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 8e32c2c..c9b5dbd 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -5,7 +5,7 @@ Require Import ZBinary. From bbv Require Import ZLib. From compcert Require Import Integers Coqlib. -Require Import Coquplib. +Require Import Vericertlib. Local Open Scope Z_scope. @@ -298,48 +298,44 @@ Module IntExtra. (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize)) (repr (Byte.unsigned d)))). - Definition byte0 (n: int) : byte := Byte.repr $ unsigned n. - Definition ibyte0 (n: int) : int := Int.repr $ Byte.unsigned $ byte0 n. + Definition byte1 (n: int) : byte := Byte.repr (unsigned n). - Definition byte1 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr Byte.zwordsize. - Definition ibyte1 (n: int) : int := Int.repr $ Byte.unsigned $ byte1 n. + Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))). - Definition byte2 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (2 * Byte.zwordsize). - Definition ibyte2 (n: int) : int := Int.repr $ Byte.unsigned $ byte2 n. + Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))). - Definition byte3 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (3 * Byte.zwordsize). - Definition ibyte3 (n: int) : int := Int.repr $ Byte.unsigned $ byte3 n. + Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))). - Lemma bits_byte0: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte0 n) i = testbit n i. + Lemma bits_byte1: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i. Proof. - intros. unfold byte0. rewrite Byte.testbit_repr; auto. + intros. unfold byte1. rewrite Byte.testbit_repr; auto. Qed. - Lemma bits_byte1: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n (i + Byte.zwordsize). + Lemma bits_byte2: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize). Proof. - intros. unfold byte1. rewrite Byte.testbit_repr; auto. + intros. unfold byte2. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. apply zlt_true. omega. omega. Qed. - Lemma bits_byte2: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + (2 * Byte.zwordsize)). + Lemma bits_byte3: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)). Proof. - intros. unfold byte2. rewrite Byte.testbit_repr; auto. + intros. unfold byte3. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). apply zlt_true. omega. omega. Qed. - Lemma bits_byte3: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (3 * Byte.zwordsize)). + Lemma bits_byte4: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)). Proof. - intros. unfold byte3. rewrite Byte.testbit_repr; auto. + intros. unfold byte4. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). diff --git a/src/common/Maps.v b/src/common/Maps.v index 3236417..b5a2fb2 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -1,4 +1,4 @@ -From coqup Require Import Coquplib. +From vericert Require Import Vericertlib. From compcert Require Export Maps. From compcert Require Import Errors. diff --git a/src/common/Monad.v b/src/common/Monad.v index 628963e..8517186 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -20,10 +20,6 @@ Module MonadExtra(M : Monad). Module MonadNotation. - Notation "A ; B" := - (bind A (fun _ => B)) - (at level 200, B at level 200). - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/common/Show.v b/src/common/Show.v index c994df3..4c66725 100644 --- a/src/common/Show.v +++ b/src/common/Show.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index ed1b9e7..2eada2f 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -1,5 +1,5 @@ From compcert Require Errors. -From coqup Require Import Monad. +From vericert Require Import Monad. From Coq Require Import Lists.List. Module Type State. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 5d10cd7..b1a885e 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Verilog ValueInt Compiler. +From vericert Require Verilog Value Compiler. From Coq Require DecidableClass. @@ -134,7 +134,7 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". Extract Constant Compiler.time => "Timing.time_coq". -Extract Constant Coquplib.debug_print => "print_newline". +Extract Constant Vericertlib.debug_print => "print_newline". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) @@ -167,7 +167,7 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction - Verilog.module ValueInt.uvalueToZ coqup.Compiler.transf_hls + Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 1869a8f..8245a06 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -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 ValueInt Statemonad. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. @@ -311,16 +311,26 @@ 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 => - ret (boplitz Vadd r1 off) + if (check_address_parameter_signed off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") | Op.Ascaled scale offset, r1::nil => - ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") | Op.Aindexed2 offset, r1::r2::nil => - ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + if (check_address_parameter_signed offset) + then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in - ret (Vlit (ZToValue a)) + if (check_address_parameter_unsigned a) + then ret (Vlit (ZToValue a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. @@ -402,38 +412,26 @@ 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 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 *) +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 - ret (Vlit (ZToValue a)) - | _, _ => error (Errors.msg "Veriloggen: translate_arr_addressing unsuported addressing") + 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. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := @@ -448,16 +446,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := 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) => @@ -472,25 +460,17 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni 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 + | Iload mem addr args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do src <- translate_arr_access mem addr args stack; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst src) + else error (Errors.msg "State is larger than 2^32.") + | Istore mem addr args src n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + 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. *) + else error (Errors.msg "State is larger than 2^32.") | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") @@ -596,7 +576,7 @@ 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 8 (Z.to_nat f.(fn_stacksize)); + 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; diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 943b76e..ddf8c3a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -18,8 +18,8 @@ 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. +From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. +From vericert Require HTL Verilog. Require Import Lia. @@ -342,1944 +342,2122 @@ 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. -(* 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. *) + 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) + | H: match _ with _ => _ end = OK _ _ _ |- _ => 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 + | H : context[bop] |- _ => unfold bop in H + | |- context[boplit] => unfold boplit + | H : context[boplit] |- _ => unfold boplit in H + | |- context[boplitz] => unfold boplitz + | H : context[boplitz] |- _ => unfold boplitz in H + | |- val_value_lessdef Values.Vundef _ => solve [constructor] + | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H + | |- val_value_lessdef (Values.Vint _) _ => constructor; auto + | H : ret _ _ = OK _ _ _ |- _ => inv H + | H : context[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 + | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H + | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H + | |- 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 + | H : ?b = _ |- _ = boolToValue ?b => rewrite H + end. + Ltac inv_lessdef := lazymatch goal with + | H2 : context[RTL.max_reg_function ?f], H : Registers.Regmap.get ?r ?rs = _, + H1 : Registers.Regmap.get ?r0 ?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 H2 in HPle1; inv HPle1; + let HPle2 := fresh "HPle" in + assert (HPle2 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H2 in HPle2; inv HPle2 + | H2 : context[RTL.max_reg_function ?f], H : 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 H2 in HPle1; inv HPle1 + end. + Ltac solve_cond := + match goal with + | H : context[match _ with _ => _ end] |- _ => repeat (unfold_merge H) + | H : ?f = _ |- context[boolToValue ?f] => rewrite H; solve [auto] + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ => + rewrite H2 in H; discriminate + | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ => + rewrite H2 in H; discriminate + | |- context[val_value_lessdef Values.Vundef _] => + econstructor; split; econstructor; econstructor; auto; solve [constructor] + | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, + H2 : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H3 : Registers.Regmap.get ?r0 ?rs = Values.Vint _, + H4 : Values.Vint _ = Registers.Regmap.get ?r0 ?rs|- _ => + rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor + | H1 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _, + H2 : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H3 : Registers.Regmap.get ?r0 ?rs = Values.Vptr _ _, + H4 : Values.Vptr _ _ = Registers.Regmap.get ?r0 ?rs|- _ => + rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor; + unfold Ptrofs.ltu, Int.ltu in *; unfold Ptrofs.of_int in *; + repeat (rewrite Ptrofs.unsigned_repr in *; auto using Int.unsigned_range_2) + | H : _ :: _ = _ :: _ |- _ => inv H + | H : ret _ _ = OK _ _ _ |- _ => inv H + | |- _ => + eexists; split; [ econstructor; econstructor; auto + | simplify; inv_lessdef; repeat (unfold valueToPtr, valueToInt in *; solve_cond); + unfold valueToPtr in * + ] + 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. + - 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. + (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, + Search Int.repr. + repeat (rewrite Int.unsigned_repr). auto.*) + - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). + destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac. + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. rewrite H2 in H0. inv H0. unfold valueToPtr. unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + * inv Heqv. unfold valueToInt in *. inv H2. inv H0. unfold valueToInt in *. trivial. + * constructor. unfold valueToPtr, ZToValue in *. + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. inv Heqv. rewrite Int.add_commut. + apply AGR. auto. inv H1. inv H0. unfold valueToPtr. unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr. inv H0. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + apply Int.unsigned_range_2. + * constructor. unfold valueToPtr, ZToValue in *. + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. inv Heqv. + apply AGR. auto. inv H0. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + inv H1. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. apply Int.unsigned_range_2. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). inv Heqv. inv H3. + unfold valueToInt, ZToValue. auto. + * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). + * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). + * constructor. unfold valueToPtr, ZToValue. unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + unfold valueToPtr, ZToValue. + repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1. + inv Heqv1. inv Heqv0. unfold valueToInt in *. + assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H2. inv H2. auto. + rewrite Heqv2 in H2. inv H2. + rewrite Heqv2 in H3. discriminate. + repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1. + repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1. + constructor. unfold valueToPtr, ZToValue. inv Heqv0. inv Heqv1. + assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H3. inv H3. + + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. inv H2. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. apply Int.unsigned_range_2. + apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. apply Int.unsigned_range_2. + + rewrite Heqv2 in H3. inv H3. + + rewrite Heqv2 in H4. inv H4. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + eexists. split. constructor. + constructor. unfold valueToPtr, ZToValue. rewrite Ptrofs.add_zero_l. unfold Ptrofs.of_int. + rewrite Int.unsigned_repr. symmetry. apply Ptrofs.repr_unsigned. + unfold check_address_parameter_unsigned in *. apply Ptrofs.unsigned_range_2. + - unfold translate_condition in *; repeat unfold_match H1; + unfold translate_comparison in *; repeat unfold_match H1; inv H1; + unfold translate_comparisonu, translate_comparison_imm, translate_comparison_immu in *; + unfold Op.eval_condition, Values.Val.of_optbool, Values.Val.cmp_bool, Values.Val.cmpu_bool, bop in *; + simplify; + repeat (match goal with |- context[match ?d with _ => _ end] => destruct d eqn:? end; + match goal with H : context[match ?d with _ => _ end] |- _ => repeat unfold_match H end); + try (match goal with |- context[if ?d then _ else _] => destruct d eqn:? end); + simplify; repeat solve_cond; + try (match goal with H : ?f = _ |- context[boolToValue ?f] => rewrite H; solve [auto] end); + try (match goal with H : context[match ?d with _ => _ end] |- _ => repeat unfold_match H end); + simplify; repeat solve_cond. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + + rewrite H3 in H0. inv H0. constructor. unfold valueToInt, intToValue in *. rewrite H1. auto. + - admit. (* select *) + Admitted. + + Lemma eval_cond_correct : + exists v' : value, + Verilog.expr_runp f' asr asa e v' /\ + val_value_lessdef + (Values.Val.of_optbool + (Op.eval_condition cond + (map (fun r : positive => Registers.Regmap.get r rs) args) m)) v' + 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. exact tt. + 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. exact tt. + 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. *) - Admitted. + eapply Smallstep.forward_simulation_plus; eauto with htlproof. + apply senv_preserved. + Qed. End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 82b6da9..93d5612 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -18,7 +18,7 @@ From compcert Require RTL Op Maps Errors. From compcert Require Import Maps Integers. -From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap. +From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap. Require Import Lia. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. @@ -138,19 +138,16 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : - forall chunk addr args s s' i e dst n, + forall mem addr args s s' i c 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) + 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) | tr_instr_Istore : - forall chunk addr args s s' i e src n, + forall mem addr args s s' i c 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) + 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) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> @@ -178,7 +175,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := 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) -> + 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 -> st = ((RTL.max_reg_function f) + 1)%positive -> @@ -343,15 +340,6 @@ Proof. 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 -> @@ -407,6 +395,15 @@ Proof. Qed. Hint Resolve translate_instr_freshreg_trans : htlspec. +Lemma translate_arr_access_freshreg_trans : + forall mem addr args st s r s' i, + translate_arr_access mem addr args st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_arr_access_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 -> @@ -444,15 +441,10 @@ Proof. 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. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_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. + - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_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. @@ -522,8 +514,7 @@ Proof. destruct (peq pc pc1). - subst. destruct instr1 eqn:?; try discriminate; - try destruct_optional; try (destruct m; try discriminate); - inv_add_instr; econstructor; try assumption. + try destruct_optional; 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. @@ -540,7 +531,6 @@ Proof. + 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 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. @@ -549,7 +539,7 @@ Proof. * inversion H2. replace (st_st s2) with (st_st s0) by congruence. econstructor. apply Z.leb_le; assumption. - eauto with htlspec. eassumption. + eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f5d5fa7..a0be0fa 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -19,7 +19,7 @@ From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST. -From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. Definition transl_list_fun (a : node * Verilog.stmnt) := let (n, stmnt) := a in diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 5b467a7..9abbd4b 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -17,8 +17,8 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. -From coqup Require HTL. -From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap. +From vericert Require HTL. +From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. Local Open Scope assocmap. diff --git a/src/verilog/Array.v b/src/verilog/Array.v index be06541..02b6d33 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -1,7 +1,7 @@ Set Implicit Arguments. Require Import Lia. -Require Import Coquplib. +Require Import Vericertlib. From Coq Require Import Lists.List Datatypes. Import ListNotations. diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index c5cfa3f..8d8788a 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Import Coquplib ValueInt. +From vericert Require Import Vericertlib ValueInt. From compcert Require Import Maps. Definition reg := positive. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index b3d1442..620ef14 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -17,8 +17,8 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib ValueInt AssocMap Array. -From coqup Require Verilog. +From vericert Require Import Vericertlib ValueInt AssocMap Array. +From vericert Require Verilog. From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml index 36fdd3c..44f8b01 100644 --- a/src/verilog/PrintHTL.ml +++ b/src/verilog/PrintHTL.ml @@ -1,5 +1,5 @@ (* -*- mode: tuareg -*- - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -open ValueInt +open Value open Datatypes open Camlcoq open AST @@ -27,7 +27,7 @@ open AST open HTL open PrintAST open PrintVerilog -open CoqupClflags +open VericertClflags let pstr pp = fprintf pp "%s" diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index a172b3a..f348ee6 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -1,5 +1,5 @@ (* -*- mode: tuareg -*- - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -17,7 +17,7 @@ *) open Verilog -open ValueInt +open Value open Datatypes open Camlcoq @@ -26,7 +26,7 @@ open Clflags open Printf -open CoqupClflags +open VericertClflags let concat = String.concat "" @@ -70,30 +70,16 @@ let unop = function let register a = sprintf "reg_%d" (P.to_int a) -let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l)) +let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l)) -let literal_int i = sprintf "32'd%d" i - -let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8) - - -let rec pprint_expr = - let array_byte r i = function - | 0 -> concat [register r; "["; pprint_expr i; "]"] - | n -> concat [register r; "["; pprint_expr i; " + "; literal_int n; "][7:0]"] - in function +let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s - | Vvarb0 s -> byte 0 s - | Vvarb1 s -> byte 1 s - | Vvarb2 s -> byte 2 s - | Vvarb3 s -> byte 3 s | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] - | Vload (s, i) -> concat ["{"; array_byte s i 3; ", "; array_byte s i 2; ", "; array_byte s i 1; ", "; array_byte s i 0; "}"] let rec pprint_stmnt i = let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s; @@ -183,12 +169,9 @@ let testbench = "module testbench; always #5 clk = ~clk; - reg [31:0] count; - initial count = 0; always @(posedge clk) begin - count <= count + 1; if (finish == 1) begin - $display(\"finished: %d cycles %d\", return_val, count); + $display(\"finished: %d\", return_val); $finish; end end diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 5fd8fe9..47af3ef 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -18,8 +18,8 @@ val pprint_stmnt : int -> Verilog.stmnt -> string -val print_value : out_channel -> ValueInt.value -> unit +val print_value : out_channel -> Value.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit -val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit +val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit diff --git a/src/verilog/Value.v b/src/verilog/Value.v index af2b822..41a41b4 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -21,7 +21,7 @@ From bbv Require Import Word. From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. -From coqup Require Import Coquplib. +From vericert Require Import Vericertlib. (* end hide *) (** * Value diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index 151feef..c7f69a1 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -21,7 +21,7 @@ From bbv Require Import Word. From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. -From coqup Require Import Coquplib. +From vericert Require Import Vericertlib. (* end hide *) (** * Value @@ -77,6 +77,7 @@ Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i. Definition valueToPtr (i : value) : Integers.ptrofs := Ptrofs.of_int i. +Search Ptrofs.of_int Ptrofs.to_int. Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 6a1bece..3b0dd0a 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -29,7 +29,7 @@ Require Import Lia. Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.ValueInt IntegerExtra AssocMap Array. +From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array. From compcert Require Events. From compcert Require Import Integers Errors Smallstep Globalenvs. @@ -155,18 +155,13 @@ Inductive unop : Type := (** ** Expressions *) Inductive expr : Type := -| Vlit : value -> expr (** literal *) -| Vvar : reg -> expr (** reg *) -| Vvarb0 : reg -> expr (** 1st byte projection of reg *) -| Vvarb1 : reg -> expr -| Vvarb2 : reg -> expr -| Vvarb3 : reg -> expr -| Vvari : reg -> expr -> expr (** array *) +| Vlit : value -> expr +| Vvar : reg -> expr +| Vvari : reg -> expr -> expr | Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr -| Vternary : expr -> expr -> expr -> expr -| Vload : reg -> expr -> expr. (** 4-byte concatenation load *) +| Vternary : expr -> expr -> expr -> expr. Definition posToExpr (p : positive) : expr := Vlit (posToValue p). @@ -340,57 +335,41 @@ Definition unop_run (op : unop) (v1 : value) : value := Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop := | erun_Vlit : - forall fext asr asa v, - expr_runp fext asr asa (Vlit v) v + forall fext reg stack v, + expr_runp fext reg stack (Vlit v) v | erun_Vvar : - forall fext asr asa v r, - asr#r = v -> - expr_runp fext asr asa (Vvar r) v - | erun_Vvarb0 : - forall fext asr asa v r, - asr#r = v -> - expr_runp fext asr asa (Vvarb0 r) (IntExtra.ibyte0 v) - | erun_Vvarb1 : - forall fext asr asa v r, - asr#r = v -> - expr_runp fext asr asa (Vvarb1 r) (IntExtra.ibyte1 v) - | erun_Vvarb2 : - forall fext asr asa v r, - asr#r = v -> - expr_runp fext asr asa (Vvarb2 r) (IntExtra.ibyte2 v) - | erun_Vvarb3 : - forall fext asr asa v r, - asr#r = v -> - expr_runp fext asr asa (Vvarb3 r) (IntExtra.ibyte3 v) + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvar r) v | erun_Vvari : - forall fext asr asa v iexp i r, - expr_runp fext asr asa iexp i -> - arr_assocmap_lookup asa r (valueToNat i) = Some v -> - expr_runp fext asr asa (Vvari r iexp) v + forall fext reg stack v iexp i r, + expr_runp fext reg stack iexp i -> + arr_assocmap_lookup stack r (valueToNat i) = Some v -> + expr_runp fext reg stack (Vvari r iexp) v | erun_Vbinop : - forall fext asr asa op l r lv rv resv, - expr_runp fext asr asa l lv -> - expr_runp fext asr asa r rv -> + forall fext reg stack op l r lv rv resv, + expr_runp fext reg stack l lv -> + expr_runp fext reg stack r rv -> Some resv = binop_run op lv rv -> - expr_runp fext asr asa (Vbinop op l r) resv + expr_runp fext reg stack (Vbinop op l r) resv | erun_Vunop : - forall fext asr asa u vu op oper resv, - expr_runp fext asr asa u vu -> + forall fext reg stack u vu op oper resv, + expr_runp fext reg stack u vu -> oper = unop_run op -> resv = oper vu -> - expr_runp fext asr asa (Vunop op u) resv + expr_runp fext reg stack (Vunop op u) resv | erun_Vternary_true : - forall fext asr asa c ts fs vc vt, - expr_runp fext asr asa c vc -> - expr_runp fext asr asa ts vt -> + forall fext reg stack c ts fs vc vt, + expr_runp fext reg stack c vc -> + expr_runp fext reg stack ts vt -> valueToBool vc = true -> - expr_runp fext asr asa (Vternary c ts fs) vt + expr_runp fext reg stack (Vternary c ts fs) vt | erun_Vternary_false : - forall fext asr asa c ts fs vc vf, - expr_runp fext asr asa c vc -> - expr_runp fext asr asa fs vf -> + forall fext reg stack c ts fs vc vf, + expr_runp fext reg stack c vc -> + expr_runp fext reg stack fs vf -> valueToBool vc = false -> - expr_runp fext asr asa (Vternary c ts fs) vf. + expr_runp fext reg stack (Vternary c ts fs) vf. Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) @@ -450,8 +429,8 @@ Inductive location : Type := | LocArray (_ : reg) (_ : nat). Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := -| Reg : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) -| RegIndexed : forall f asr asa r iexp iv, +| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) +| Indexed : forall f asr asa r iexp iv, expr_runp f asr asa iexp iv -> location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). @@ -795,16 +774,11 @@ Proof. repeat (try match goal with | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvarb0 _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvarb1 _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvarb2 _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvarb3 _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vload _ _) _ |- _ ] => invert H | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, H2 : expr_runp _ _ _ ?e _ |- _ ] => |