Mercurial > hg > Papers > 2020 > soto-midterm
diff src/HoareSoundness.agda.replaced @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HoareSoundness.agda.replaced Tue Sep 08 18:38:08 2020 +0900 @@ -0,0 +1,197 @@ +{-@$\#$@ OPTIONS --universe-polymorphism @$\#$@-} + +open import Level +open import Data.Nat.Base +open import Data.Product +open import Data.Bool.Base +open import Data.Empty +open import Data.Sum +open import Relation.Binary +open import Relation.Nullary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import RelOp +open import utilities + +module HoareSoundness + (Cond : Set) + (PrimComm : Set) + (neg : Cond @$\rightarrow$@ Cond) + (_@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond) + (Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set) + (State : Set) + (SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set) + (tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@ + (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ SemCond b2 s) + (respNeg : (b : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s)) + (respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (b1 @$\wedge$@ b2) s) + ((SemCond b1 s) @$\times$@ (SemCond b2 s))) + (PrimSemComm : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l) + (Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set) + (axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@ + (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@ + SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ SemCond bPost s2) where + +open import Hoare PrimComm Cond Axiom Tautology _@$\wedge$@_ neg + +open import RelOp +module RelOpState = RelOp State + +NotP : {S : Set} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S +NotP X s = @$\neg$@ X s + +_\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2) + +when : {X Y Z : Set} @$\rightarrow$@ (X @$\rightarrow$@ Z) @$\rightarrow$@ (Y @$\rightarrow$@ Z) @$\rightarrow$@ + X ⊎ Y @$\rightarrow$@ Z +when f g (inj@$\_{1}$@ x) = f x +when f g (inj@$\_{2}$@ y) = g y + +-- semantics of commands +SemComm : Comm @$\rightarrow$@ Rel State (Level.zero) +SemComm Skip = RelOpState.deltaGlob +SemComm Abort = RelOpState.emptyRel +SemComm (PComm pc) = PrimSemComm pc +SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) +SemComm (If b c1 c2) + = RelOpState.union + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm c1)) + (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm c2)) +SemComm (While b c) + = RelOpState.unionInf + (@$\lambda$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ + RelOpState.comp (RelOpState.repeat + n + (RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm c))) + (RelOpState.delta (NotP (SemCond b)))) + +Satisfies : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set +Satisfies bPre cm bPost + = (s1 : State) @$\rightarrow$@ (s2 : State) @$\rightarrow$@ + SemCond bPre s1 @$\rightarrow$@ SemComm cm s1 s2 @$\rightarrow$@ SemCond bPost s2 + +Soundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost +Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 + = axiomValid bPre cm bPost pr s1 s2 q1 q2 +Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2 + = substId1 State {Level.zero} {State} {s1} {s2} (proj@$\_{2}$@ q2) (SemCond bPost) q1 +Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () +Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) + s1 s2 q1 q2 + = let hyp : Satisfies bPre' cm bPost' + hyp = Soundness pr + r1 : SemCond bPre' s1 + r1 = tautValid bPre bPre' tautPre s1 q1 + r2 : SemCond bPost' s2 + r2 = hyp s1 s2 r1 q2 + in tautValid bPost' bPost tautPost s2 r2 +Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) + s1 s2 q1 q2 + = let hyp1 : Satisfies bPre cm1 bMid + hyp1 = Soundness pr1 + hyp2 : Satisfies bMid cm2 bPost + hyp2 = Soundness pr2 + sMid : State + sMid = proj@$\_{1}$@ q2 + r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2 + r1 = proj@$\_{2}$@ q2 + r2 : SemComm cm1 s1 sMid + r2 = proj@$\_{1}$@ r1 + r3 : SemComm cm2 sMid s2 + r3 = proj@$\_{2}$@ r1 + r4 : SemCond bMid sMid + r4 = hyp1 s1 sMid q1 r2 + in hyp2 sMid s2 r4 r3 +Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) + s1 s2 q1 q2 + = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost + hypThen = Soundness pThen + hypElse : Satisfies (bPre @$\wedge$@ neg b) cmElse bPost + hypElse = Soundness pElse + rThen : RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm cmThen) s1 s2 @$\rightarrow$@ + SemCond bPost s2 + rThen = @$\lambda$@ h @$\rightarrow$@ + let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2 + t1 = (proj@$\_{2}$@ (RelOpState.deltaRestPre + (SemCond b) + (SemComm cmThen) s1 s2)) h + t2 : SemCond (bPre @$\wedge$@ b) s1 + t2 = (proj@$\_{2}$@ (respAnd bPre b s1)) + (q1 , proj@$\_{1}$@ t1) + in hypThen s1 s2 t2 (proj@$\_{2}$@ t1) + rElse : RelOpState.comp + (RelOpState.delta (NotP (SemCond b))) + (SemComm cmElse) s1 s2 @$\rightarrow$@ + SemCond bPost s2 + rElse = @$\lambda$@ h @$\rightarrow$@ + let t10 : (NotP (SemCond b) s1) @$\times$@ + (SemComm cmElse s1 s2) + t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre + (NotP (SemCond b)) (SemComm cmElse) s1 s2) + h + t6 : SemCond (neg b) s1 + t6 = proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10) + t7 : SemComm cmElse s1 s2 + t7 = proj@$\_{2}$@ t10 + t8 : SemCond (bPre @$\wedge$@ neg b) s1 + t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1) + (q1 , t6) + in hypElse s1 s2 t8 t7 + in when rThen rElse q2 +Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 + = proj@$\_{2}$@ (respAnd bInv (neg b) s2) t20 + where + hyp : Satisfies (bInv @$\wedge$@ b) cm' bInv + hyp = Soundness pr + n : @$\mathbb{N}$@ + n = proj@$\_{1}$@ q2 + Rel1 : @$\mathbb{N}$@ @$\rightarrow$@ Rel State (Level.zero) + Rel1 = @$\lambda$@ m @$\rightarrow$@ + RelOpState.repeat + m + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm cm')) + t1 : RelOpState.comp + (Rel1 n) + (RelOpState.delta (NotP (SemCond b))) s1 s2 + t1 = proj@$\_{2}$@ q2 + t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2) + t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost + (NotP (SemCond b)) (Rel1 n) s1 s2) + t1 + t16 : Rel1 n s1 s2 + t16 = proj@$\_{1}$@ t15 + t17 : NotP (SemCond b) s2 + t17 = proj@$\_{2}$@ t15 + lem1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ + SemCond bInv ss2 + lem1 @$\mathbb{N}$@.zero ss2 h + = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1 + lem1 (@$\mathbb{N}$@.suc n) ss2 h + = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@ + SemCond bInv z + hyp2 = lem1 n + s20 : State + s20 = proj@$\_{1}$@ h + t21 : Rel1 n s1 s20 + t21 = proj@$\_{1}$@ (proj@$\_{2}$@ h) + t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2) + t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre + (SemCond b) (SemComm cm') s20 ss2) + (proj@$\_{2}$@ (proj@$\_{2}$@ h)) + t23 : SemCond (bInv @$\wedge$@ b) s20 + t23 = proj@$\_{2}$@ (respAnd bInv b s20) + (hyp2 s20 t21 , proj@$\_{1}$@ t22) + in hyp s20 ss2 t23 (proj@$\_{2}$@ t22) + t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2 + t20 = lem1 n s2 t16 , proj@$\_{2}$@ (respNeg b s2) t17