Theory Fun6_secure
subsection "Proof"
theory Fun6_secure
imports Fun6
begin
definition common :: "enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool"
where
"common = (λw1 w2
(pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(pstate3 = pstate4 ∧
cfg1 = cfg3 ∧ cfg2 = cfg4 ∧
pcOf cfg3 = pcOf cfg4 ∧ map pcOf cfgs3 = map pcOf cfgs4 ∧
pcOf cfg3 ∈ PC ∧ pcOf ` (set cfgs3) ⊆ PC ∧
llength ibT1 = ∞ ∧ llength ibT2 = ∞ ∧
llength ibUT1 = ∞ ∧ llength ibUT2 = ∞ ∧
ibT1 = ibT3 ∧ ibT2 = ibT4 ∧
ibUT1 = ibUT3 ∧ ibUT2 = ibUT4 ∧
w1 = w2 ∧
array_base aa1 (getAvstore (stateOf cfg3)) = array_base aa1 (getAvstore (stateOf cfg4)) ∧
(∀cfg3'∈set cfgs3. array_base aa1 (getAvstore (stateOf cfg3')) = array_base aa1 (getAvstore (stateOf cfg3))) ∧
(∀cfg4'∈set cfgs4. array_base aa1 (getAvstore (stateOf cfg4')) = array_base aa1 (getAvstore (stateOf cfg4))) ∧
array_base aa2 (getAvstore (stateOf cfg3)) = array_base aa2 (getAvstore (stateOf cfg4)) ∧
(∀cfg3'∈set cfgs3. array_base aa2 (getAvstore (stateOf cfg3')) = array_base aa2 (getAvstore (stateOf cfg3))) ∧
(∀cfg4'∈set cfgs4. array_base aa2 (getAvstore (stateOf cfg4')) = array_base aa2 (getAvstore (stateOf cfg4))) ∧
(statA = Diff ⟶ statO = Diff) ∧
Dist ls1 ls2 ls3 ls4))"
lemma common_implies: "common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf cfg1 < 14 ∧ pcOf cfg2 = pcOf cfg1 ∧
ibT1 ≠ [[]] ∧ ibT2 ≠ [[]] ∧
ibUT1 ≠ [[]] ∧ ibUT2 ≠ [[]] ∧
w1 = w2"
unfolding common_def PC_def by (auto simp: image_def subset_eq)
definition Δ0 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δ0 = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ∧
pcOf cfg3 ∈ beforeWhile ∧
(pcOf cfg3 > 1 ⟶ same_var_o tt cfg3 cfgs3 cfg4 cfgs4) ∧
(pcOf cfg3 > 2 ⟶ same_var_o xx cfg3 cfgs3 cfg4 cfgs4) ∧
(pcOf cfg3 > 4 ⟶ same_var_o xx cfg3 cfgs3 cfg4 cfgs4) ∧
noMisSpec cfgs3
))"
lemmas Δ0_defs = Δ0_def common_def PC_def same_var_o_def
beforeWhile_def noMisSpec_def
lemma Δ0_implies: "Δ0 num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf cfg1 < 14 ∧ pcOf cfg2 = pcOf cfg1 ∧
ibT1 ≠ [[]] ∧ ibT2 ≠ [[]] ∧
ibUT1 ≠ [[]] ∧ ibUT2 ≠ [[]] ∧
cfgs4 = []"
apply (meson Δ0_def common_implies)
by (simp_all add: Δ0_defs, metis Nil_is_map_conv)
definition Δ1 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δ1 = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ∧
pcOf cfg3 ∈ afterWhile ∧
same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
noMisSpec cfgs3
))"
lemmas Δ1_defs = Δ1_def common_def noMisSpec_def PC_def afterWhile_def same_var_o_def
lemma Δ1_implies: "Δ1 n w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf cfg3 < 14 ∧ cfgs3 = [] ∧ ibT3 ≠ [[]] ∧
pcOf cfg4 < 14 ∧ cfgs4 = [] ∧ ibT4 ≠ [[]] ∧
ibUT3 ≠ [[]] ∧ ibUT4 ≠ [[]]"
unfolding Δ1_defs apply clarify
by (metis atLeastAtMost_iff eval_nat_numeral(2) infinity_ne_i0
less_Suc_eq_le list.map_disc_iff llength_LNil semiring_norm(28))
definition Δ1' :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δ1' = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ∧
same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
whileSpeculation cfg3 (last cfgs3) ∧
misSpecL1 cfgs3 ∧ misSpecL1 cfgs4 ∧
w1 = ∞
))"
lemmas Δ1'_defs = Δ1'_def common_def PC_def same_var_def
startOfIfThen_def startOfElseBranch_def
misSpecL1_def whileSpec_defs
lemma Δ1'_implies: "Δ1' num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf cfg3 < 14 ∧ pcOf cfg4 < 14 ∧
whileSpeculation cfg3 (last cfgs3) ∧
whileSpeculation cfg4 (last cfgs4) ∧
length cfgs3 = Suc 0 ∧ length cfgs4 = Suc 0"
unfolding Δ1'_defs by clarsimp
definition Δ2 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δ2 = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ∧
same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
pcOf cfg3 = startOfIfThen ∧ pcOf (last cfgs3) ∈ inElseIf ∧
misSpecL1 cfgs3 ∧ misSpecL1 cfgs4 ∧
(pcOf (last cfgs3) = startOfElseBranch ⟶ w1 = ∞) ∧
(pcOf (last cfgs3) = 3 ⟶ w1 = 3) ∧
(pcOf (last cfgs3) = startOfWhileThen ∨
pcOf (last cfgs3) = whileElse ⟶ w1 = 1)
))"
lemmas Δ2_defs = Δ2_def common_def PC_def same_var_o_def misSpecL1_def
startOfIfThen_def inElseIf_def same_var_def
startOfWhileThen_def whileElse_def startOfElseBranch_def
lemma Δ2_implies: "Δ2 num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf (last cfgs3) ∈ inElseIf ∧ pcOf cfg3 = 7 ∧
pcOf (last cfgs4) = pcOf (last cfgs3) ∧
pcOf cfg4 = pcOf cfg3 ∧ length cfgs3 = Suc 0 ∧
length cfgs4 = Suc 0 ∧ same_var xx (last cfgs3) (last cfgs4)"
apply(intro conjI)
unfolding Δ2_defs
apply (simp_all add: image_subset_iff)
by (metis last_in_set length_0_conv Nil_is_map_conv last_map length_map)+
definition Δ2' :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δ2' = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ∧
same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
pcOf cfg3 = startOfIfThen ∧
whileSpeculation (cfgs3!0) (last cfgs3) ∧
misSpecL2 cfgs3 ∧ misSpecL2 cfgs4 ∧
w1 = 2
))"
lemmas Δ2'_defs = Δ2'_def common_def PC_def same_var_def
startOfElseBranch_def startOfIfThen_def
whileSpec_defs misSpecL2_def
lemma Δ2'_implies: "Δ2' num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf cfg3 = 7 ∧ pcOf cfg4 = 7 ∧
whileSpeculation (cfgs3!0) (last cfgs3) ∧
whileSpeculation (cfgs4!0) (last cfgs4) ∧
length cfgs3 = 2 ∧ length cfgs4 = 2"
apply(intro conjI)
unfolding Δ2'_defs apply (simp add: lessI, clarify)
apply linarith+ apply simp_all
by (metis list.inject map_L2)
definition Δ3 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δ3 = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO.
(common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ∧
same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
pcOf cfg3 = startOfElseBranch ∧ pcOf (last cfgs3) ∈ inThenIfBeforeOutput ∧
misSpecL1 cfgs3 ∧
(pcOf (last cfgs3) = 7 ⟶ w1 = ∞) ∧
(pcOf (last cfgs3) = 8 ⟶ w1 = 2) ∧
(pcOf (last cfgs3) = 9 ⟶ w1 = 1)
))"
lemmas Δ3_defs = Δ3_def common_def PC_def same_var_o_def
startOfElseBranch_def inThenIfBeforeOutput_def
lemma Δ3_implies: "Δ3 num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
(pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)
statA
(cfg1,ibT1,ibUT1,ls1)
(cfg2,ibT2,ibUT2,ls2)
statO ⟹
pcOf (last cfgs3) ∈ inThenIfBeforeOutput ∧
pcOf (last cfgs4) = pcOf (last cfgs3) ∧
pcOf cfg3 = 12 ∧ pcOf cfg3 = pcOf cfg4 ∧
length cfgs3 = Suc 0 ∧ length cfgs4 = Suc 0"
apply(intro conjI)
unfolding Δ3_defs
apply (simp_all add: image_subset_iff)
by (metis last_map map_is_Nil_conv length_map)+
definition Δe :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where
"Δe = (λnum w1 w2 (pstate3,cfg3,cfgs3,ib3,ls3)
(pstate4,cfg4,cfgs4,ib4,ls4)
statA
(cfg1,ib1,ls1)
(cfg2,ib2,ls2)
statO.
(pcOf cfg3 = endPC ∧ pcOf cfg4 = endPC ∧ cfgs3 = [] ∧ cfgs4 = [] ∧
pcOf cfg1 = endPC ∧ pcOf cfg2 = endPC))"
lemmas Δe_defs = Δe_def common_def endPC_def
lemma init: "initCond Δ0"
unfolding initCond_def apply safe
subgoal for pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3
pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4
unfolding istateO.simps apply clarsimp
apply(cases "getAvstore (stateOf cfg3)", cases "getAvstore (stateOf cfg4)")
unfolding Δ0_defs
unfolding array_base_def by auto .
lemma step0: "unwindIntoCond Δ0 (oor Δ0 Δ1)"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δ0: "Δ0 n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases cfg3) (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases cfg4) (metis state.collapse vstore.collapse)
note cfg = cfg3 cfg4
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
have f1:"¬finalN ss1"
using Δ0 unfolding ss
apply-by(frule Δ0_implies, simp)
have f2:"¬finalN ss2"
using Δ0 unfolding ss
apply-by(frule Δ0_implies, simp)
have f3:"¬finalS ss3"
using Δ0 unfolding ss
apply-apply(frule Δ0_implies, unfold Δ0_defs)
using finalS_cond' by simp
have f4:"¬finalS ss4"
using Δ0 unfolding ss
apply-apply(frule Δ0_implies, unfold Δ0_defs)
using finalS_cond' by simp
note finals = f1 f2 f3 f4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using finals by auto
then show "isIntO ss3 = isIntO ss4" by simp
show "react (oor Δ0 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 (oor Δ0 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 (oor Δ0 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 (oor Δ0 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
proof(rule match12_simpleI,rule disjI2, intro conjI)
fix ss3' ss4' statA'
assume statA': "statA' = sstatA' statA ss3 ss4"
and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')"
and sa: "Opt.eqAct ss3 ss4"
note v3 = v(1) note v4 = v(2)
obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
by (cases ss3', auto)
obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
by (cases ss4', auto)
note ss = ss ss3' ss4'
obtain pc3 vs3 avst3 h3 p3 where
cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases cfg3) (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases cfg4) (metis state.collapse vstore.collapse)
note cfg = cfg3 cfg4
show "eqSec ss1 ss3"
using v sa Δ0 finals unfolding ss
by (simp add: Δ0_defs eqSec_def)
show "eqSec ss2 ss4"
using v sa Δ0 finals unfolding ss
by (simp add: Δ0_defs eqSec_def, metis map_is_Nil_conv)
show "Van.eqAct ss1 ss2"
using v sa Δ0 unfolding ss
apply-apply(frule Δ0_implies)
unfolding Opt.eqAct_def
Van.eqAct_def
by(simp_all add: Δ0_defs, linarith)
show "match12_12 (oor Δ0 Δ1) ∞ ∞ ss3' ss4' statA' ss1 ss2 statO"
unfolding match12_12_def
proof(rule exI[of _ "nextN ss1"], rule exI[of _ "nextN ss2"],unfold Let_def, intro conjI impI)
show "validTransV (ss1, nextN ss1)"
by (simp add: f1 nextN_stepN)
show "validTransV (ss2, nextN ss2)"
by (simp add: f2 nextN_stepN)
{assume sstat: "statA' = Diff"
show "sstatO' statO ss1 ss2 = Diff"
using v sa Δ0 sstat unfolding ss cfg statA' apply simp
apply(simp add: Δ0_defs sstatO'_def sstatA'_def finalS_def final_def)
using cases_14[of pc3] apply(elim disjE)
apply simp_all apply(cases statO, simp_all) apply(cases statA, simp_all)
apply(cases statO, simp_all) apply (cases statA, simp_all)
by (smt (z3) status.distinct status.exhaust newStat.simps)+
} note stat = this
show "oor Δ0 Δ1 ∞ ∞ ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
case nonspec_mispred
then show ?thesis using sa Δ0 stat unfolding ss
by (simp add: Δ0_defs numeral_1_eq_Suc_0, linarith)
next
case spec_normal
then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
next
case spec_mispred
then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
next
case spec_Fence
then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
next
case spec_resolve
then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
next
case nonspec_normal note nn3 = nonspec_normal
show ?thesis
using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
case nonspec_mispred
then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
next
case spec_normal
then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
next
case spec_mispred
then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
next
case spec_Fence
then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
next
case spec_resolve
then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
next
case nonspec_normal note nn4 = nonspec_normal
show ?thesis using sa Δ0 stat v3 v4 nn3 nn4 unfolding ss cfg apply clarsimp
apply(unfold Δ0_defs, clarsimp, elim disjE)
subgoal by(rule oorI1, auto simp add: Δ0_defs)
subgoal by (rule oorI1, simp add: Δ0_defs)
subgoal by (rule oorI2, simp add: Δ1_defs) .
qed
qed
qed
qed
qed
qed
lemma step1: "unwindIntoCond Δ1 (oor5 Δ1 Δ1' Δ2 Δ3 Δe)"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δ1: "Δ1 n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases cfg3) (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases cfg4) (metis state.collapse vstore.collapse)
note cfg = cfg3 cfg4
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
have f1:"¬finalN ss1"
using Δ1 unfolding ss Δ1_def apply clarify
apply(frule common_implies)
using finalB_pcOf_iff finalN_iff_finalB nat_less_le by metis
have f2:"¬finalN ss2"
using Δ1 unfolding ss Δ1_def apply clarify
apply(frule common_implies)
using finalB_pcOf_iff finalN_iff_finalB nat_less_le by metis
have f3:"¬finalS ss3"
using Δ1 unfolding ss
apply-apply(frule Δ1_implies)
by (simp add: finalS_cond')
have f4:"¬finalS ss4"
using Δ1 unfolding ss
apply-apply(frule Δ1_implies)
by (simp add: finalS_cond')
note finals = f1 f2 f3 f4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using finals by auto
then show "isIntO ss3 = isIntO ss4" by simp
show "react (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
proof(rule match12_simpleI,rule disjI2, intro conjI)
fix ss3' ss4' statA'
assume statA': "statA' = sstatA' statA ss3 ss4"
and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')"
and sa: "Opt.eqAct ss3 ss4"
note v3 = v(1) note v4 = v(2)
obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
by (cases ss3', auto)
obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
by (cases ss4', auto)
note ss = ss ss3' ss4'
show "eqSec ss1 ss3"
using v sa Δ1 finals unfolding ss by (simp add: Δ1_defs eqSec_def)
show "eqSec ss2 ss4"
using v sa Δ1 finals unfolding ss
by (simp add: Δ1_defs eqSec_def, metis map_is_Nil_conv)
show "Van.eqAct ss1 ss2"
using v sa Δ1 unfolding ss apply- apply(frule Δ1_implies)
unfolding Opt.eqAct_def Van.eqAct_def
apply(simp_all add: Δ1_defs)
by (metis f3 getActO_pcOf numeral_eq_iff numeral_less_iff semiring_norm(77,78,81,89) ss3)
show "match12_12 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) ∞ ∞ ss3' ss4' statA' ss1 ss2 statO"
unfolding match12_12_def
proof(rule exI[of _ "nextN ss1"], rule exI[of _ "nextN ss2"],unfold Let_def, intro conjI impI)
show "validTransV (ss1, nextN ss1)"
by (simp add: f1 nextN_stepN)
show "validTransV (ss2, nextN ss2)"
by (simp add: f2 nextN_stepN)
{assume sstat: "statA' = Diff"
show "sstatO' statO ss1 ss2 = Diff"
using v sa Δ1 sstat finals unfolding ss cfg statA'
apply-apply(frule Δ1_implies)
apply(simp add: Δ1_defs sstatO'_def sstatA'_def newStat_EqI)
using cases_14[of pc3] apply(elim disjE, simp_all)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all, cases statA)
by (simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all)
by(cases statA, simp_all add: newStat_EqI)
subgoal apply(cases statO, simp_all, cases statA)
by (simp_all add: newStat_EqI split: if_splits)
subgoal apply(cases statO, simp_all, cases statA)
by (simp_all add: newStat_EqI split: if_splits)
subgoal apply(cases statO, simp_all, cases statA)
by (simp_all add: newStat_EqI split: if_splits) .
} note stat = this
show "oor5 Δ1 Δ1' Δ2 Δ3 Δe ∞ ∞ ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
case spec_normal
then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs)
next
case spec_mispred
then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs)
next
case spec_Fence
then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs)
next
case spec_resolve
then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs)
next
case nonspec_normal note nn3 = nonspec_normal
show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
case nonspec_mispred
then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs)
next
case spec_normal
then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs)
next
case spec_mispred
then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs)
next
case spec_Fence
then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs)
next
case spec_resolve
then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs)
next
case nonspec_normal note nn4 = nonspec_normal
then show ?thesis using sa Δ1 stat v3 v4 nn3 nn4 f4 unfolding ss cfg Opt.eqAct_def
apply clarsimp using cases_14[of pc3] apply(elim disjE)
subgoal by (simp add: Δ1_defs)
subgoal by (simp add: Δ1_defs)
subgoal by (simp add: Δ1_defs)
subgoal using xx_0_cases[of vs3] apply(elim disjE)
subgoal by(rule oor5I1, auto simp add: Δ1_defs)
subgoal by(rule oor5I1, auto simp add: Δ1_defs) .
subgoal apply(rule oor5I1) by (auto simp add: Δ1_defs)
subgoal apply(rule oor5I1) by (auto simp add: Δ1_defs)
subgoal using xx_NN_cases[of vs3] apply(elim disjE)
subgoal by(rule oor5I1, auto simp add: Δ1_defs)
subgoal by(rule oor5I1, auto simp add: Δ1_defs) .
subgoal by(rule oor5I1, auto simp add: Δ1_defs hh)
subgoal by(rule oor5I1, auto simp add: Δ1_defs)
subgoal by(rule oor5I1, auto simp add: Δ1_defs hh)
subgoal by(rule oor5I1, auto simp add: Δ1_defs hh)
subgoal by(rule oor5I1, auto simp add: Δ1_defs)
subgoal by(rule oor5I1, auto simp add: Δ1_defs)
by(rule oor5I5, simp_all add: Δ1_defs Δe_defs)
qed
next
case nonspec_mispred note nm3 = nonspec_mispred
show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs)
next
case spec_normal
then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs)
next
case spec_mispred
then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs)
next
case spec_Fence
then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs)
next
case spec_resolve
then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs)
next
case nonspec_mispred note nm4 = nonspec_mispred
then show ?thesis using sa Δ1 stat v3 v4 nm3 nm4 unfolding ss cfg apply clarsimp
using cases_14[of pc3] apply(elim disjE)
prefer 4 subgoal using xx_0_cases[of vs3] apply(elim disjE)
subgoal by(rule oor5I2, auto simp add: Δ1_defs Δ1'_defs)
subgoal by(rule oor5I2, auto simp add: Δ1_defs Δ1'_defs) .
prefer 6 subgoal using xx_NN_cases[of vs3] apply(elim disjE)
subgoal apply(rule oor5I3) by (auto simp add: Δ1_defs Δ2_defs)
subgoal apply(rule oor5I4) by (auto simp add: Δ1_defs Δ3_defs) .
by (simp_all add: Δ1_defs)
qed
qed
qed
qed
qed
qed
lemma step2: "unwindIntoCond Δ2 (oor3 Δ2 Δ2' Δ1)"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δ2: "Δ2 n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
lcfgs3: "last cfgs3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases "last cfgs3") (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
lcfgs4: "last cfgs4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases "last cfgs4") (metis state.collapse vstore.collapse)
note lcfgs = lcfgs3 lcfgs4
have f1:"¬finalN ss1"
using Δ2 unfolding ss Δ2_def
apply clarsimp
by(frule common_implies, simp)
have f2:"¬finalN ss2"
using Δ2 unfolding ss Δ2_def
apply clarsimp
by(frule common_implies, simp)
have f3:"¬finalS ss3"
using Δ2 unfolding ss
apply-apply(frule Δ2_implies)
by (simp add: finalS_if_spec)
have f4:"¬finalS ss4"
using Δ2 unfolding ss
apply-apply(frule Δ2_implies)
by (simp add: finalS_if_spec)
note finals = f1 f2 f3 f4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using finals by auto
then show "isIntO ss3 = isIntO ss4" by simp
then have lpc3:"pcOf (last cfgs3) = 12 ∨
pcOf (last cfgs3) = 3 ∨
pcOf (last cfgs3) = 4 ∨
pcOf (last cfgs3) = 13"
using Δ2 unfolding ss Δ2_defs by simp
have sec3[simp]:"¬ isSecO ss3"
using Δ2 finals unfolding ss isSecO_def
by(simp add: Δ2_defs, metis list.size(3) n_not_Suc_n)
have sec4[simp]:"¬ isSecO ss4"
using Δ2 unfolding ss
by (simp add: Δ2_defs, metis list.size(3) n_not_Suc_n)
have stat[simp]:"⋀s3' s4' statA'. statA' = sstatA' statA ss3 ss4 ⟹
validTransO (ss3, s3') ⟹ validTransO (ss4, s4') ⟹
(statA = statA' ∨ statO = Diff)"
subgoal for ss3' ss4'
apply (cases ss3, cases ss4, cases ss1, cases ss2)
apply (cases ss3', cases ss4', clarsimp)
using Δ2 finals unfolding ss apply clarsimp
apply(simp_all add: Δ2_defs sstatA'_def)
apply(cases statO, simp_all) by (cases statA, simp_all add: newStat_EqI) .
have xx:"vs3 xx = vs4 xx" using Δ2 lcfgs unfolding ss Δ2_defs apply clarsimp
by (metis cfgs_Suc_zero config.sel(2) list.set_intros(1) state.sel(1) vstore.sel)
have oor3_rule:"⋀ss3' ss4'. ss3 →S ss3' ⟹ ss4 →S ss4' ⟹
(pcOf (last cfgs3) = 12 ⟶ oor3 Δ2 Δ2' Δ1 ∞ 3 3 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)
∧ (pcOf (last cfgs3) = 3 ∧ mispred pstate4 [7, 3] ⟶ oor3 Δ2 Δ2' Δ1 ∞ 2 2 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)
∧ (pcOf (last cfgs3) = 3 ∧ ¬mispred pstate4 [7, 3] ⟶ oor3 Δ2 Δ2' Δ1 ∞ 1 1 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)
∧ ((pcOf (last cfgs3) = 4 ∨ pcOf (last cfgs3) = 13) ⟶ oor3 Δ2 Δ2' Δ1 ∞ 0 0 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO) ⟹
∃w1'<w1. ∃w2'<w2. oor3 Δ2 Δ2' Δ1 ∞ w1' w2' ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO"
subgoal for ss3' ss4' apply(cases ss3', cases ss4')
subgoal for pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3'
pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4'
subgoal premises p using lpc3 apply-apply(erule disjE)
subgoal apply(intro exI[of _ 3], intro conjI)
subgoal using Δ2 unfolding ss Δ2_defs apply clarify
by (metis enat_ord_simps(4) numeral_ne_infinity)
apply(intro exI[of _ 3], rule conjI)
subgoal using Δ2 unfolding ss Δ2_defs apply clarify
by (metis enat_ord_simps(4) numeral_ne_infinity)
using p by (simp add: p)
apply(erule disjE)
subgoal apply(cases "mispred pstate4 [7, 3]")
subgoal apply(intro exI[of _ 2], intro conjI)
using Δ2 unfolding ss Δ2_defs apply clarify
apply (metis enat_ord_number(2) eval_nat_numeral(3) lessI)
apply(intro exI[of _ 2], rule conjI)
using Δ2 unfolding ss Δ2_defs apply clarify
apply (metis enat_ord_number(2) eval_nat_numeral(3) lessI)
using Δ2 p unfolding ss Δ2_defs by clarify
subgoal apply(intro exI[of _ 1], intro conjI)
using Δ2 unfolding ss Δ2_defs apply clarify
apply (metis one_less_numeral_iff semiring_norm(77))
apply(intro exI[of _ 1], rule conjI)
using Δ2 unfolding ss Δ2_defs apply clarify
apply (metis one_less_numeral_iff semiring_norm(77))
using Δ2 p unfolding ss Δ2_defs by clarify .
subgoal apply(intro exI[of _ 0], intro conjI)
using Δ2 unfolding ss Δ2_defs apply clarify
apply (metis less_numeral_extra(1))
apply(intro exI[of _ 0], rule conjI)
using Δ2 unfolding ss Δ2_defs apply clarify
apply (metis less_numeral_extra(1))
using Δ2 p unfolding ss Δ2_defs by clarify . . . .
show "react (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
apply(rule match12_simpleI, simp_all, rule disjI1)
subgoal for ss3' ss4' apply(cases ss3', cases ss4')
subgoal for pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3'
pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4'
apply-apply(rule oor3_rule, assumption+, intro conjI impI)
subgoal premises prem using prem(1)[unfolded ss prem(4)]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs)
next
case spec_mispred
then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs)
next
case spec_Fence
then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs)
next
case spec_resolve
then show ?thesis
using Δ2 prem(6) unfolding ss apply (simp add: Δ2_defs, clarsimp)
by (meson doubleton_eq_iff numeral_eq_iff semiring_norm(89) semiring_norm(90))
next
case spec_normal note sn3 = spec_normal
show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs)
next
case spec_Fence
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_resolve
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_mispred
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_normal note sn4 = spec_normal
have pc4:"pc4 = 12" using Δ2 prem lcfgs unfolding ss Δ2_defs by auto
show ?thesis
using Δ2 prem sn3 sn4 finals stat unfolding ss prem(4,5) lcfgs
apply-apply(frule Δ2_implies, unfold Δ2_defs) apply clarsimp
apply(rule oor3I1) apply(simp_all add: Δ2_defs pc4)
using final_def config.sel(2) last_in_set
lcfgs state.sel(1,2) vstore.sel xx
by (metis (mono_tags, lifting))
qed
qed
subgoal premises prem using prem(1)[unfolded ss prem(4)]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs)
next
case spec_Fence
then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs)
next
case spec_normal
then show ?thesis using stat Δ2 prem unfolding ss by (simp add: Δ2_defs, metis cfgs_map)
next
case spec_resolve
then show ?thesis
using Δ2 prem(6) resolve_73
unfolding ss Δ2_defs using cfgs_map misSpecL1_def
by (clarify,smt (z3) insert_commute list.simps(15) resolve.simps)
next
case spec_mispred note sm3 = spec_mispred
show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs)
next
case spec_resolve
then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_Fence
then show ?thesis using sm3 Δ2 unfolding ss apply-apply(frule Δ2_implies)
by (simp add: Δ2_defs)
next
case spec_normal
then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_mispred note sm4 = spec_mispred
have pc:"pc4 = 3"
using prem(6) lcfgs Δ2 unfolding ss apply-apply(frule Δ2_implies)
by (simp add: Δ2_defs )
show ?thesis apply(rule oor3I2)
unfolding ss Δ2'_def using xx_0_cases[of vs3] apply(elim disjE)
subgoal using Δ2 lcfgs prem pc sm3 sm4 xx finals stat unfolding ss
apply- apply(simp add: Δ2_defs Δ2'_defs, clarify)
apply(intro conjI)
subgoal by (metis config.sel(2) last_in_set state.sel(1,2) vstore.sel final_def)
subgoal by (metis config.sel(2) last_in_set state.sel(2))
subgoal by (metis config.sel(2) last_in_set state.sel(2))
subgoal by (metis config.sel(2) last_in_set state.sel(2))
subgoal by (smt(verit) prem(1) prem(2) ss)
subgoal by (metis config.sel(2) last_in_set state.sel(1) vstore.sel) .
subgoal using Δ2 lcfgs prem pc sm3 sm4 xx finals stat unfolding ss
apply- apply(simp add: Δ2_defs Δ2'_defs, clarify)
apply(intro conjI)
subgoal by (metis config.sel(2) last_in_set state.sel(1,2) vstore.sel final_def)
subgoal by (metis config.sel(2) last_in_set state.sel(2))
subgoal by (metis config.sel(2) last_in_set state.sel(2))
subgoal by (metis config.sel(2) last_in_set state.sel(2))
subgoal by (smt(verit) prem(1) prem(2) ss)
subgoal by (metis config.sel(2) last_in_set state.sel(1) vstore.sel) . .
qed
qed
subgoal premises prem using prem(1)[unfolded ss prem(4)]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs)
next
case spec_Fence
then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs)
next
case spec_mispred
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case spec_resolve
then show ?thesis
using Δ2 prem(6) resolve_73
unfolding ss Δ2_defs using cfgs_map misSpecL1_def
by (clarify,smt (z3) insert_commute list.simps(15) resolve.simps)
next
case spec_normal note sn3 = spec_normal
show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs)
next
case spec_Fence
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_resolve
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_mispred
then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
next
case spec_normal note sn4 = spec_normal
show ?thesis
using Δ2 lcfgs prem sn3 sn4 finals unfolding ss
apply-apply(frule Δ2_implies, unfold Δ2_defs) apply clarsimp
apply(rule oor3I1)
using xx_0_cases[of vs3] apply(elim disjE)
subgoal apply(simp_all add: Δ2_defs, clarify)
using config.sel(2) last_in_set stat state.sel(1,2) vstore.sel
by (smt (verit, ccfv_SIG) Opt.final_def config.sel(1) eval_nat_numeral(3) f3 f4 is_Output_1 le_imp_less_Suc le_refl nat_less_le ss)
subgoal apply(simp_all add: Δ2_defs, clarify)
using config.sel(2) last_in_set stat state.sel(1,2) vstore.sel
apply(intro conjI,unfold config.sel(1))
subgoal by simp
subgoal by simp
subgoal by (metis array_baseSimp)
subgoal by (metis array_baseSimp)
subgoal by (metis array_baseSimp)
subgoal by (metis array_baseSimp)
subgoal by (smt (verit) Opt.final_def ss)
apply (smt (verit) cfgs_Suc_zero lcfgs list.set_intros(1))
apply (smt (verit) cfgs_Suc_zero lcfgs list.set_intros(1))
apply presburger
apply (smt (verit) insertCI list.simps(15) resolve.elims(3) resolve_74 resolve_127)
by linarith .
qed
qed
subgoal premises prem using prem(1)[unfolded ss prem(4)]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs)
next
case spec_Fence
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case spec_mispred
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case spec_normal
then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)
next
case spec_resolve note sr3 = spec_resolve
show ?thesis using prem(2)[unfolded ss prem(5)] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
next
case spec_normal
then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs, metis)
next
case spec_mispred
then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs, metis)
next
case spec_Fence
then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs, metis)
next
case spec_resolve note sr4 = spec_resolve
show ?thesis using stat Δ2 prem sr3 sr4
unfolding ss lcfgs apply-
apply(frule Δ2_implies) apply (simp add: Δ2_defs Δ1_defs)
apply(rule oor3I3, simp add: Δ1_defs)
by (metis prem(1) prem(2) ss)
qed
qed. . .
qed
qed
lemma step3: "unwindIntoCond Δ3 (oor Δ3 Δ1)"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δ3: "Δ3 n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
lcfgs3: "last cfgs3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases "last cfgs3") (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
lcfgs4: "last cfgs4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases "last cfgs4") (metis state.collapse vstore.collapse)
note lcfgs = lcfgs3 lcfgs4
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
have f1:"¬finalN ss1"
using Δ3 unfolding ss Δ3_def
apply clarsimp
by(frule common_implies, simp)
have f2:"¬finalN ss2"
using Δ3 unfolding ss Δ3_def
apply clarsimp
by(frule common_implies, simp)
have f3:"¬finalS ss3"
using Δ3 unfolding ss
apply-apply(frule Δ3_implies)
using finalS_if_spec by force
have f4:"¬finalS ss4"
using Δ3 unfolding ss
apply-apply(frule Δ3_implies)
using finalS_if_spec by force
note finals = f1 f2 f3 f4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using finals by auto
then show "isIntO ss3 = isIntO ss4" by simp
then have lpc3:"pcOf (last cfgs3) = 7 ∨
pcOf (last cfgs3) = 8"
using Δ3 unfolding ss Δ3_defs by simp
have sec3[simp]:"¬ isSecO ss3"
using Δ3 unfolding ss by (simp add: Δ3_defs, metis list.size(3) n_not_Suc_n)
have sec4[simp]:"¬ isSecO ss4"
using Δ3 unfolding ss
by (simp add: Δ3_defs, metis list.size(3) map_is_Nil_conv nat.distinct(1))
have stat[simp]:"⋀s3' s4' statA'. statA' = sstatA' statA ss3 ss4 ⟹
validTransO (ss3, s3') ⟹ validTransO (ss4, s4') ⟹
(statA = statA' ∨ statO = Diff)"
subgoal for ss3' ss4'
apply (cases ss3, cases ss4, cases ss1, cases ss2)
apply (cases ss3', cases ss4', clarsimp)
using Δ3 finals unfolding ss apply clarsimp
apply(simp_all add: Δ3_defs sstatA'_def)
apply(cases statO, simp_all) by (cases statA, simp_all add: newStat_EqI) .
have "vs3 xx = vs4 xx" using Δ3 lcfgs unfolding ss Δ3_defs apply clarsimp
by (metis cfgs_Suc_zero config.sel(2) list.set_intros(1) state.sel(1) vstore.sel)
then have a1x:"(array_loc aa1 (nat (vs4 xx)) avst4) =
(array_loc aa1 (nat (vs3 xx)) avst3)"
using Δ3 lcfgs unfolding ss Δ3_defs array_loc_def apply clarsimp
by (metis Zero_not_Suc config.sel(2) last_in_set list.size(3) state.sel(2))
have oor2_rule:"⋀ss3' ss4'. ss3 →S ss3' ⟹ ss4 →S ss4' ⟹
(pcOf (last cfgs3) = 7 ⟶ oor Δ3 Δ1 ∞ 2 2 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)
∧ (pcOf (last cfgs3) = 8 ⟶ oor Δ3 Δ1 ∞ 1 1 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)⟹
∃w1'<w1. ∃w2'<w2. oor Δ3 Δ1 ∞ w1' w2' ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO"
subgoal for ss3' ss4' apply(cases ss3', cases ss4')
subgoal for pstate3' cfg3' cfgs3' ib3' ls3'
pstate4' cfg4' cfgs4' ib4' ls4'
using lpc3 apply(elim disjE)
subgoal apply(intro exI[of _ 2], intro conjI)
subgoal using Δ3 unfolding ss Δ3_defs apply clarify
by (metis enat_ord_simps(4) numeral_ne_infinity)
apply(intro exI[of _ 2], rule conjI)
subgoal using Δ3 unfolding ss Δ3_defs apply clarify
by (metis enat_ord_simps(4) numeral_ne_infinity)
by simp
subgoal apply(intro exI[of _ 1], intro conjI)
subgoal using Δ3 unfolding ss Δ3_defs apply clarify
by (metis one_less_numeral_iff semiring_norm(76))
apply(intro exI[of _ 1], rule conjI)
subgoal using Δ3 unfolding ss Δ3_defs apply clarify
by (metis one_less_numeral_iff semiring_norm(76))
by simp . . .
show "react (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
apply(rule match12_simpleI, simp_all, rule disjI1)
subgoal for ss3' ss4' apply(cases ss3', cases ss4')
subgoal for pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3'
pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4'
apply-apply(rule oor2_rule, assumption+, intro conjI impI)
subgoal premises prem using prem(1)[unfolded ss prem(4)]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs)
next
case spec_mispred
then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs)
next
case spec_resolve
then show ?thesis
using Δ3 prem(6) resolve_127
unfolding ss Δ3_defs by (clarify,metis cfgs_map misSpecL1_def)
next
case spec_Fence
then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs)
next
case spec_normal note sn3 = spec_normal
show ?thesis
using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs)
next
case spec_mispred
then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs, metis config.sel(1) last_map)
next
case spec_Fence
then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss
by (simp add: Δ3_defs, metis config.sel(1) last_map)
next
case spec_resolve
then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs)
next
case spec_normal note sn4 = spec_normal
show ?thesis
apply(intro oorI1)
unfolding ss Δ3_def prem(4,5) apply- apply(clarify,intro conjI)
subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss hh
apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs)
using cases_14[of pc3] apply simp apply(elim disjE)
apply simp_all by (metis config.sel(2) last_in_set state.sel(2) Dist_ignore a1x )+
subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss prem(4,5) hh
apply- apply(frule Δ3_implies) apply(simp_all add: Δ3_defs)
using cases_14[of pc3] apply simp apply(elim disjE)
apply simp_all
by (metis config.collapse config.inject last_in_set state.sel(1) vstore.sel)+
subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss prem(4,5) hh
apply- apply(frule Δ3_implies) by(simp add: Δ3_defs)
subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss hh
apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs)
using cases_14[of pc3] apply simp apply(elim disjE)
by simp_all
subgoal using stat Δ3 lcfgs sn3 sn4 unfolding ss hh
apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs)
using cases_14[of pc3] apply (simp add: array_loc_def) apply(elim disjE)
by (simp_all add: array_loc_def)
subgoal using stat Δ3 lcfgs sn3 sn4 unfolding ss hh
apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs)
using cases_14[of pc3] apply (simp add: array_loc_def) apply(elim disjE)
by (simp_all add: array_loc_def)
subgoal using stat Δ3 lcfgs sn3 sn4 unfolding ss hh
apply- apply(frule Δ3_implies) by(simp add: Δ3_defs)
subgoal using stat Δ3 lcfgs sn3 sn4 prem(6) unfolding ss hh
apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) .
qed
qed
subgoal premises prem using prem(1)[unfolded ss prem(4)]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs)
next
case spec_mispred
then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs)
next
case spec_Fence
then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs)
next
case spec_normal
then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs)
next
case spec_resolve note sr3 = spec_resolve
show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ3 lcfgs sr3 unfolding ss by (simp add: Δ3_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ3 lcfgs sr3 unfolding ss by (simp add: Δ3_defs)
next
case spec_mispred
then show ?thesis using stat Δ3 lcfgs sr3 unfolding ss by (simp add: Δ3_defs)
next
case spec_Fence
then show ?thesis using stat Δ3 lcfgs sr3 unfolding ss by (simp add: Δ3_defs)
next
case spec_normal
then show ?thesis using stat Δ3 lcfgs sr3 unfolding ss by (simp add: Δ3_defs)
next
case spec_resolve note sr4 = spec_normal
show ?thesis using stat Δ3 prem sr3 sr4
unfolding ss lcfgs apply-
apply(frule Δ3_implies) apply (simp add: Δ3_defs Δ1_defs)
apply(rule oorI2, simp add: Δ1_defs local.spec_resolve)
by (metis prem(1) ss3)
qed qed . . .
qed
qed
lemma step4: "unwindIntoCond Δ1' Δ1"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δ1': "Δ1' n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases cfg3) (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases cfg4) (metis state.collapse vstore.collapse)
note cfg = cfg3 cfg4
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
have f1:"¬finalN ss1"
using Δ1' unfolding ss Δ1'_def
apply clarsimp
by(frule common_implies, simp)
have f2:"¬finalN ss2"
using Δ1' unfolding ss Δ1'_def
apply clarsimp
by(frule common_implies, simp)
have f3:"¬finalS ss3"
using Δ1' unfolding ss
apply-apply(frule Δ1'_implies)
by (simp add: finalS_while_spec)
have f4:"¬finalS ss4"
using Δ1' unfolding ss
apply-apply(frule Δ1'_implies)
by (simp add: finalS_while_spec)
note finals = f1 f2 f3 f4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using finals by auto
then show "isIntO ss3 = isIntO ss4" by simp
have match12_aux:"
(⋀s1' s2' statA'.
statA' = sstatA' statA ss3 ss4 ⟹
validTransO (ss3, s1') ⟹
validTransO (ss4, s2') ⟹
Opt.eqAct ss3 ss4 ⟹
(¬ isSecO ss3 ∧ ¬ isSecO ss4 ∧
(statA = statA' ∨ statO = Diff) ∧
Δ1 ∞ 1 1 s1' s2' statA' ss1 ss2 statO))
⟹ match12 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
apply(rule match12_simpleI, rule disjI1)
apply(rule exI[of _ 1], rule conjI)
subgoal using Δ1' unfolding ss Δ1'_defs apply clarify
by(metis enat_ord_simps(4) infinity_ne_i1)
apply(rule exI[of _ 1], rule conjI)
subgoal using Δ1' unfolding ss Δ1'_defs apply clarify
by(metis enat_ord_simps(4) infinity_ne_i1)
by auto
show "react Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
proof(rule match12_aux, intro conjI)
fix ss3' ss4' statA'
assume statA': "statA' = sstatA' statA ss3 ss4"
and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')"
and sa: "Opt.eqAct ss3 ss4"
note v3 = v(1) note v4 = v(2)
obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
by (cases ss3', auto)
obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
by (cases ss4', auto)
note ss = ss ss3' ss4'
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
show "¬ isSecO ss3"
using v sa Δ1' unfolding ss
by (simp add: Δ1'_defs,metis list.size(3) n_not_Suc_n)
show "¬ isSecO ss4"
using v sa Δ1' unfolding ss
by (simp add: Δ1'_defs,metis list.size(3) n_not_Suc_n)
show stat: "statA = statA' ∨ statO = Diff"
using v sa Δ1'
apply (cases ss3, cases ss4, cases ss1, cases ss2)
apply (cases ss3', cases ss4', clarsimp)
using v sa Δ1' unfolding ss statA' apply clarsimp
apply(simp_all add: Δ1'_defs sstatA'_def)
apply(cases statO, simp_all)
apply(cases statA, simp_all add: newStat_EqI)
unfolding finalS_def final_def
using One_nat_def less_numeral_extra(4)
less_one list.size(3) map_is_Nil_conv
by (smt (verit) status.exhaust newStat.simps)
show "Δ1 ∞ 1 1 ss3' ss4' statA' ss1 ss2 statO"
using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs)
next
case nonspec_mispred
then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs)
next
case spec_Fence
then show ?thesis using sa Δ1' unfolding ss
apply (simp add: Δ1'_defs, clarify, elim disjE)
by (simp_all add: Δ1_defs Δ1'_defs)
next
case spec_mispred
then show ?thesis using sa Δ1' unfolding ss
apply (simp add: Δ1'_defs, clarify, elim disjE)
by (simp_all add: Δ1_defs Δ1'_defs)
next
case spec_normal note sn3 = spec_normal
show ?thesis using Δ1' sn3(2) unfolding ss
apply (simp add: Δ1'_defs, clarsimp)
by (smt (z3) insert_commute)
next
case spec_resolve note sr3 = spec_resolve
show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs)
next
case nonspec_mispred
then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs)
next
case spec_mispred
then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs, metis)
next
case spec_normal
then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs, metis)
next
case spec_Fence
then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs, metis)
next
case spec_resolve note sr4 = spec_resolve
show ?thesis
using sa stat Δ1' v3 v4 sr3 sr4 unfolding ss hh
apply(simp add: Δ1'_defs Δ1_defs)
by (metis atLeastAtMost_iff atLeastatMost_empty_iff empty_iff empty_set
nat_le_linear numeral_le_iff semiring_norm(68,69,72)
length_1_butlast length_map in_set_butlastD)
qed
qed
qed
qed
qed
lemma step5: "unwindIntoCond Δ2' Δ2"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δ2': "Δ2' n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases cfg3) (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases cfg4) (metis state.collapse vstore.collapse)
note cfg = cfg3 cfg4
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
have f1:"¬finalN ss1"
using Δ2' unfolding ss Δ2'_def
apply clarsimp
by(frule common_implies, simp)
have f2:"¬finalN ss2"
using Δ2' unfolding ss Δ2'_def
apply clarsimp
by(frule common_implies, simp)
have f3:"¬finalS ss3"
using Δ2' unfolding ss
apply-apply(frule Δ2'_implies)
using finalS_while_spec_L2 by force
have f4:"¬finalS ss4"
using Δ2' unfolding ss
apply-apply(frule Δ2'_implies)
using finalS_while_spec_L2 by force
note finals = f1 f2 f3 f4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using finals by auto
then show "isIntO ss3 = isIntO ss4" by simp
have sec3[simp]:"¬ isSecO ss3"
using Δ2' unfolding ss
by (simp add: Δ2'_defs, metis list.size(3) zero_neq_numeral)
have sec4[simp]:"¬ isSecO ss4"
using Δ2' unfolding ss
by (simp add: Δ2'_defs, metis list.size(3) zero_neq_numeral)
have stat[simp]:"⋀s3' s4' statA'. statA' = sstatA' statA ss3 ss4 ⟹
validTransO (ss3, s3') ⟹ validTransO (ss4, s4') ⟹
(statA = statA' ∨ statO = Diff)"
subgoal for ss3' ss4'
apply (cases ss3, cases ss4, cases ss1, cases ss2)
apply (cases ss3', cases ss4', clarsimp)
using Δ2' finals unfolding ss apply clarsimp
apply(simp_all add: Δ2'_defs sstatA'_def)
apply(cases statO, simp_all) by (cases statA, simp_all add: newStat_EqI) .
have match12_aux:"
(⋀pstate3' cfg3' cfgs3' ib3' ibUT3' ls3'
pstate4' cfg4' cfgs4' ib4' ibUT4' ls4' statA'.
(pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3) →S (pstate3', cfg3', cfgs3', ib3', ibUT3', ls3') ⟹
(pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4) →S (pstate4', cfg4', cfgs4', ib4', ibUT4', ls4') ⟹
Opt.eqAct ss3 ss4 ⟹ statA' = sstatA' statA ss3 ss4 ⟹
(Δ2 ∞ 1 1 (pstate3', cfg3', cfgs3', ib3', ibUT3', ls3') (pstate4', cfg4', cfgs4', ib4', ibUT4', ls4') statA' ss1 ss2 statO))
⟹ match12 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
apply(rule match12_simpleI, simp_all, rule disjI1)
apply(rule exI[of _ 1], rule conjI)
subgoal using Δ2' unfolding ss Δ2'_defs apply clarify
by (metis one_less_numeral_iff semiring_norm(76))
apply(rule exI[of _ 1], rule conjI)
subgoal using Δ2' unfolding ss Δ2'_defs apply clarify
by (metis one_less_numeral_iff semiring_norm(76))
subgoal for ss3' ss4' apply(cases ss3', cases ss4')
subgoal for pstate3' cfg3' cfgs3' ib3' ibUT3' ls3'
pstate4' cfg4' cfgs4' ib4' ibUT4' ls4'
using ss3 ss4 by blast . .
show "react Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
apply(rule match12_aux)
subgoal premises prem using prem(1)[unfolded ss ]
proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2' unfolding ss by (auto simp add: Δ2'_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2' unfolding ss by (auto simp add: Δ2'_defs)
next
case spec_mispred
then show ?thesis using stat Δ2' prem unfolding ss by (auto simp add: Δ2'_defs)
next
case spec_normal
then show ?thesis using stat Δ2' prem unfolding ss by (auto simp add: Δ2'_defs)
next
case spec_Fence
then show ?thesis using stat Δ2' prem unfolding ss by (auto simp add: Δ2'_defs)
next
case spec_resolve note sr3 = spec_resolve
show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
case nonspec_normal
then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
next
case nonspec_mispred
then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
next
case spec_mispred
then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
next
case spec_normal
then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
next
case spec_Fence
then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
next
case spec_resolve note sr4 = spec_resolve
show ?thesis
using stat Δ2' prem sr3 sr4 unfolding ss
apply(simp add: Δ2'_defs Δ2_defs)
apply(intro conjI)
apply (metis last_map map_butlast map_is_Nil_conv)
apply (metis image_subset_iff in_set_butlastD)
apply(metis) apply(metis) apply (metis in_set_butlastD)
apply (metis in_set_butlastD) apply (metis in_set_butlastD)
apply (metis in_set_butlastD) apply (metis in_set_butlastD)
apply (metis in_set_butlastD) apply (metis prem(1) prem(2) ss3 ss4)
apply (metis in_set_butlastD) apply (metis in_set_butlastD)
apply (smt (verit, ccfv_SIG) butlast.simps(2) last_ConsL last_map
length_0_conv length_map map_L2 map_butlast not_Cons_self2)
apply clarify apply(elim disjE)
apply (metis map_L2 butlast.simps(2) last.simps last_map list.simps(8)
map_butlast not_Cons_self2 numeral_eq_iff semiring_norm(88))
by (metis map_L2 butlast.simps(2) last.simps last_map list.simps(8)
map_butlast image_constant_conv not_Cons_self2 image_subset_iff
list.set_intros(1,2) list.simps(15) resolve.simps resolve_127
set_empty2 subset_insertI resolve_73 numeral_eq_iff )+
qed
qed .
qed
qed
lemma stepe: "unwindIntoCond Δe Δe"
proof(rule unwindIntoCond_simpleI)
fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
and Δe: "Δe n w1 w2 ss3 ss4 statA ss1 ss2 statO"
obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
by (cases ss3, auto)
obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
by (cases ss4, auto)
obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
by (cases ss1, auto)
obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
by (cases ss2, auto)
note ss = ss3 ss4 ss1 ss2
obtain pc3 vs3 avst3 h3 p3 where
cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
by (cases cfg3) (metis state.collapse vstore.collapse)
obtain pc4 vs4 avst4 h4 p4 where
cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
by (cases cfg4) (metis state.collapse vstore.collapse)
note cfg = cfg3 cfg4
obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
note hh = h3 h4
show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
using Δe Opt.final_def finalS_def stepS_endPC endPC_def finalB_endPC
unfolding Δe_defs ss by clarsimp
then show "isIntO ss3 = isIntO ss4" by simp
show "react Δe w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding react_def proof(intro conjI)
show "match1 Δe w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match1_def by (simp add: finalS_def final_def)
show "match2 Δe w1 w2 ss3 ss4 statA ss1 ss2 statO"
unfolding match2_def by (simp add: finalS_def final_def)
show "match12 Δe w1 w2 ss3 ss4 statA ss1 ss2 statO"
apply(rule match12_simpleI) using Δe unfolding ss
by (simp add: Δe_defs stepS_endPC)
qed
qed
lemmas theConds = step0 step1 step2 step3 step4 step5 stepe
proposition lrsecure
proof-
define m where m: "m ≡ (7::nat)"
define Δs where Δs: "Δs ≡ λi::nat.
if i = 0 then Δ0
else if i = 1 then Δ1
else if i = 2 then Δ2
else if i = 3 then Δ3
else if i = 4 then Δ1'
else if i = 5 then Δ2'
else Δe"
define nxt where nxt: "nxt ≡ λi::nat.
if i = 0 then {0,1::nat}
else if i = 1 then {1,4,2,3,6}
else if i = 2 then {2,5,1}
else if i = 3 then {3,1}
else if i = 4 then {1}
else if i = 5 then {2}
else {6}"
show ?thesis apply(rule distrib_unwind_lrsecure[of m nxt Δs])
subgoal unfolding m by auto
subgoal unfolding nxt m by auto
subgoal using init unfolding Δs by auto
subgoal
unfolding m nxt Δs apply (simp split: if_splits)
using theConds
unfolding oor_def oor3_def oor4_def oor5_def by auto .
qed
end