Mercurial > hg > Papers > 2020 > soto-midterm
comparison src/agda-hoare-soundness.agda @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 0:b919985837a3 | 1:73127e0ab57c |
|---|---|
| 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) |