This commit is contained in:
Michael Zhang 2024-06-12 09:22:36 -04:00
parent e416d21387
commit c0191ea593
8 changed files with 256 additions and 157 deletions

View file

@ -1,78 +0,0 @@
module Ahmed.LogicalRelations where
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Fin
open import Data.Product
open import Relation.Nullary using (Dec; yes; no)
data type : Set where
bool : type
_-→_ : type type type
data ctx : Set where
nil : ctx
_,_ : ctx type ctx
data var : ctx type Set where
zero : {Γ τ} var (Γ , τ) τ
suc : {Γ τ₁ τ₂} var Γ τ₂ var (Γ , τ₁) τ₂
data term : ctx type Set where
true : {Γ} term Γ bool
false : {Γ} term Γ bool
`_ : {Γ τ} var Γ τ term Γ τ
λ[_]_ : {Γ τ₂} (τ₁ : type) (e : term (Γ , τ₁) τ₂) term Γ (τ₁ -→ τ₂)
_∙_ : {Γ τ₁ τ₂} term Γ (τ₁ -→ τ₂) term Γ τ₁ term Γ τ₂
length : ctx
length nil = zero
length (ctx , _) = suc (length ctx)
extend : {Γ Δ}
( {τ} var Γ τ var Δ τ)
( {τ₁ τ₂} var (Γ , τ₂) τ₁ var (Δ , τ₂) τ₁)
extend ρ zero = zero
extend ρ (suc c) = suc (ρ c)
rename : {Γ Δ}
( {τ} var Γ τ var Δ τ)
( {τ} term Γ τ term Δ τ)
rename ρ true = true
rename ρ false = false
rename ρ (` x) = ` (ρ x)
rename ρ (λ[ τ₁ ] c) = λ[ τ₁ ] rename (extend ρ) c
rename ρ (c c₁) = rename ρ c rename ρ c₁
extends : {Γ Δ}
( {τ} var Γ τ term Δ τ)
( {τ₁ τ₂} var (Γ , τ₂) τ₁ term (Δ , τ₂) τ₁)
extends σ zero = ` zero
extends σ (suc x) = rename suc (σ x)
subst : {Γ Δ}
( {τ} var Γ τ term Δ τ)
( {τ} term Γ τ term Δ τ)
subst ρ true = true
subst ρ false = false
subst ρ (` x) = ρ x
subst ρ (λ[ τ₁ ] x) = λ[ τ₁ ] subst (extends ρ) x
subst ρ (x x₁) = subst ρ x subst ρ x₁
_[_] : {Γ τ₁ τ₂} term (Γ , τ₂) τ₁ term Γ τ₂ term Γ τ₁
_[_] {Γ} {τ₁} {τ₂} e e₁ = subst σ e
where
σ : {τ} var (Γ , τ₂) τ term Γ τ
σ zero = e₁
σ (suc x) = ` x
data value : {Γ τ} term Γ τ Set where
true : {Γ} value {Γ} true
false : {Γ} value {Γ} false
λ[_]_ : {Γ τ₁ τ₂} {e : term (Γ , τ₁) τ₂} value (λ[ τ₁ ] e)
data step : {Γ τ} term Γ τ term Γ τ Set where
β-λ : {Γ τ₁ τ₂ v} (e : term (Γ , τ₁) τ₂) value v
step ((λ[ τ₁ ] e) v) (e [ v ])

View file

@ -1,4 +1,3 @@
{-# OPTIONS --prop #-}
module Ahmed.Day1 where module Ahmed.Day1 where
open import Agda.Builtin.Sigma open import Agda.Builtin.Sigma

View file

@ -1,77 +0,0 @@
module Day1
let var = int
type ty =
| TyBool
| TyArrow of ty * ty
type term =
| EVar of int
| ETrue
| EFalse
| EIfThenElse of term * term * term
| ELambda of ty * term
| EApp of term * term
type value =
| VTrue
| VFalse
| VLambda of ty * term
type evalctx =
| ECDot
| ECIfThenElse of evalctx * term * term
| ECAppL of evalctx * term
| ECAppR of value * evalctx
type step : term -> term -> Type =
| StepIfTrue : (e1 : term) -> (e2 : term) -> step (EIfThenElse (ETrue, e1, e2)) e1
| StepIfFalse : (e1 : term) -> (e2 : term) -> step (EIfThenElse (EFalse, e1, e2)) e2
let ctx = var -> option ty
let empty : ctx = fun _ -> None
let extend (t : ty) (g : ctx) : ctx = fun y -> if y = 0 then Some t else g (y - 1)
noeq type typing : ctx -> term -> ty -> Type =
| TypeTrue : (ctx : ctx) -> typing ctx ETrue TyBool
| TypeFalse : (ctx : ctx) -> typing ctx EFalse TyBool
| TypeIfThenElse : (ctx : ctx) -> (ty : ty)
-> (c : term) -> (e1 : term) -> (e2 : term)
-> typing ctx c TyBool
-> typing ctx e1 ty -> typing ctx e2 ty
-> typing ctx (EIfThenElse (c, e1, e2)) ty
let vRelation (ty : ty) (term : term) : prop =
match ty, term with
| (TyBool, ETrue) -> True
| (TyBool, EFalse) -> True
| _ -> False
let irred (term : term) : prop = admit()
let rec stepsToInNSteps (e1 : term) (e2 : term) (n : nat) : prop =
if n = 0 then False
else exists e' . (stepsToInNSteps e' e2 (n - 1) /\ (step e1 e'))
// let stepsTo (e1 : term) (e2 : term) : prop =
let eRelation (ty : ty) (term : term) : prop =
exists e' . irred e' /\ vRelation ty e'
let goodRelation (g : ctx) =
admit()
let subst (#ctx:ctx) (g : goodRelation ctx) (term : term) =
admit()
// let typeSoundness (ctx : ctx) (term : term) (ty : ty) : prop =
// forall (e' : )
let semanticSoundness (ctx : ctx) (term : term) (ty : ty) : prop =
forall (y : goodRelation ctx) . eRelation ty (subst y term)
let fundamentalProperty (#ctx : ctx) (#term : term) (#ty : ty)
(_ : typing ctx term ty) : semanticSoundness ctx term ty =
admit()

135
ahmed/day2.agda Normal file
View file

@ -0,0 +1,135 @@
module Ahmed.Day2 where
open import Agda.Builtin.Sigma
open import Data.Bool
open import Data.Empty
open import Data.Fin hiding (fold)
open import Data.Maybe
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Nullary
id : {A : Set} A A
id {A} x = x
data type : Set where
unit : type
bool : type
_-→_ : type type type
`_ : type
μ_ : type type
data term : Set where
`_ : term
`true : term
`false : term
`if_then_else_ : term term term term
`λ[_]_ : (τ : type) (e : term) term
_∙_ : term term term
`fold : term term
`unfold : term term
data ctx : Set where
nil : ctx
cons : ctx type ctx
lookup : ctx Maybe type
lookup nil _ = nothing
lookup (cons ctx₁ x) zero = just x
lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
data type-sub : Set where
nil : type-sub
type-subst : type type type
type-subst unit v = unit
type-subst bool v = bool
type-subst (τ -→ τ₁) v = (type-subst τ v) -→ (type-subst τ₁ v)
type-subst (` zero) v = v
type-subst (` suc x) v = ` x
type-subst (μ τ) v = μ (type-subst τ v)
data sub : Set where
nil : sub
cons : sub term sub
subst : term term term
subst (` zero) v = v
subst (` suc x) v = ` x
subst `true v = `true
subst `false v = `false
subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
subst (x x₁) v = (subst x v) (subst x₁ v)
subst (`fold x) v = `fold (subst x v)
subst (`unfold x) v = `unfold (subst x v)
data value-rel : type term Set where
v-`true : value-rel bool `true
v-`false : value-rel bool `false
v-`λ[_]_ : {τ e} value-rel τ (`λ[ τ ] e)
v-`fold : {τ e} value-rel (type-subst τ (μ τ)) e value-rel (μ τ) (`fold e)
data good-subst : ctx sub Set where
nil : good-subst nil nil
cons : {ctx τ γ v}
good-subst ctx γ
value-rel τ v
good-subst (cons ctx τ) γ
data step : term term Set where
step-if-1 : {e₁ e₂} step (`if `true then e₁ else e₂) e₁
step-if-2 : {e₁ e₂} step (`if `false then e₁ else e₂) e₂
step-`λ : {τ e v} step ((`λ[ τ ] e) v) (subst e v)
step-`fold : {v} step (`unfold (`fold v)) v
data steps : term term Set where
zero : {e} steps zero e e
suc : {e e' e''} (n : ) step e e' steps n e' e'' steps (suc n) e e''
data _⊢__ : ctx term type Set where
type-`true : {ctx} ctx `true bool
type-`false : {ctx} ctx `false bool
type-`ifthenelse : {ctx e e₁ e₂ τ}
ctx e bool
ctx e₁ τ
ctx e₂ τ
ctx (`if e then e₁ else e₂) τ
type-`x : {ctx x}
(p : Is-just (lookup ctx x))
ctx (` x) (to-witness p)
type-`λ : {ctx τ τ₂ e}
(cons ctx τ) e τ₂
ctx (`λ[ τ ] e) (τ -→ τ₂)
type-∙ : {ctx τ₁ τ₂ e₁ e₂}
ctx e₁ (τ₁ -→ τ₂)
ctx e₂ τ₂
ctx (e₁ e₂) τ₂
type-`fold : {ctx τ e}
ctx e (type-subst τ (μ τ))
ctx (`fold e) (μ τ)
type-`unfold : {ctx τ e}
ctx e (μ τ)
ctx (`unfold e) (type-subst τ (μ τ))
irreducible : term Set
irreducible e = ¬ ( λ e' step e e')
data term-relation : type term Set where
e-term : {τ e}
( {n} (e' : term) steps n e e' irreducible e' value-rel τ e')
term-relation τ e
type-sound : {Γ e τ} Γ e τ Set
type-sound {Γ} {e} {τ} s = {n} (e' : term) steps n e e' value-rel τ e' λ e'' step e' e''
_⊨__ : (Γ : ctx) (e : term) (τ : type) Set
_⊨__ Γ e τ = (γ : sub) (good-subst Γ γ) term-relation τ e
fundamental : {Γ e τ} (well-typed : Γ e τ) type-sound well-typed Γ e τ
fundamental {Γ} {e} {τ} well-typed type-sound γ good-sub = e-term f
where
f : {n : } (e' : term) steps n e e' irreducible e' value-rel τ e'
f e' steps irred = [ id , (λ exists ⊥-elim (irred exists)) ] (type-sound e' steps)

View file

@ -2,3 +2,46 @@
#import "@preview/prooftrees:0.1.0": * #import "@preview/prooftrees:0.1.0": *
#show: doc => conf("Language-Based Security", doc) #show: doc => conf("Language-Based Security", doc)
Security labels
Flow relations
- If $l_1 subset.sq.eq l_2$ then information is allowed to flow from $l_1$ to $l_2$
- This should be reflexive and transitive
- *NOT* be symmetric
- This is known as a _pre-order_
- We may also want to add anti-symmetry, which makes it a _partial order_
- Actually, we could use a join-semi-lattice. (Denning 1978)
- _Unique_ least upper bound operation
- If we didn't have least upper bound, then $c = a plus.circle b ; d_1 = c; d_2 = c$ may not work
More general form of non-interference:
- Lattice $(Lambda, subset.sq.eq)$ of security levels
- Using this, Program $c$ is non-interfering if:
- $forall sigma_1, sigma_2, sigma'_1, sigma'_2, l in Lambda => \
"if" sigma_1 op(=)_l sigma_2 "and" angle.l c, sigma_1 angle.r arrow.b.double sigma'_1 "and" angle.l c, sigma_2 angle.r arrow.b.double sigma'_2 \
"then" sigma'_1 op(=)_l sigma'_2$
=== Threat model
Information channels convey information
Categorized into (Lampson 1973)
- Legitimate channels
- Covert channels (and side channels)
=== Interaction
Adding to IMP:
$
x := ... | "input from" l | "output" x "to" l \
"Trace" in.rev tau ::= epsilon | tau dot "in"(n, l) | tau dot "out"(n, l)
$
Trace is a sequence of events
New non-interference, based on traces. The execution trace needs to be the same!

2
experiments/tc.agda Normal file
View file

@ -0,0 +1,2 @@
module Experiments.Tc where

View file

@ -136,3 +136,63 @@ _Answer._ Any time you add a syntactic construct, it comes at a price.
- Stan https://en.wikipedia.org/wiki/Stan_(software) - Stan https://en.wikipedia.org/wiki/Stan_(software)
- https://www.tensorflow.org/probability Google - https://www.tensorflow.org/probability Google
- https://pyro.ai/ Uber - https://pyro.ai/ Uber
=== Tiny Cond
Observe, can prune worlds that can't happen.
Un-normalized semantics where the probabilities of things don't sum to 1.
#let observe = "observe"
$ db(observe p \; e) (rho) (v) = cases(
db(e) (rho) (v) "if" db(p) (rho) = tt,
0 "else",
) $
To normalize, divide by the sum
$ db(e)(rho)(v) = frac(db(e) (rho) (v), db(e) (rho) (tt) + db(e) (rho) (ff)) $
== Operational sampling semantics
Expectation of a random variable, $EE$
$ EE_Pr[f] = sum^N_w Pr(w) times f(w) \
approx 1/N sum^N_(w tilde Pr) f(w)
$
Approximate with a finite sample, where $w$ ranges over the sample
To prove our runtime strategy sound, we're going to relate it to an _expectation_.
https://en.wikipedia.org/wiki/Concentration_inequality
=== Big step semantics
#let bigstep(sigma, e, v) = $#sigma tack.r #e arrow.b.double #v$
$ sigma tack.r angle.l e . rho angle.r arrow.b.double v $
$tack.r$ read as "in the context of"
We externalized the randomness and put it all in $sigma$
This is like pattern matching:
$ v :: bigstep(sigma, flip 1/2, v )$
== Lecture 3
=== Rejection sampling
=== Search
$x <- flip 1/2 \
y <- ifthenelse(x, flip 1/3, flip 1/4) \
z <- ifthenelse(y, flip 1/6, flip 1/7) \
ret z$
You can draw a search tree of probabilities. Add up the probabilities to get the probability that a program returns a specific value.
You can share $z$ since it doesn't depend directly on $x$. This builds a *binary decision diagram*.

15
zdancewic/monads.agda Normal file
View file

@ -0,0 +1,15 @@
{-# OPTIONS --guardedness #-}
{-# OPTIONS --type-in-type #-}
module Zdancewic.Monads where
open import Agda.Primitive
open import Data.Nat
record ITree (E : Set Set) (R : Set) : Set where
coinductive
field
ret : R
tau : ITree E R
vis : {A} (e : E A) (A ITree E R)