From ed0cee996a2c46811ba540d00fabcd1b572b89a1 Mon Sep 17 00:00:00 2001 From: Tianyu Chen Date: Sun, 17 Mar 2024 23:43:41 -0400 Subject: [PATCH] check --- src/Security/SimRel.agda | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/Security/SimRel.agda b/src/Security/SimRel.agda index 2d89778..41d7a02 100644 --- a/src/Security/SimRel.agda +++ b/src/Security/SimRel.agda @@ -142,3 +142,19 @@ data _⊢_≤_⇐_ : Label → Term → CCTerm → Type → Set where → ⊢ PC ⇐ g₂ -------------------------------------------- → g₁ ⊢ prot ℓ′ M′ ≤ protect PC v ℓ M A ⇐ B + + +≤-value-pc : ∀ {g₁ g₂ M V A} + → g₁ ⊢ M ≤ V ⇐ A + → Value V + -------------------------------- + → g₂ ⊢ M ≤ V ⇐ A +≤-value-pc (≤-addr x) (V-raw V-addr) = ≤-addr x +≤-value-pc (≤-lam x y) (V-raw V-ƛ) = ≤-lam x y +≤-value-pc (≤-const x) (V-raw V-const) = ≤-const x +≤-value-pc (≤-wrapped-addr 𝓋 x) (V-cast V-addr x₁) = ≤-wrapped-addr 𝓋 x +≤-value-pc (≤-cast (≤-addr x)) (V-cast V-addr i) = ≤-cast (≤-addr x) +≤-value-pc (≤-wrapped-lam M≤V 𝓋 x) (V-cast V-ƛ i) = ≤-wrapped-lam M≤V 𝓋 x +≤-value-pc (≤-cast (≤-lam M≤V x)) (V-cast V-ƛ i) = ≤-cast (≤-lam M≤V x) +≤-value-pc (≤-wrapped-const 𝓋 x y) (V-cast V-const x₁) = ≤-wrapped-const 𝓋 x y +≤-value-pc (≤-cast (≤-const x)) (V-cast V-const x₁) = ≤-cast (≤-const x)