Module LowerBound
Let WFSKELINK: SkEnv.wf skenv_link.
Proof.
Let ININCL: forall p (IN: In p prog), <<INCL: SkEnv.includes skenv_link p.(Mod.sk)>>.
Proof.
Definition local_genv (p : Asm.program) :=
(skenv_link.(SkEnv.project) p.(Sk.of_program fn_sig)).(SkEnv.revive) p.
Lemma match_genvs_sub A B V W R (ge1: Genv.t A V) (ge2: Genv.t B W)
(MATCHGE: Genv.match_genvs R ge1 ge2):
sub_match_genvs R ge1 ge2.
Proof.
inv MATCHGE.
econs;
i;
ss;
eauto.
-
rewrite mge_next.
refl.
-
etrans;
eauto.
-
unfold Genv.find_def in *.
specialize (
mge_defs b).
inv mge_defs;
eq_closure_tac.
eauto.
Qed.
Lemma match_genvs_le A B V W R1 R2 (ge1: Genv.t A V) (ge2: Genv.t B W)
(MATCHGE: Genv.match_genvs R1 ge1 ge2)
(LE: R1 <2= R2):
Genv.match_genvs R2 ge1 ge2.
Proof.
inv MATCHGE. econs; i; ss; eauto.
cinv (mge_defs b).
- econs 1.
- econs 2. eapply LE; eauto.
Qed.
Definition genv_le (ge_src ge_tgt: Genv.t fundef unit): Prop :=
sub_match_genvs (@def_match _ _) ge_src ge_tgt.
Lemma skenv_link_public_eq id:
Genv.public_symbol skenv_link id = Senv.public_symbol (symbolenv (sem prog)) id.
Proof.
ss. des_ifs.
Qed.
Lemma MATCH_PROG:
match_prog sk tprog.
Proof.
Lemma public_eq:
prog_public sk = prog_public tprog.
Proof.
Lemma genv_public_eq:
Genv.genv_public skenv_link = Genv.genv_public tge.
Proof.
Lemma main_eq:
prog_main sk = prog_main tprog.
Proof.
Lemma match_skenv_link_tge :
Genv.match_genvs (fun skdef fdef => skdef_of_gdef fn_sig fdef = skdef) skenv_link tge.
Proof.
Lemma sub_match_local_genv ge_local
(MATCHGE: genv_le ge_local tge):
sub_match_genvs (fun fdef skdef => def_match (skdef_of_gdef fn_sig fdef) (skdef)) ge_local skenv_link.
Proof.
destruct match_skenv_link_tge.
inv MATCHGE.
unfold Genv.find_symbol,
Genv.find_def in *.
econs.
-
rewrite <-
mge_next.
eauto.
-
i.
eapply sub_mge_symb0 in FIND.
rewrite mge_symb in FIND.
eauto.
-
i.
eapply sub_mge_defs0 in FIND.
des.
specialize (
mge_defs b).
inv mge_defs.
+
eq_closure_tac.
+
eq_closure_tac.
esplits;
eauto.
inv MATCHDEF;
ss;
des_ifs;
econs.
Qed.
Inductive valid_owner fptr (p: Asm.program) : Prop :=
| valid_owner_intro
fd
(MSFIND: ge.(Ge.find_fptr_owner) fptr (AsmC.modsem skenv_link p))
(FINDF: Genv.find_funct (local_genv p) fptr = Some (Internal fd))
(PROGIN: In (AsmC.module p) prog).
Lemma owner_genv_le p
(IN: In (AsmC.module p) prog):
genv_le (local_genv p) tge.
Proof.
Lemma symb_preserved id:
Senv.public_symbol (symbolenv (semantics tprog)) id =
Senv.public_symbol (symbolenv (sem prog)) id.
Proof.
Lemma symb_main :
Genv.find_symbol skenv_link (prog_main sk) =
Genv.find_symbol tge (prog_main tprog).
Proof.
Lemma local_global_consistent
ge_local
(LE: genv_le ge_local tge)
fptr fd
(LOCAL: Genv.find_funct ge_local fptr = Some (Internal fd))
skd
(GLOBAL: Genv.find_funct skenv_link fptr = Some skd):
Sk.get_sig skd = fd.(fn_sig).
Proof.
initial memory ********************************
Variable m_init : mem.
Hypothesis INIT_MEM: sk.(Sk.load_mem) = Some m_init.
Definition m_tgt_init := m_init.
Lemma TGT_INIT_MEM: Genv.init_mem tprog = Some m_tgt_init.
Proof.
Definition init_inject := Mem.flat_inj (Mem.nextblock m_init).
Lemma initmem_inject: Mem.inject init_inject m_init m_tgt_init.
Proof.
Lemma init_inject_ge :
skenv_inject skenv_link init_inject m_init.
Proof.
Lemma senv_same :
(tge: Senv.t) = (skenv_link: Senv.t).
Proof.
Lemma system_symbols_inject j m
(SKINJ: skenv_inject skenv_link j m):
symbols_inject_weak j (System.globalenv skenv_link) skenv_link m.
Proof.
Section SYSTEM.
Lemma system_function_ofs j b_src b_tgt delta fd m
(SKINJ: skenv_inject skenv_link j m)
(FIND: Genv.find_funct_ptr (System.globalenv skenv_link) b_src = Some fd)
(INJ: j b_src = Some (b_tgt, delta)):
delta = 0.
Proof.
Lemma system_sig j b_src b_tgt delta ef m
(SKINJ: skenv_inject skenv_link j m)
(FIND: Genv.find_funct_ptr (System.globalenv skenv_link) b_src = Some (External ef))
(INJ: j b_src = Some (b_tgt, delta)):
Genv.find_funct_ptr tge b_tgt = Some (External ef).
Proof.
Lemma system_receptive_at st frs:
receptive_at (sem prog)
(State ((Frame.mk (System.modsem skenv_link) st) :: frs)).
Proof.
End SYSTEM.
Section ASMLEMMAS.
Lemma asm_determinate_at p st:
determinate_at (semantics p) st.
Proof.
generalize (
semantics_determinate p);
intro P.
inv P.
econs;
ii;
ss;
eauto.
eapply sd_final_nostep;
eauto.
Qed.
End ASMLEMMAS.
regset ********************************
Definition initial_regset : regset :=
(Pregmap.init Vundef)
# PC <- (Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero)
# RA <- Vnullptr
# RSP <- (Vptr 1%positive Ptrofs.zero).
Definition initial_tgt_regset := initial_regset.
Lemma init_mem_nextblock F V (p: AST.program F V) m
(INIT: Genv.init_mem p = Some m):
Plt 1 (Mem.nextblock m).
Proof.
Lemma update_agree j rs_src rs_tgt pr v
(AGREE: agree j rs_src rs_tgt)
(UPDATE: Val.inject j v (rs_tgt # pr)):
agree j (rs_src # pr <- v) rs_tgt.
Proof.
destruct pr; intros pr0; specialize (AGREE pr0); destruct pr0; eauto.
- destruct i, i0; eauto.
- destruct f, f0; eauto.
- destruct c, c0; eauto.
Qed.
Lemma initial_regset_agree: agree init_inject initial_regset initial_tgt_regset.
Proof.
calee initial ********************************
Inductive wf_init_rs (j: meminj) (rs_caller rs_callee: regset) : Prop :=
| wf_init_rs_intro
(PCSAME: rs_caller # PC = rs_callee # PC)
(RANOTFPTR: forall blk ofs (RAVAL: rs_callee RA = Vptr blk ofs),
~ Plt blk (Genv.genv_next skenv_link))
(RASAME: inj_same j (rs_caller # RA) (rs_callee # RA))
(RSPSAME: inj_same j (rs_caller # RSP) (rs_callee # RSP))
(CALLEESAVE: forall mr, Conventions1.is_callee_save mr ->
inj_same j (rs_caller (to_preg mr))
(rs_callee (to_preg mr))).
Lemma preg_case pr :
(exists mr, pr = to_preg mr) \/
(pr = PC) \/ (exists c, pr = CR c) \/ (pr = RSP) \/ (pr = RA).
Proof.
destruct (
to_mreg pr)
eqn:
EQ.
-
left.
exists m.
unfold to_mreg in *.
destruct pr;
clarify.
destruct i;
clarify;
auto.
destruct f;
clarify;
auto.
-
right.
unfold to_mreg in *.
destruct pr;
clarify;
eauto.
destruct i;
clarify;
auto.
destruct f;
clarify;
auto.
Qed.
Lemma callee_save_agree j rs_caller init_rs rs_callee rs_tgt sg mr rs
(WF: wf_init_rs j rs_caller init_rs)
(AGREE: agree j rs_callee rs_tgt)
(RETV: loc_result sg = One mr)
(CALLEESAVE: forall mr, Conventions1.is_callee_save mr ->
Val.lessdef (init_rs mr.(to_preg)) (rs_callee mr.(to_preg)))
(RSRA: rs_callee # PC = init_rs # RA)
(RSRSP: rs_callee # RSP = init_rs # RSP)
(RS: rs = (set_pair (loc_external_result sg) (rs_callee mr.(to_preg)) (Asm.regset_after_external rs_caller)) #PC <- (rs_caller RA)):
agree j rs rs_tgt.
Proof.
match stack ********************************
Inductive match_stack (j: meminj) : (Values.block -> Z -> Prop) -> regset -> list Frame.t -> Prop :=
| match_stack_init
init_rs P
(RSRA: init_rs # RA = Vnullptr)
(RSPC: init_rs # PC = Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero)
(SIG: skenv_link.(Genv.find_funct) (Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero) = Some (Internal signature_main)):
match_stack j P init_rs nil
| match_stack_cons
fr frs p st init_rs0 init_rs1 P0 P1 sg blk ofs
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p) (AsmC.mkstate init_rs1 st))
(STACK: match_stack j P0 init_rs1 frs)
(WF: wf_init_rs j st.(st_rs) init_rs0)
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = Some sg)
(RSPPTR: st.(st_rs) # RSP = Vptr blk ofs)
(RANGE: P0 \2/ (brange blk (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + 4 * size_arguments sg)) <2= P1):
match_stack j P1 init_rs0 (fr::frs)
| match_stack_cons_asmstyle
fr frs p st init_rs0 init_rs1 P0
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p) (AsmC.mkstate init_rs1 st))
(STACK: match_stack j P0 init_rs1 frs)
(WF: inj_same j (st.(st_rs) # RA) (init_rs0 # RA))
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = None):
match_stack j P0 init_rs0 (fr::frs)
.
Inductive match_stack_call (j: meminj) : mem -> (Values.block -> Z -> Prop) -> regset -> list Frame.t -> Prop :=
| match_stack_call_init
init_rs m P
(MEM: m = m_init)
(INITRS: init_rs = initial_regset)
(SIG: skenv_link.(Genv.find_funct) (Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero) = Some (Internal signature_main)):
match_stack_call j m P init_rs nil
| match_stack_call_cons
fr frs p st init_rs0 init_rs1 m P0 P1 sg blk ofs
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs1 st))
(INITRS: init_rs0 = st.(st_rs))
(STACK: match_stack j P0 init_rs1 frs)
(MEM: m = st.(st_m))
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = Some sg)
(RSPPTR: init_rs0 # RSP = Vptr blk ofs)
(RANGE: P0 \2/ (brange blk (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + 4 * size_arguments sg)) <2= P1):
match_stack_call j m P1 init_rs0 (fr::frs)
| match_stack_call_cons_asmstyle
fr frs p st init_rs0 init_rs1 m P0
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs1 st))
(INITRS: init_rs0 = st.(st_rs))
(STACK: match_stack j P0 init_rs1 frs)
(MEM: m = st.(st_m))
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = None):
match_stack_call j m P0 init_rs0 (fr::frs).
Lemma match_stack_incr j1 j2 init_rs l P0 P1
(INCR: inject_incr j1 j2)
(PLE: P0 <2= P1)
(MATCH: match_stack j1 P0 init_rs l):
match_stack j2 P1 init_rs l.
Proof.
revert init_rs INCR P0 P1 PLE MATCH.
induction l;
ss;
ii;
inv MATCH.
-
econs;
ss;
eauto.
-
econs;
ss;
auto.
+
eapply IHl;
cycle 2;
eauto.
+
inv WF.
econs;
eauto.
*
eapply inj_same_incr;
eauto.
*
eapply inj_same_incr;
eauto.
*
ii.
eapply inj_same_incr;
eauto.
+
eauto.
+
eauto.
+
eauto.
-
econs 3;
ss;
eauto.
eapply inj_same_incr;
eauto.
Qed.
Lemma frame_inj a0 b0 a1 b1
(EQ: Frame.mk a0 b0 = Frame.mk a1 b1):
b0 ~= b1.
Proof.
inv EQ. eauto. Qed.
Lemma asm_frame_inj se1 se2 p1 p2 st1 st2
(EQ : Frame.mk (modsem se1 p1) st1 = Frame.mk (modsem se2 p2) st2):
st1 = st2.
Proof.
Lemma asm_frame_inj2 p1 p2 st1 st2
(EQ : Frame.mk (modsem skenv_link p1) st1
= Frame.mk (modsem skenv_link p2) st2):
local_genv p1 = local_genv p2.
Proof.
Lemma skenv_inject_memory j m m_tgt
(GEINJECT: skenv_inject skenv_link j m)
(INJ: Mem.inject j m m_tgt):
Ple (Genv.genv_next skenv_link) (Mem.nextblock m).
Proof.
arguments ********************************
Program Definition callee_initial_mem' (blk: Values.block) (ofs: ptrofs)
(m0: mem) (m: mem) (sg: signature) (args: list val): mem :=
Mem.mkmem
(PMap.set
(m.(Mem.nextblock))
(_FillArgsParallel.fill_args_src_blk
(m0.(Mem.mem_contents) !! blk)
((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.mem_contents) !! (Mem.nextblock m))
(Ptrofs.unsigned ofs) 0 args (loc_arguments sg)) ((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.mem_contents)))
((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.mem_access))
((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.nextblock)) _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
Definition callee_initial_reg' (sg: signature) (args: list val): Mach.regset :=
fun mr => if extcall_args_reg mr sg
then _FillArgsParallel.fill_args_src_reg args (loc_arguments sg) mr
else Vundef.
Definition callee_initial_inj' (blk: Values.block) (ofs: ptrofs)
(j: meminj) (m_src: mem): meminj :=
fun blk' => if (peq blk' (Mem.nextblock m_src))
then
match (j blk) with
| Some (blk_tgt, delta) => Some (blk_tgt, delta + Ptrofs.unsigned ofs)
| None => None
end
else j blk'.
Lemma typify_list_lessdef args typs
(LEN: Datatypes.length args = Datatypes.length typs):
Val.lessdef_list (typify_list args typs) args.
Proof.
revert typs LEN.
induction args;
ss.
ii.
destruct typs;
inv LEN.
unfold typify_list,
zip,
typify.
des_ifs;
eauto.
Qed.
Lemma asm_extcall_arguments_mach rs m:
Asm.extcall_arguments rs m <2=
Mach.extcall_arguments (AsmregsC.to_mregset rs) m (rs RSP).
Proof.
ii.
eapply list_forall2_imply;
eauto.
i.
inv H1;
econs.
-
inv H2;
econs.
ss.
-
inv H2;
inv H3;
econs;
ss.
-
inv H2;
inv H3;
econs;
ss.
Qed.
Lemma callee_initial_arguments (rs: regset) m0 m1 blk ofs sg args targs
(ARGS: Asm.extcall_arguments rs m0 sg args)
(RSRSP: rs RSP = Vptr blk ofs)
(ARGRANGE: Ptrofs.unsigned ofs + 4 * size_arguments sg <= Ptrofs.max_unsigned)
(TYP: typecheck args sg targs):
Mach.extcall_arguments
(callee_initial_reg' sg targs)
(callee_initial_mem' blk ofs m0 m1 sg targs)
(Vptr (Mem.nextblock m1) Ptrofs.zero) sg targs.
Proof.
Lemma callee_initial_inj_incr blk ofs j m_src
(NONE: j (Mem.nextblock m_src) = None):
inject_incr j (callee_initial_inj' blk ofs j m_src).
Proof.
ii. unfold callee_initial_inj'. des_ifs; eauto.
Qed.
Lemma callee_initial_mem_nextblock m0 m1 blk ofs sg targs:
Mem.nextblock (callee_initial_mem' blk ofs m0 m1 sg targs) =
Pos.succ (Mem.nextblock m1).
Proof.
unfold callee_initial_mem'. ss.
Qed.
Lemma callee_initial_mem_perm m0 m1 blk ofs sg targs blk' ofs' p k:
Mem.perm (callee_initial_mem' blk ofs m0 m1 sg targs) blk' ofs' p k
<-> if (peq (Mem.nextblock m1) blk')
then (zle 0 ofs' && zlt ofs' (4 * size_arguments sg))
else Mem.perm m1 blk' ofs' p k.
Proof.
Lemma callee_initial_inject' (rs: regset) m_src0 m_src1 m_tgt j blk ofs sg args targs
(INJECT: Mem.inject j m_src0 m_tgt)
(ARGS: Asm.extcall_arguments rs m_src0 sg args)
(RSRSP: rs RSP = Vptr blk ofs)
(FREE: freed_from m_src0 m_src1 blk ofs.(Ptrofs.unsigned) (ofs.(Ptrofs.unsigned) + 4 * (size_arguments sg)))
(ARGRANGE: Ptrofs.unsigned ofs + 4 * size_arguments sg <= Ptrofs.max_unsigned)
(TYP: typecheck args sg targs)
(ALIGN: forall chunk (CHUNK: size_chunk chunk <= 4 * (size_arguments sg)),
(align_chunk chunk | ofs.(Ptrofs.unsigned))):
Mem.inject
(callee_initial_inj' blk ofs j m_src1)
(callee_initial_mem' blk ofs m_src0 m_src1 sg targs)
m_tgt.
Proof.
Lemma callee_initial_rsp_inj_same blk ofs j m
(VALID: j (Mem.nextblock m) = None)
(MAPPED: j blk <> None):
inj_same
(callee_initial_inj' blk ofs j m)
(Vptr blk ofs)
(Vptr (Mem.nextblock m) Ptrofs.zero).
Proof.
unfold callee_initial_inj'.
destruct (
j blk)
as [[]|]
eqn:
EQ;
clarify.
econs;
eauto.
-
instantiate (1:=
z).
instantiate (1:=
b).
des_ifs.
-
des_ifs.
-
rewrite Ptrofs.unsigned_zero.
lia.
Qed.
Require Import JunkBlock.
Definition pos_nat_add (p: positive) (n: nat) : positive :=
if Zerob.zerob n
then p
else (p + Pos.of_nat n)%positive.
Fixpoint callee_initial_junk' (rs: regset) (nb: Values.block) (j: meminj) (l: list preg)
: regset * nat * meminj :=
match l with
| [] => (rs, 0%nat, j)
| hd::tl =>
match callee_initial_junk' rs nb j tl with
| (rs', n, j') =>
match rs' hd with
| Vptr blk ofs =>
(Pregmap.set hd (Vptr (pos_nat_add nb n) ofs) rs',
Datatypes.S n,
(fun blk' => if peq blk' (pos_nat_add nb n)
then (j' blk)
else (j' blk')))
| _ => (rs', n, j')
end
end
end.
Lemma assign_junk_blocks_contents m n b
(VALID: Mem.valid_block m b):
(Mem.mem_contents (assign_junk_blocks m n)) !! b = (Mem.mem_contents m) !! b.
Proof.
Lemma callee_initial_junk_spec rs_src rs_tgt rs' m_src m_tgt j j' l n
(AGREE: agree j rs_src rs_tgt)
(INJECT: Mem.inject j m_src m_tgt)
(INITIAL: callee_initial_junk' rs_src m_src.(Mem.nextblock) j l = (rs', n, j')):
(<<AGREE: agree j' rs' rs_tgt>>) /\
(<<INJECT: Mem.inject j' (assign_junk_blocks m_src n) m_tgt>>) /\
(<<SEP: forall b p (NOTMAP: j b = None) (MAP: j' b = Some p),
~ Mem.valid_block m_src b>>) /\
(<<INCR: inject_incr j j'>>) /\
(<<JUNK: forall r (IN: In r l),
is_junk_value m_src (assign_junk_blocks m_src n) (rs' r)>>) /\
(<<SAME: forall r, inj_same j' (rs_src r) (rs' r)>>) /\
(<<EQ: forall r (NIN: ~ In r l), rs_src r = rs' r>>)
.
Proof.
revert l rs'
j'
n INITIAL.
induction l;
ss;
i;
clarify.
-
esplits;
eauto.
+
ii.
clarify.
+
i.
clarify.
-
des_ifs_safe.
exploit IHl;
eauto.
i.
des.
assert ((
exists blk ofs,
r a =
Vptr blk ofs) \/ (
forall blk ofs,
r a <>
Vptr blk ofs)).
{
clear.
destruct (
r a);
eauto;
try by (
right;
ii;
clarify). }
des.
{
des_ifs.
assert (
INCR0:
inject_incr
m
(
fun blk' =>
if peq blk' (
pos_nat_add (
Mem.nextblock m_src)
n0)
then m blk else m blk')).
{
ii.
des_ifs_safe;
eauto.
des_ifs_safe.
exfalso.
eapply Mem.valid_block_inject_1 in H;
eauto.
unfold Mem.valid_block in *.
clear -
H.
rewrite assign_junk_blocks_nextblock in *.
eapply Plt_strict;
eauto. }
esplits;
eauto.
-
ii.
unfold Pregmap.set.
des_ifs.
+
cinv (
AGREE0 a);
rewrite Heq0 in *;
clarify.
econs;
des_ifs.
+
eapply val_inject_incr;
eauto.
-
econs; [
econs|..];
i;
try erewrite assign_junk_blocks_perm in *.
+
des_ifs.
*
exfalso.
eapply Mem.perm_valid_block in H0.
clear -
H0.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega.
*
eapply Mem.mi_perm;
try apply INJECT0;
eauto.
erewrite assign_junk_blocks_perm in *.
auto.
+
des_ifs.
*
unfold Mem.range_perm in *.
exfalso.
exploit H0;
eauto.
{
instantiate (1:=
ofs0).
set (
size_chunk_pos chunk).
lia. }
erewrite assign_junk_blocks_perm.
i.
eapply Mem.perm_valid_block in H1.
clear -
H1.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega.
*
eapply Mem.mi_align;
try apply INJECT0;
eauto.
unfold Mem.range_perm in *.
try erewrite assign_junk_blocks_perm in *.
eauto.
+
des_ifs.
*
exfalso.
eapply Mem.perm_valid_block in H0.
clear -
H0.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega.
*
replace (
ZMap.get ofs0 (
Mem.mem_contents (
assign_junk_blocks m_src (
Datatypes.S n0))) !!
b1)
with (
ZMap.get ofs0 (
Mem.mem_contents (
assign_junk_blocks m_src n0)) !!
b1).
{
exploit Mem.mi_memval;
try apply INJECT0;
eauto.
-
try erewrite assign_junk_blocks_perm in *.
eauto.
-
i.
eapply memval_inject_incr;
eauto. }
{
repeat erewrite assign_junk_blocks_contents;
auto.
-
eapply Mem.perm_valid_block;
eauto.
-
eapply Mem.perm_valid_block;
eauto. }
+
des_ifs.
*
unfold pos_nat_add,
Mem.valid_block in *.
rewrite assign_junk_blocks_nextblock in *.
exfalso.
apply H.
clear.
ss.
des_ifs;
try xomega.
*
eapply Mem.mi_freeblocks;
try apply INJECT0.
ii.
apply H.
unfold Mem.valid_block in *.
rewrite assign_junk_blocks_nextblock in *.
clear -
H0.
eapply Plt_Ple_trans;
eauto.
unfold Zerob.zerob in *.
ss.
des_ifs;
try xomega.
+
des_ifs.
*
eapply Mem.mi_mappedblocks;
try apply INJECT0;
eauto.
*
eapply Mem.mi_mappedblocks;
try apply INJECT0;
eauto.
+
ii.
try erewrite assign_junk_blocks_perm in *.
eapply Mem.mi_no_overlap;
try apply INJECT0;
eauto.
*
clear H1.
des_ifs.
exfalso.
eapply Mem.perm_valid_block in H2.
clear -
H2.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega.
*
clear H2.
des_ifs.
exfalso.
eapply Mem.perm_valid_block in H3.
clear -
H3.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega.
*
erewrite assign_junk_blocks_perm in *.
auto.
*
erewrite assign_junk_blocks_perm in *.
auto.
+
des_ifs.
*
exfalso.
des.
{
eapply Mem.perm_valid_block in H0.
clear -
H0.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega. }
{
eapply Mem.perm_valid_block in H0.
clear -
H0.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega. }
*
eapply Mem.mi_representable;
try eapply INJECT0;
eauto.
try erewrite assign_junk_blocks_perm in *.
eauto.
+
des_ifs.
*
right.
ii.
eapply Mem.perm_valid_block in H1.
clear -
H1.
unfold pos_nat_add,
Mem.valid_block in *.
des_ifs;
xomega.
*
exploit Mem.mi_perm_inv;
try apply INJECT0;
eauto.
i.
try erewrite assign_junk_blocks_perm in *.
eauto.
-
ii.
unfold Mem.valid_block in *.
des_ifs.
+
clear -
H.
unfold pos_nat_add in *.
des_ifs;
xomega.
+
exploit SEP;
eauto.
-
des_ifs.
etrans;
eauto.
-
ii.
des.
+
clarify.
rewrite Pregmap.gss.
unfold is_junk_value,
Mem.valid_block.
rewrite assign_junk_blocks_nextblock.
split.
*
clear.
unfold pos_nat_add.
des_ifs;
xomega.
*
clear.
unfold pos_nat_add.
ss.
des_ifs;
xomega.
+
exploit JUNK;
eauto.
i.
unfold is_junk_value,
Mem.valid_block in *.
rewrite assign_junk_blocks_nextblock in *.
unfold Pregmap.set.
clear -
H Heq0.
unfold pos_nat_add.
ss.
des_ifs;
split;
try xomega.
des.
destruct n0;
clarify;
ss;
xomega.
-
ii.
unfold Pregmap.set.
des_ifs.
+
cinv (
SAME a).
*
rewrite VAL1 in *;
clarify;
eauto.
econs;
eauto.
des_ifs.
*
rewrite Heq0 in *.
cinv (
AGREE0 a);
rewrite Heq0 in *;
clarify.
econs;
eauto.
des_ifs.
+
eapply inj_same_incr;
eauto.
-
i.
unfold Pregmap.set.
des_ifs.
+
exfalso.
eauto.
+
eapply EQ;
eauto. }
{
assert ((
r,
n0,
m) = (
rs',
n,
j')).
{
des_ifs.
exfalso.
eapply H;
eauto. }
clear INITIAL.
clarify.
esplits;
eauto.
i.
des;
clarify;
eauto.
unfold is_junk_value.
des_ifs.
exfalso.
eapply H;
eauto. }
Qed.
Definition callee_save_registers : list preg :=
[RA; IR RBX; IR RBP; IR R12; IR R13; IR R14; IR R15].
Lemma callee_save_registers_spec r:
In r callee_save_registers <->
((exists mr (MR: to_preg mr = r), is_callee_save mr) \/
(r = RA)).
Proof.
split.
-
i.
ss.
destruct H;
eauto.
destruct (
to_mreg r)
eqn:
MR.
+
left.
exists m.
des;
clarify;
eexists;
ss;
clarify.
+
des;
clarify.
-
unfold is_callee_save.
i.
des.
+
des_ifs;
ss;
eauto 10.
+
ss.
eauto.
Qed.
match states ********************************
Definition different_owner (v0 v1 : val): Prop :=
forall mod0 mod1
(OWNER0: ge.(Ge.find_fptr_owner) v0 mod0)
(OWNER1: ge.(Ge.find_fptr_owner) v1 mod1),
mod0 <> mod1.
Inductive match_states : Sem.state -> Asm.state -> nat -> Prop :=
| match_states_intro
j fr frs p init_rs rs_src rs_tgt m_src m_tgt n P
(AGREE: agree j rs_src rs_tgt)
(INJ: Mem.inject j m_src m_tgt)
(MEMWF: Mem.unchanged_on (loc_not_writable m_init) m_init m_src)
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(GEINJECT: skenv_inject skenv_link j m_src)
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs (Asm.State rs_src m_src)))
(STACK: match_stack j P init_rs frs)
(PWF: P <2= ~2 (SimMemInj.valid_blocks m_init /2\ loc_not_writable m_init))
(WFINJ: inj_range_wf skenv_link j m_src P)
(ORD: n = if (external_state (local_genv p) (rs_src # PC))
then (length frs + 2)%nat else 0%nat):
match_states (State (fr::frs)) (Asm.State rs_tgt m_tgt) n
| match_states_call
j init_rs frs args fptr_arg vs_arg m_arg m_src rs_tgt m_tgt ofs blk sg P n
(CSTYLE: args = Args.Cstyle fptr_arg vs_arg m_arg)
(STACK: match_stack_call j m_src P init_rs frs)
(PWF: P <2= ~2 (SimMemInj.valid_blocks m_init /2\ loc_not_writable m_init))
(AGREE: agree j init_rs rs_tgt)
(INJECT: Mem.inject j m_src m_tgt)
(MEMWF: Mem.unchanged_on (loc_not_writable m_init) m_init m_src)
(GEINJECT: skenv_inject skenv_link j m_src)
(FPTR: fptr_arg = init_rs # PC)
(ARGRANGE: Ptrofs.unsigned ofs + 4 * size_arguments sg <= Ptrofs.max_unsigned)
(SIG: exists skd, skenv_link.(Genv.find_funct) fptr_arg
= Some skd /\ Sk.get_csig skd = Some sg)
(ALIGN: forall chunk (CHUNK: size_chunk chunk <= 4 * (size_arguments sg)),
(align_chunk chunk | ofs.(Ptrofs.unsigned)))
(ARGS: Asm.extcall_arguments init_rs m_src sg vs_arg)
(RSPPTR: init_rs # RSP = Vptr blk ofs)
(WFINJ: inj_range_wf skenv_link j m_arg P)
(RAPTR: <<TPTR: Val.has_type (init_rs RA) Tptr>> /\ <<RADEF: init_rs RA <> Vundef>>)
(FREE: freed_from m_src m_arg blk ofs.(Ptrofs.unsigned) (ofs.(Ptrofs.unsigned) + 4 * (size_arguments sg)))
(ORD: n = 1%nat):
match_states (Callstate args frs) (Asm.State rs_tgt m_tgt) n
| match_states_call_asmstyle
j init_rs frs args m_src rs_tgt m_tgt P n
(ASMSTYLE: args = Args.Asmstyle init_rs m_src)
(STACK: match_stack_call j m_src P init_rs frs)
(PWF: P <2= ~2 (SimMemInj.valid_blocks m_init /2\ loc_not_writable m_init))
(AGREE: agree j init_rs rs_tgt)
(INJECT: Mem.inject j m_src m_tgt)
(MEMWF: Mem.unchanged_on (loc_not_writable m_init) m_init m_src)
(GEINJECT: skenv_inject skenv_link j m_src)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs # PC)
= Some skd /\ Sk.get_csig skd = None)
(WFINJ: inj_range_wf skenv_link j m_src P)
(RAPTR: <<TPTR: Val.has_type (init_rs RA) Tptr>> /\ <<RADEF: init_rs RA <> Vundef>>)
(ORD: n = 1%nat):
match_states (Callstate args frs) (Asm.State rs_tgt m_tgt) n
.
Lemma init_volatile_readonly blk
(VOL: Genv.block_is_volatile skenv_link blk)
ofs:
loc_not_writable m_init blk ofs.
Proof.
Lemma volatile_readonly m blk
(MEMWF: Mem.unchanged_on (loc_not_writable m_init) m_init m)
(VOL: Genv.block_is_volatile skenv_link blk)
ofs:
loc_not_writable m blk ofs.
Proof.
Lemma inj_range_wf_step j0 j1 m0 m1 P
(MEMPERM: forall blk ofs p, Mem.perm m1 blk ofs Max p -> Mem.perm m0 blk ofs Max p \/ j0 blk = None)
(INCR: inject_incr j0 j1)
(RANGEWF: inj_range_wf skenv_link j0 m0 P)
(INJ: exists m_tgt, Mem.inject j1 m1 m_tgt):
inj_range_wf skenv_link j1 m1 P.
Proof.
ii.
des.
inv INJ.
inv mi_inj.
destruct (
RANGEWF blk).
-
destruct (
j1 blk)
eqn:
EQ.
+
destruct p.
econs 2;
eauto;
ii.
*
eapply mi_align;
eauto.
ii.
specialize (
H _ H0).
ss.
des.
--
eapply Mem.perm_max;
eauto.
--
exfalso.
eapply BOT.
eauto.
*
des;
exfalso;
eapply BOT;
eauto.
*
exfalso.
eapply BOT.
eauto.
+
econs 1;
eauto.
-
econs 2;
eauto.
ii.
eapply ALIGN.
ii.
specialize (
H x0 PR).
ss.
des;
eauto.
eapply Mem.perm_max in H.
eapply MEMPERM in H.
des;
clarify.
eauto.
Qed.
Lemma asm_step_init_simulation
args frs st_tgt p n
(MTCHST: match_states (Callstate args frs) st_tgt n)
(OWNER: valid_owner args.(Args.get_fptr) p)
(PROGIN: In (AsmC.module p) prog):
exists rs m,
(AsmC.initial_frame skenv_link p args (AsmC.mkstate rs (Asm.State rs m))) /\
(match_states (State ((Frame.mk (AsmC.modsem skenv_link p) (AsmC.mkstate rs (Asm.State rs m))) :: frs)) st_tgt 0).
Proof.
transf initial final ********************************
Lemma transf_initial_states:
forall st1, Sem.initial_state prog st1 ->
exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2 1.
Proof.
Lemma transf_final_states:
forall st1 st2 r n,
match_states st1 st2 n -> Sem.final_state st1 r -> Asm.final_state st2 r.
Proof.
intros st_src st_tgt r n MTCHST FINAL.
inv FINAL.
inv MTCHST.
ss.
inv FINAL0;
clarify.
inv STACK.
econs.
-
specialize (
AGREE PC).
rewrite RSRA in *.
rewrite RSRA0 in *.
inv AGREE;
ss.
-
des.
rewrite RSPC in *.
exploit local_global_consistent;
eauto.
intro SGEQ.
rewrite <-
SGEQ in *.
clarify.
ss.
unfold signature_main,
loc_arguments,
loc_result in *.
Transparent Archi.ptr64.
ss.
unfold loc_result_64 in *.
ss.
clarify.
ss.
specialize (
AGREE RAX).
clarify.
ss.
rewrite INT in *.
inv AGREE;
auto.
Qed.
transf step ********************************
Lemma asm_step_internal_simulation
st_src0 st_src1 st_tgt0 tr frs p init_rs n0
(STEP: Asm.step skenv_link (local_genv p) st_src0 tr st_src1)
(PROGIN: In (AsmC.module p) prog)
(MTCHST: match_states (State ((Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs st_src0))::frs)) st_tgt0 n0):
exists st_tgt1 n1,
Asm.step skenv_link tge st_tgt0 tr st_tgt1 /\
match_states (State ((Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs st_src1))::frs)) st_tgt1 n1.
Proof.
Lemma step_internal_simulation
fr0 frs tr st0 st_tgt0 n0
(STEP: fr0.(Frame.ms).(ModSem.step) skenv_link fr0.(Frame.ms).(ModSem.globalenv) fr0.(Frame.st) tr st0)
(MTCHST: match_states (State (fr0 :: frs)) st_tgt0 n0):
exists st_tgt1 n1, Asm.step skenv_link tge st_tgt0 tr st_tgt1 /\
match_states (State ((fr0.(Frame.update_st) st0) :: frs)) st_tgt1 n1.
Proof.
inv MTCHST.
inv STEP.
exploit asm_step_internal_simulation;
ss;
eauto.
-
econs;
eauto.
-
ii.
des.
esplits;
ss;
eauto.
destruct st0;
ss;
clarify.
eassumption.
Qed.
Lemma Mem_unchanged_on_strengthen P m0 m1:
Mem.unchanged_on P m0 m1 <-> Mem.unchanged_on (SimMemInj.valid_blocks m0 /2\ P) m0 m1.
Proof.
Lemma step_return_simulation
fr0 fr1 frs retv st0 st_tgt n0
(FINAL: fr0.(Frame.ms).(ModSem.final_frame) fr0.(Frame.st) retv)
(AFTER: fr1.(Frame.ms).(ModSem.after_external) fr1.(Frame.st) retv st0)
(MTCHST: match_states (State (fr0 :: fr1 :: frs)) st_tgt n0):
exists n1, match_states (State ((fr1.(Frame.update_st) st0) :: frs)) st_tgt n1 /\ (n1 < n0)%nat.
Proof.
Lemma step_call_simulation
fr0 frs args st_tgt n
(AT: fr0.(Frame.ms).(ModSem.at_external) fr0.(Frame.st) args)
(MTCHST: match_states (State (fr0 :: frs)) st_tgt n):
match_states (Callstate args (fr0 :: frs)) st_tgt 1%nat.
Proof.
Lemma below_block_is_volatile F V (ge': Genv.t F V) b
(LE: ~ Plt b (Genv.genv_next ge')):
Genv.block_is_volatile ge' b = false.
Proof.
Lemma step_init_simulation
args frs st_tgt p n
(MTCHST: match_states (Callstate args frs) st_tgt n)
(OWNER: valid_owner args.(Args.get_fptr) p)
(PROGIN: In (AsmC.module p) prog):
exists st_src, step ge (Callstate args frs) E0 st_src /\ match_states st_src st_tgt 0.
Proof.
Lemma at_external_external p st frs st_tgt n args
(MTCHST: match_states
(State
((Frame.mk (AsmC.modsem skenv_link p) st)::frs))
st_tgt n)
(ATEXTERNAL: at_external skenv_link p st args):
(1 < n)%nat.
Proof.
Lemma normal_state_fsim_step frs st_src1 st_tgt0 t n0
(MTCHST: match_states (State frs) st_tgt0 n0)
(STEP: step ge (State frs) t st_src1):
(exists st_tgt1 n1, Asm.step skenv_link tge st_tgt0 t st_tgt1 /\ match_states st_src1 st_tgt1 n1) \/
(exists n1, match_states st_src1 st_tgt0 n1 /\ n1 < n0)%nat /\ (t = E0).
Proof.
Lemma owner_asm_or_system fptr ms
(OWNER: Ge.find_fptr_owner ge fptr ms):
(<<ASMMOD: exists p, ms = AsmC.modsem skenv_link p /\ In (AsmC.module p) prog>>)\/
(<<SYSMOD: ms = System.modsem skenv_link>>).
Proof.
inv OWNER.
clear -
MODSEM.
unfold ge in *.
unfold load_genv,
load_modsems,
prog,
flip in *.
ss.
des;
auto.
left.
generalize progs ms MODSEM.
intros l.
induction l;
ss;
i.
des;
eauto.
rewrite in_map_iff in *.
des.
clarify.
rewrite in_map_iff in *.
des.
clarify.
exists x1.
esplits;
eauto.
right.
apply in_map_iff.
esplits;
et.
Qed.
Lemma find_fptr_owner_determ
fptr ms0 ms1
(FIND0: Ge.find_fptr_owner ge fptr ms0)
(FIND1: Ge.find_fptr_owner ge fptr ms1):
ms0 = ms1
.
Proof.
Lemma init_case st args frs fptr
(STATE: st = Callstate args frs)
(FPTR: fptr = args.(Args.get_fptr)):
(<<ASMMOD: exists p, valid_owner fptr p>>) \/
(<<SYSMOD: ge.(Ge.find_fptr_owner)
fptr (System.modsem skenv_link)>>) \/
(<<UNSAFE: ~ safe (sem prog) st>>).
Proof.
Lemma call_step_noevent ge' args frs st1 tr
(STEP: step ge' (Callstate args frs) tr st1):
E0 = tr.
Proof.
inv STEP. auto. Qed.
Lemma syscall_receptive
st_src0 st_src1 st_tgt0 args frs fptr tr0 n0
(STATE: st_src0 = Callstate args frs)
(FPTR: fptr = args.(Args.get_fptr))
(SYSMOD: ge.(Ge.find_fptr_owner)
fptr (System.modsem skenv_link))
(MTCHST: match_states st_src0 st_tgt0 n0)
(STEP0: Sem.step ge st_src0 tr0 st_src1):
receptive_at (sem prog) st_src1.
Proof.
Lemma syscall_simulation
st_src0 st_src1 st_src2 st_tgt0 args frs fptr tr0 tr1 n0
(STATE: st_src0 = Callstate args frs)
(FPTR: fptr = args.(Args.get_fptr))
(SYSMOD: ge.(Ge.find_fptr_owner)
fptr (System.modsem skenv_link))
(MTCHST: match_states st_src0 st_tgt0 n0)
(STEP0: Sem.step ge st_src0 tr0 st_src1)
(STEP1: Sem.step ge st_src1 tr1 st_src2):
receptive_at (sem prog) st_src2 /\
exists st_tgt1 n1,
(<< STEPTGT: Asm.step skenv_link tge st_tgt0 tr1 st_tgt1 >>) /\
(<< MTCHST: forall st_src3 tr2
(STEP2: Sem.step ge st_src2 tr2 st_src3),
match_states st_src3 st_tgt1 n1 /\ tr2 = E0>>) /\
(n1 < length frs + 3)%nat.
Proof.
Lemma match_states_call_ord_1 args frs st_tgt n
(MTCHST: match_states (Callstate args frs) st_tgt n):
1%nat = n.
Proof.
inv MTCHST; auto. Qed.
Lemma src_receptive_at st_src st_tgt n
(MTCHST: match_states st_src st_tgt n):
receptive_at (sem prog) st_src.
Proof.
inv MTCHST;
ss.
-
eapply SemProps.lift_receptive_at.
{
ss.
des_ifs. }
ss.
eapply modsem_receptive.
-
econs;
i.
+
set (
STEP :=
H).
inv STEP.
inv H0.
eexists.
eauto.
+
ii.
inv H.
ss.
omega.
-
econs;
i.
+
set (
STEP :=
H).
inv STEP.
inv H0.
eexists.
eauto.
+
ii.
inv H.
ss.
omega.
Qed.
Lemma match_state_xsim:
forall st_src st_tgt n (MTCHST: match_states st_src st_tgt n),
xsim (sem prog) (semantics tprog) lt n st_src st_tgt.
Proof.
pcofix CIH.
i.
pfold.
destruct st_src.
-
exploit init_case;
ss.
instantiate (1:=
frs).
instantiate (2:=
args).
i.
des.
+
destruct (
match_states_call_ord_1 MTCHST).
right.
econs;
i.
*
exfalso.
inv MTCHST.
{
inv FINALTGT.
inv ASMMOD.
inv MSFIND.
unfold Genv.find_funct in *.
ss.
des_ifs.
specialize (
AGREE PC).
inv AGREE;
rewrite Heq in *;
clarify.
unfold Vnullptr in *.
des_ifs.
congruence. }
{
inv FINALTGT.
inv ASMMOD.
inv MSFIND.
unfold Genv.find_funct in *.
ss.
des_ifs.
specialize (
AGREE PC).
inv AGREE;
rewrite Heq in *;
clarify.
unfold Vnullptr in *.
des_ifs.
congruence. }
*
exploit step_init_simulation;
try eassumption.
{
inv ASMMOD.
eauto. }
i.
des.
econs 2;
ss;
eauto.
rewrite LINK_SK.
split;
auto.
apply star_one.
eauto.
+
left.
right.
econs.
econs 1;
et;
cycle 1.
{
i.
exfalso.
inv FINALSRC. }
i.
destruct (
call_step_noevent STEPSRC).
destruct (
match_states_call_ord_1 MTCHST).
exists 0%
nat.
exists st_tgt.
split.
{
right.
split;
auto. }
left.
pfold.
left.
right.
econs.
econs;
et;
cycle 1.
{
i.
exfalso.
inv STEPSRC.
ss.
rewrite LINK_SK in *.
destruct (
find_fptr_owner_determ SYSMOD MSFIND).
inv INIT.
inv FINALSRC.
inv FINAL. }
i.
exists (
length frs + 3)%
nat.
ss.
rewrite LINK_SK in *.
exploit syscall_simulation;
eauto.
i.
des.
exists st_tgt1.
split.
{
left.
split;
cycle 1.
{
inv STEPSRC.
ss.
destruct (
find_fptr_owner_determ SYSMOD MSFIND).
ss.
eapply system_receptive_at. }
apply plus_one.
econs; [
apply asm_determinate_at|].
s.
folder.
rewrite senv_same.
auto. }
left.
pfold.
left.
right.
econs.
econs;
et;
cycle 1.
{
i.
exfalso.
inv STEPSRC.
ss.
destruct (
find_fptr_owner_determ SYSMOD MSFIND).
inv INIT.
inv STEPSRC0;
ss; [|
inv FINAL].
inv STEP.
inv FINALSRC.
ss.
inv MTCHST.
inv STACK.
inv SYSMOD.
ss.
unfold System.globalenv in *.
unfold initial_regset,
Pregmap.set in *.
des_ifs.
clarify. }
i.
ss.
rewrite LINK_SK in *.
apply MTCHST0 in STEPSRC1.
des.
clarify.
exists n1,
st_tgt1.
split.
{
right.
split;
auto. }
right.
eauto.
+
right.
econs;
i;
try (
exfalso;
eauto).
-
left.
right.
econs.
econs;
cycle 1.
+
i.
econs.
*
exploit transf_final_states;
eauto.
*
i.
inv FINAL0.
inv FINAL1.
eq_closure_tac.
*
ii.
inv FINAL.
inv H;
eq_closure_tac.
+ *
i.
ss.
rewrite LINK_SK in *.
exploit normal_state_fsim_step;
eauto.
i.
des;
esplits;
eauto.
--
left.
split;
cycle 1.
{
eapply src_receptive_at;
eauto. }
econs;
ss.
++
econs;
eauto.
{
apply asm_determinate_at. }
s.
folder.
rewrite senv_same.
et.
++
econs 1.
++
rewrite E0_right.
auto.
Qed.
Lemma transf_xsim_properties:
xsim_properties (sem prog) (semantics tprog) nat lt.
Proof.
Lemma transf_program_correct:
mixed_simulation (Sem.sem prog) (Asm.semantics tprog).
Proof.
End PRESERVATION.
Require Import BehaviorsC.
Theorem lower_bound_correct
(asms: list Asm.program):
(<<INITUB: program_behaves (sem (map AsmC.module asms)) (Goes_wrong E0)>>) \/
exists link_tgt,
(<<TGT: link_list asms = Some link_tgt>>)
/\ (<<REFINE: improves (sem (map AsmC.module asms)) (Asm.semantics link_tgt)>>).
Proof.