|
1
|
1 Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
|
|
|
2 HTProof bPre cm bPost -> Satisfies bPre cm bPost
|
|
|
3 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
|
|
|
4 = axiomValid bPre cm bPost pr s1 s2 q1 q2
|
|
|
5 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
|
|
|
6 = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
|
|
|
7 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
|
|
|
8 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
|
|
|
9 s1 s2 q1 q2
|
|
|
10 = let hyp : Satisfies bPre' cm bPost'
|
|
|
11 hyp = Soundness pr
|
|
|
12 in tautValid bPost' bPost tautPost s2 (hyp s1 s2 (tautValid bPre bPre' tautPre s1 q1) q2)
|
|
|
13 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
|
|
|
14 s1 s2 q1 q2
|
|
|
15 = let hyp1 : Satisfies bPre cm1 bMid
|
|
|
16 hyp1 = Soundness pr1
|
|
|
17 hyp2 : Satisfies bMid cm2 bPost
|
|
|
18 hyp2 = Soundness pr2
|
|
|
19 in hyp2 (proj₁ q2) s2 (hyp1 s1 (proj₁ q2) q1 (proj₁ (proj₂ q2))) (proj₂ (proj₂ q2))
|
|
|
20 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
|
|
|
21 s1 s2 q1 q2
|
|
|
22 = let hypThen : Satisfies (bPre /\ b) cmThen bPost
|
|
|
23 hypThen = Soundness pThen
|
|
|
24 hypElse : Satisfies (bPre /\ neg b) cmElse bPost
|
|
|
25 hypElse = Soundness pElse
|
|
|
26 rThen : RelOpState.comp (RelOpState.delta (SemCond b))
|
|
|
27 (SemComm cmThen) s1 s2 -> SemCond bPost s2
|
|
|
28 rThen = λ h -> hypThen s1 s2 ((proj₂ (respAnd bPre b s1)) (q1 , proj₁ t1))
|
|
|
29 (proj₂ ((proj₂ (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h))
|
|
|
30 rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
|
|
|
31 (SemComm cmElse) s1 s2 -> SemCond bPost s2
|
|
|
32 rElse = λ h ->
|
|
|
33 let t10 : (NotP (SemCond b) s1) × (SemComm cmElse s1 s2)
|
|
|
34 t10 = proj₂ (RelOpState.deltaRestPre
|
|
|
35 (NotP (SemCond b)) (SemComm cmElse) s1 s2) h
|
|
|
36 in hypElse s1 s2 (proj₂ (respAnd bPre (neg b) s1)
|
|
|
37 (q1 , (proj₂ (respNeg b s1) (proj₁ t10)))) (proj₂ t10)
|
|
|
38 in when rThen rElse q2
|
|
|
39 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
|
|
|
40 = proj₂ (respAnd bInv (neg b) s2)
|
|
|
41 (lem1 (proj₁ q2) s2 (proj₁ t15) , proj₂ (respNeg b s2) (proj₂ t15))
|
|
|
42 where
|
|
|
43 hyp : Satisfies (bInv /\ b) cm' bInv
|
|
|
44 hyp = Soundness pr
|
|
|
45 Rel1 : ℕ -> Rel State (Level.zero)
|
|
|
46 Rel1 = λ m ->
|
|
|
47 RelOpState.repeat
|
|
|
48 m
|
|
|
49 (RelOpState.comp (RelOpState.delta (SemCond b))
|
|
|
50 (SemComm cm'))
|
|
|
51 t15 : (Rel1 (proj₁ q2) s1 s2) × (NotP (SemCond b) s2)
|
|
|
52 t15 = proj₂ (RelOpState.deltaRestPost
|
|
|
53 (NotP (SemCond b)) (Rel1 (proj₁ q2)) s1 s2) (proj₂ q2)
|
|
|
54 lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 -> SemCond bInv ss2
|
|
|
55 lem1 zero ss2 h = substId1 State (proj₂ h) (SemCond bInv) q1
|
|
|
56 lem1 (suc n) ss2 h
|
|
|
57 = let hyp2 : (z : State) -> Rel1 (proj₁ q2) s1 z ->
|
|
|
58 SemCond bInv z
|
|
|
59 hyp2 = lem1 n
|
|
|
60 t22 : (SemCond b (proj₁ h)) × (SemComm cm' (proj₁ h) ss2)
|
|
|
61 t22 = proj₂ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') (proj₁ h) ss2)
|
|
|
62 (proj₂ (proj₂ h))
|
|
|
63 t23 : SemCond (bInv /\ b) (proj₁ h)
|
|
|
64 t23 = proj₂ (respAnd bInv b (proj₁ h))
|
|
|
65 (hyp2 (proj₁ h) (proj₁ (proj₂ h)) , proj₁ t22)
|
|
|
66 in hyp (proj₁ h) ss2 t23 (proj₂ t22)
|
