|
4
|
1 Soundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
2 HTProof bPre cm bPost @$\rightarrow$@ 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@$\text{2}$@ 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 r1 : SemCond bPre' s1
|
|
|
13 r1 = tautValid bPre bPre' tautPre s1 q1
|
|
|
14 r2 : SemCond bPost' s2
|
|
|
15 r2 = hyp s1 s2 r1 q2
|
|
|
16 in tautValid bPost' bPost tautPost s2 r2
|
|
|
17 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
|
|
|
18 s1 s2 q1 q2
|
|
|
19 = let hyp1 : Satisfies bPre cm1 bMid
|
|
|
20 hyp1 = Soundness pr1
|
|
|
21 hyp2 : Satisfies bMid cm2 bPost
|
|
|
22 hyp2 = Soundness pr2
|
|
|
23 sMid : State
|
|
|
24 sMid = proj@$\text{1}$@ q2
|
|
|
25 r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2
|
|
|
26 r1 = proj@$\text{2}$@ q2
|
|
|
27 r2 : SemComm cm1 s1 sMid
|
|
|
28 r2 = proj@$\text{1}$@ r1
|
|
|
29 r3 : SemComm cm2 sMid s2
|
|
|
30 r3 = proj@$\text{2}$@ r1
|
|
|
31 r4 : SemCond bMid sMid
|
|
|
32 r4 = hyp1 s1 sMid q1 r2
|
|
|
33 in hyp2 sMid s2 r4 r3
|
|
|
34 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
|
|
|
35 s1 s2 q1 q2
|
|
|
36 = let hypThen : Satisfies (bPre /\ b) cmThen bPost
|
|
|
37 hypThen = Soundness pThen
|
|
|
38 hypElse : Satisfies (bPre /\ neg b) cmElse bPost
|
|
|
39 hypElse = Soundness pElse
|
|
|
40 rThen : RelOpState.comp
|
|
|
41 (RelOpState.delta (SemCond b))
|
|
|
42 (SemComm cmThen) s1 s2 @$\rightarrow$@
|
|
|
43 SemCond bPost s2
|
|
|
44 rThen = @$\lambda$@ h @$\rightarrow$@
|
|
|
45 let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2
|
|
|
46 t1 = (proj@$\text{2}$@ (RelOpState.deltaRestPre
|
|
|
47 (SemCond b)
|
|
|
48 (SemComm cmThen) s1 s2)) h
|
|
|
49 t2 : SemCond (bPre /\ b) s1
|
|
|
50 t2 = (proj@$\text{2}$@ (respAnd bPre b s1))
|
|
|
51 (q1 , proj@$\text{1}$@ t1)
|
|
|
52 in hypThen s1 s2 t2 (proj@$\text{2}$@ t1)
|
|
|
53 rElse : RelOpState.comp
|
|
|
54 (RelOpState.delta (NotP (SemCond b)))
|
|
|
55 (SemComm cmElse) s1 s2 @$\rightarrow$@
|
|
|
56 SemCond bPost s2
|
|
|
57 rElse = @$\lambda$@ h @$\rightarrow$@
|
|
|
58 let t10 : (NotP (SemCond b) s1) @$\times$@
|
|
|
59 (SemComm cmElse s1 s2)
|
|
|
60 t10 = proj@$\text{2}$@ (RelOpState.deltaRestPre
|
|
|
61 (NotP (SemCond b)) (SemComm cmElse) s1 s2)
|
|
|
62 h
|
|
|
63 t6 : SemCond (neg b) s1
|
|
|
64 t6 = proj@$\text{2}$@ (respNeg b s1) (proj@$\text{1}$@ t10)
|
|
|
65 t7 : SemComm cmElse s1 s2
|
|
|
66 t7 = proj@$\text{2}$@ t10
|
|
|
67 t8 : SemCond (bPre /\ neg b) s1
|
|
|
68 t8 = proj@$\text{2}$@ (respAnd bPre (neg b) s1)
|
|
|
69 (q1 , t6)
|
|
|
70 in hypElse s1 s2 t8 t7
|
|
|
71 in when rThen rElse q2
|
|
|
72 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
|
|
|
73 = proj@$\text{2}$@ (respAnd bInv (neg b) s2) t20
|
|
|
74 where
|
|
|
75 hyp : Satisfies (bInv /\ b) cm' bInv
|
|
|
76 hyp = Soundness pr
|
|
|
77 n : $mathbb{N}$
|
|
|
78 n = proj@$\text{1}$@ q2
|
|
|
79 Rel1 : $mathbb{N}$ @$\rightarrow$@ Rel State (Level.zero)
|
|
|
80 Rel1 = @$\lambda$@ m @$\rightarrow$@
|
|
|
81 RelOpState.repeat
|
|
|
82 m
|
|
|
83 (RelOpState.comp (RelOpState.delta (SemCond b))
|
|
|
84 (SemComm cm'))
|
|
|
85 t1 : RelOpState.comp
|
|
|
86 (Rel1 n)
|
|
|
87 (RelOpState.delta (NotP (SemCond b))) s1 s2
|
|
|
88 t1 = proj@$\text{2}$@ q2
|
|
|
89 t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2)
|
|
|
90 t15 = proj@$\text{2}$@ (RelOpState.deltaRestPost
|
|
|
91 (NotP (SemCond b)) (Rel1 n) s1 s2)
|
|
|
92 t1
|
|
|
93 t16 : Rel1 n s1 s2
|
|
|
94 t16 = proj@$\text{1}$@ t15
|
|
|
95 t17 : NotP (SemCond b) s2
|
|
|
96 t17 = proj@$\text{2}$@ t15
|
|
|
97 lem1 : (m : $mathbb{N}$) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@
|
|
|
98 SemCond bInv ss2
|
|
|
99 lem1 $mathbb{N}$.zero ss2 h
|
|
|
100 = substId1 State (proj@$\text{2}$@ h) (SemCond bInv) q1
|
|
|
101 lem1 ($mathbb{N}$.suc n) ss2 h
|
|
|
102 = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@
|
|
|
103 SemCond bInv z
|
|
|
104 hyp2 = lem1 n
|
|
|
105 s20 : State
|
|
|
106 s20 = proj@$\text{1}$@ h
|
|
|
107 t21 : Rel1 n s1 s20
|
|
|
108 t21 = proj@$\text{1}$@ (proj@$\text{2}$@ h)
|
|
|
109 t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2)
|
|
|
110 t22 = proj@$\text{2}$@ (RelOpState.deltaRestPre
|
|
|
111 (SemCond b) (SemComm cm') s20 ss2)
|
|
|
112 (proj@$\text{2}$@ (proj@$\text{2}$@ h))
|
|
|
113 t23 : SemCond (bInv /\ b) s20
|
|
|
114 t23 = proj@$\text{2}$@ (respAnd bInv b s20)
|
|
|
115 (hyp2 s20 t21 , proj@$\text{1}$@ t22)
|
|
|
116 in hyp s20 ss2 t23 (proj@$\text{2}$@ t22)
|
|
|
117 t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2
|
|
|
118 t20 = lem1 n s2 t16 , proj@$\text{2}$@ (respNeg b s2) t17
|
