forked from jonsterling/agda-calf
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Noninterference.agda
55 lines (46 loc) · 1.64 KB
/
Noninterference.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
{-# OPTIONS --prop --without-K --rewriting #-}
-- Theorems about noninterference.
open import Calf.CostMonoid
module Calf.Noninterference (costMonoid : CostMonoid) where
open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.Step costMonoid
open import Calf.PhaseDistinction
open import Calf.Types.Eq
open import Data.Product
open import Relation.Binary.PropositionalEquality as P
oblivious : ∀ {A B} (f : cmp (F A) → val (◯⁺ B)) →
∀ c e → f (step (F A) c e) ≡ f e
oblivious {A} {B} f c e = funext/Ω (λ u →
begin
f (step (F A) c e) u ≡⟨ cong (λ e → f e u) (step/ext (F A) e c u) ⟩
f e u
∎
)
where open ≡-Reasoning
unique : ∀ {A} → (a : val (● A)) → (u : ext) → a ≡ ∗ u
unique {A} a u =
eq/ref
(●/ind {A} a (λ a → F (eq (● A) a (∗ u)))
(λ a → ret (eq/intro (η≡∗ a u)))
(λ u → ret (eq/intro refl))
(λ a u → eq/uni _ _ u))
constant : ∀ {A B} (f : val (● A) → val (◯⁺ B)) →
Σ (val (◯⁺ B)) λ b → f ≡ λ _ → b
constant f =
(λ u → f (∗ u) u) , funext (λ a → funext/Ω (λ u →
P.cong (λ a → f a u) (unique a u)))
optimization : ∀ {C B : tp pos} {A : val C → tp pos}
(f : val (Σ++ C λ c → ● (A c)) → val (◯⁺ B)) →
Σ (val C → val (◯⁺ B)) λ f' → ∀ c a → f (c , a) ≡ f' c
optimization {C} {B} {A} f =
(λ c →
let g : val (● (A c)) → val (◯⁺ B)
g a = f (c , a) in
let (b , h) = constant {A c} {B} g in
b) ,
λ c a →
let g : val (● (A c)) → val (◯⁺ B)
g a = f (c , a) in
let (b , h) = constant {A c} {B} g in
P.cong-app h a