|
3
|
1 {-@$\#$@ OPTIONS --universe-polymorphism @$\#$@-}
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Data.Nat.Base
|
|
|
5 open import Data.Product
|
|
|
6 open import Data.Bool.Base
|
|
|
7 open import Data.Empty
|
|
|
8 open import Data.Sum
|
|
|
9 open import Relation.Binary
|
|
|
10 open import Relation.Nullary
|
|
|
11 open import Relation.Binary.Core
|
|
|
12 open import Relation.Binary.PropositionalEquality
|
|
|
13 open import RelOp
|
|
|
14 open import utilities
|
|
|
15
|
|
|
16 module HoareSoundness
|
|
|
17 (Cond : Set)
|
|
|
18 (PrimComm : Set)
|
|
|
19 (neg : Cond @$\rightarrow$@ Cond)
|
|
|
20 (_@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond)
|
|
|
21 (Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set)
|
|
|
22 (State : Set)
|
|
|
23 (SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set)
|
|
|
24 (tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@
|
|
|
25 (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ SemCond b2 s)
|
|
|
26 (respNeg : (b : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@
|
|
|
27 Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s))
|
|
|
28 (respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@
|
|
|
29 Iff (SemCond (b1 @$\wedge$@ b2) s)
|
|
|
30 ((SemCond b1 s) @$\times$@ (SemCond b2 s)))
|
|
|
31 (PrimSemComm : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l)
|
|
|
32 (Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set)
|
|
|
33 (axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@
|
|
|
34 (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@
|
|
|
35 SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ SemCond bPost s2) where
|
|
|
36
|
|
|
37 open import Hoare PrimComm Cond Axiom Tautology _@$\wedge$@_ neg
|
|
|
38
|
|
|
39 open import RelOp
|
|
|
40 module RelOpState = RelOp State
|
|
|
41
|
|
|
42 NotP : {S : Set} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S
|
|
|
43 NotP X s = @$\neg$@ X s
|
|
|
44
|
|
|
45 _\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond
|
|
|
46 b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2)
|
|
|
47
|
|
|
48 when : {X Y Z : Set} @$\rightarrow$@ (X @$\rightarrow$@ Z) @$\rightarrow$@ (Y @$\rightarrow$@ Z) @$\rightarrow$@
|
|
|
49 X ⊎ Y @$\rightarrow$@ Z
|
|
|
50 when f g (inj@$\_{1}$@ x) = f x
|
|
|
51 when f g (inj@$\_{2}$@ y) = g y
|
|
|
52
|
|
|
53 -- semantics of commands
|
|
|
54 SemComm : Comm @$\rightarrow$@ Rel State (Level.zero)
|
|
|
55 SemComm Skip = RelOpState.deltaGlob
|
|
|
56 SemComm Abort = RelOpState.emptyRel
|
|
|
57 SemComm (PComm pc) = PrimSemComm pc
|
|
|
58 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
|
|
|
59 SemComm (If b c1 c2)
|
|
|
60 = RelOpState.union
|
|
|
61 (RelOpState.comp (RelOpState.delta (SemCond b))
|
|
|
62 (SemComm c1))
|
|
|
63 (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
|
|
|
64 (SemComm c2))
|
|
|
65 SemComm (While b c)
|
|
|
66 = RelOpState.unionInf
|
|
|
67 (@$\lambda$@ (n : @$\mathbb{N}$@) @$\rightarrow$@
|
|
|
68 RelOpState.comp (RelOpState.repeat
|
|
|
69 n
|
|
|
70 (RelOpState.comp
|
|
|
71 (RelOpState.delta (SemCond b))
|
|
|
72 (SemComm c)))
|
|
|
73 (RelOpState.delta (NotP (SemCond b))))
|
|
|
74
|
|
|
75 Satisfies : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set
|
|
|
76 Satisfies bPre cm bPost
|
|
|
77 = (s1 : State) @$\rightarrow$@ (s2 : State) @$\rightarrow$@
|
|
|
78 SemCond bPre s1 @$\rightarrow$@ SemComm cm s1 s2 @$\rightarrow$@ SemCond bPost s2
|
|
|
79
|
|
|
80 Soundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
81 HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost
|
|
|
82 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
|
|
|
83 = axiomValid bPre cm bPost pr s1 s2 q1 q2
|
|
|
84 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
|
|
|
85 = substId1 State {Level.zero} {State} {s1} {s2} (proj@$\_{2}$@ q2) (SemCond bPost) q1
|
|
|
86 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
|
|
|
87 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
|
|
|
88 s1 s2 q1 q2
|
|
|
89 = let hyp : Satisfies bPre' cm bPost'
|
|
|
90 hyp = Soundness pr
|
|
|
91 r1 : SemCond bPre' s1
|
|
|
92 r1 = tautValid bPre bPre' tautPre s1 q1
|
|
|
93 r2 : SemCond bPost' s2
|
|
|
94 r2 = hyp s1 s2 r1 q2
|
|
|
95 in tautValid bPost' bPost tautPost s2 r2
|
|
|
96 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
|
|
|
97 s1 s2 q1 q2
|
|
|
98 = let hyp1 : Satisfies bPre cm1 bMid
|
|
|
99 hyp1 = Soundness pr1
|
|
|
100 hyp2 : Satisfies bMid cm2 bPost
|
|
|
101 hyp2 = Soundness pr2
|
|
|
102 sMid : State
|
|
|
103 sMid = proj@$\_{1}$@ q2
|
|
|
104 r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2
|
|
|
105 r1 = proj@$\_{2}$@ q2
|
|
|
106 r2 : SemComm cm1 s1 sMid
|
|
|
107 r2 = proj@$\_{1}$@ r1
|
|
|
108 r3 : SemComm cm2 sMid s2
|
|
|
109 r3 = proj@$\_{2}$@ r1
|
|
|
110 r4 : SemCond bMid sMid
|
|
|
111 r4 = hyp1 s1 sMid q1 r2
|
|
|
112 in hyp2 sMid s2 r4 r3
|
|
|
113 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
|
|
|
114 s1 s2 q1 q2
|
|
|
115 = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost
|
|
|
116 hypThen = Soundness pThen
|
|
|
117 hypElse : Satisfies (bPre @$\wedge$@ neg b) cmElse bPost
|
|
|
118 hypElse = Soundness pElse
|
|
|
119 rThen : RelOpState.comp
|
|
|
120 (RelOpState.delta (SemCond b))
|
|
|
121 (SemComm cmThen) s1 s2 @$\rightarrow$@
|
|
|
122 SemCond bPost s2
|
|
|
123 rThen = @$\lambda$@ h @$\rightarrow$@
|
|
|
124 let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2
|
|
|
125 t1 = (proj@$\_{2}$@ (RelOpState.deltaRestPre
|
|
|
126 (SemCond b)
|
|
|
127 (SemComm cmThen) s1 s2)) h
|
|
|
128 t2 : SemCond (bPre @$\wedge$@ b) s1
|
|
|
129 t2 = (proj@$\_{2}$@ (respAnd bPre b s1))
|
|
|
130 (q1 , proj@$\_{1}$@ t1)
|
|
|
131 in hypThen s1 s2 t2 (proj@$\_{2}$@ t1)
|
|
|
132 rElse : RelOpState.comp
|
|
|
133 (RelOpState.delta (NotP (SemCond b)))
|
|
|
134 (SemComm cmElse) s1 s2 @$\rightarrow$@
|
|
|
135 SemCond bPost s2
|
|
|
136 rElse = @$\lambda$@ h @$\rightarrow$@
|
|
|
137 let t10 : (NotP (SemCond b) s1) @$\times$@
|
|
|
138 (SemComm cmElse s1 s2)
|
|
|
139 t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre
|
|
|
140 (NotP (SemCond b)) (SemComm cmElse) s1 s2)
|
|
|
141 h
|
|
|
142 t6 : SemCond (neg b) s1
|
|
|
143 t6 = proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)
|
|
|
144 t7 : SemComm cmElse s1 s2
|
|
|
145 t7 = proj@$\_{2}$@ t10
|
|
|
146 t8 : SemCond (bPre @$\wedge$@ neg b) s1
|
|
|
147 t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1)
|
|
|
148 (q1 , t6)
|
|
|
149 in hypElse s1 s2 t8 t7
|
|
|
150 in when rThen rElse q2
|
|
|
151 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
|
|
|
152 = proj@$\_{2}$@ (respAnd bInv (neg b) s2) t20
|
|
|
153 where
|
|
|
154 hyp : Satisfies (bInv @$\wedge$@ b) cm' bInv
|
|
|
155 hyp = Soundness pr
|
|
|
156 n : @$\mathbb{N}$@
|
|
|
157 n = proj@$\_{1}$@ q2
|
|
|
158 Rel1 : @$\mathbb{N}$@ @$\rightarrow$@ Rel State (Level.zero)
|
|
|
159 Rel1 = @$\lambda$@ m @$\rightarrow$@
|
|
|
160 RelOpState.repeat
|
|
|
161 m
|
|
|
162 (RelOpState.comp (RelOpState.delta (SemCond b))
|
|
|
163 (SemComm cm'))
|
|
|
164 t1 : RelOpState.comp
|
|
|
165 (Rel1 n)
|
|
|
166 (RelOpState.delta (NotP (SemCond b))) s1 s2
|
|
|
167 t1 = proj@$\_{2}$@ q2
|
|
|
168 t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2)
|
|
|
169 t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost
|
|
|
170 (NotP (SemCond b)) (Rel1 n) s1 s2)
|
|
|
171 t1
|
|
|
172 t16 : Rel1 n s1 s2
|
|
|
173 t16 = proj@$\_{1}$@ t15
|
|
|
174 t17 : NotP (SemCond b) s2
|
|
|
175 t17 = proj@$\_{2}$@ t15
|
|
|
176 lem1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@
|
|
|
177 SemCond bInv ss2
|
|
|
178 lem1 @$\mathbb{N}$@.zero ss2 h
|
|
|
179 = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1
|
|
|
180 lem1 (@$\mathbb{N}$@.suc n) ss2 h
|
|
|
181 = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@
|
|
|
182 SemCond bInv z
|
|
|
183 hyp2 = lem1 n
|
|
|
184 s20 : State
|
|
|
185 s20 = proj@$\_{1}$@ h
|
|
|
186 t21 : Rel1 n s1 s20
|
|
|
187 t21 = proj@$\_{1}$@ (proj@$\_{2}$@ h)
|
|
|
188 t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2)
|
|
|
189 t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre
|
|
|
190 (SemCond b) (SemComm cm') s20 ss2)
|
|
|
191 (proj@$\_{2}$@ (proj@$\_{2}$@ h))
|
|
|
192 t23 : SemCond (bInv @$\wedge$@ b) s20
|
|
|
193 t23 = proj@$\_{2}$@ (respAnd bInv b s20)
|
|
|
194 (hyp2 s20 t21 , proj@$\_{1}$@ t22)
|
|
|
195 in hyp s20 ss2 t23 (proj@$\_{2}$@ t22)
|
|
|
196 t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2
|
|
|
197 t20 = lem1 n s2 t16 , proj@$\_{2}$@ (respNeg b s2) t17
|
