-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathBigStepErasedDeterministic.agda
100 lines (96 loc) · 5.41 KB
/
BigStepErasedDeterministic.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
module Dyn.BigStepErasedDeterministic where
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; ∃; ∃-syntax; Σ; Σ-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; cong; sym)
open import Function using (case_of_)
open import Common.Utils
open import Common.SecurityLabels
open import Memory.Heap
open import Dyn.Syntax
open import Dyn.Values
open import Dyn.BigStepErased
⇓ₑ-deterministic : ∀ {M μ μ₁ μ₂ pc} {V₁ V₂}
→ μ ∣ pc ⊢ M ⇓ₑ V₁ ∣ μ₁
→ μ ∣ pc ⊢ M ⇓ₑ V₂ ∣ μ₂
-------------------------------------
→ V₁ ≡ V₂ × μ₁ ≡ μ₂
⇓ₑ-deterministic (⇓ₑ-val _) (⇓ₑ-val _) = ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-app L⇓ƛN M⇓V N[V]⇓W) (⇓ₑ-app L⇓ƛN† M⇓V† N[V]⇓W†) =
case ⇓ₑ-deterministic L⇓ƛN L⇓ƛN† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic N[V]⇓W N[V]⇓W† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-app L⇓ƛN _ _) (⇓ₑ-app-● L⇓● _) =
contradiction (⇓ₑ-deterministic L⇓ƛN L⇓●) (λ ())
⇓ₑ-deterministic (⇓ₑ-app-● L⇓● _) (⇓ₑ-app L⇓ƛN _ _) =
contradiction (⇓ₑ-deterministic L⇓● L⇓ƛN) (λ ())
⇓ₑ-deterministic (⇓ₑ-app-● L⇓● M⇓V) (⇓ₑ-app-● L⇓●† M⇓V†) =
case ⇓ₑ-deterministic L⇓● L⇓●† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-if-true L⇓true M⇓V) (⇓ₑ-if-true L⇓true† M⇓V†) =
case ⇓ₑ-deterministic L⇓true L⇓true† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-if-true L⇓true _) (⇓ₑ-if-false L⇓false _) =
contradiction (⇓ₑ-deterministic L⇓true L⇓false) (λ ())
⇓ₑ-deterministic (⇓ₑ-if-true L⇓true _) (⇓ₑ-if-● L⇓●) =
contradiction (⇓ₑ-deterministic L⇓true L⇓●) (λ ())
⇓ₑ-deterministic (⇓ₑ-if-false L⇓false N⇓V) (⇓ₑ-if-false L⇓false† N⇓V†) =
case ⇓ₑ-deterministic L⇓false L⇓false† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic N⇓V N⇓V† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-if-false L⇓false _) (⇓ₑ-if-true L⇓true _) =
contradiction (⇓ₑ-deterministic L⇓false L⇓true) (λ ())
⇓ₑ-deterministic (⇓ₑ-if-false L⇓false _) (⇓ₑ-if-● L⇓●) =
contradiction (⇓ₑ-deterministic L⇓false L⇓●) (λ ())
⇓ₑ-deterministic (⇓ₑ-if-● L⇓●) (⇓ₑ-if-true L⇓true _) =
contradiction (⇓ₑ-deterministic L⇓● L⇓true ) (λ ())
⇓ₑ-deterministic (⇓ₑ-if-● L⇓●) (⇓ₑ-if-false L⇓false _) =
contradiction (⇓ₑ-deterministic L⇓● L⇓false) (λ ())
⇓ₑ-deterministic (⇓ₑ-if-● L⇓●) (⇓ₑ-if-● L⇓●†) =
case ⇓ₑ-deterministic L⇓● L⇓●† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-ref? M⇓V fresh _) (⇓ₑ-ref? M⇓V† fresh† _) =
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ →
case trans fresh (sym fresh†) of λ where
refl → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-ref?-● M⇓V) (⇓ₑ-ref?-● M⇓V†) =
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-deref M⇓a eq) (⇓ₑ-deref M⇓a† eq†) =
case ⇓ₑ-deterministic M⇓a M⇓a† of λ where
⟨ refl , refl ⟩ →
case trans (sym eq) eq† of λ where
refl → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-deref M⇓a _) (⇓ₑ-deref-● M⇓●) =
contradiction (⇓ₑ-deterministic M⇓a M⇓●) (λ ())
⇓ₑ-deterministic (⇓ₑ-deref-● M⇓●) (⇓ₑ-deref M⇓a _) =
contradiction (⇓ₑ-deterministic M⇓● M⇓a) (λ ())
⇓ₑ-deterministic (⇓ₑ-deref-● M⇓●) (⇓ₑ-deref-● M⇓●†) =
case ⇓ₑ-deterministic M⇓● M⇓●† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-assign? L⇓a M⇓V _) (⇓ₑ-assign? L⇓a† M⇓V† _) =
case ⇓ₑ-deterministic L⇓a L⇓a† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-assign? L⇓a _ _) (⇓ₑ-assign?-● L⇓● _) =
contradiction (⇓ₑ-deterministic L⇓a L⇓●) (λ ())
⇓ₑ-deterministic (⇓ₑ-assign?-● L⇓● _) (⇓ₑ-assign? L⇓a _ _) =
contradiction (⇓ₑ-deterministic L⇓● L⇓a) (λ ())
⇓ₑ-deterministic (⇓ₑ-assign?-● L⇓● M⇓V) (⇓ₑ-assign?-● L⇓●† M⇓V†) =
case ⇓ₑ-deterministic L⇓● L⇓●† of λ where
⟨ refl , refl ⟩ →
case ⇓ₑ-deterministic M⇓V M⇓V† of λ where
⟨ refl , refl ⟩ → ⟨ refl , refl ⟩