This commit is contained in:
Michael Zhang 2024-06-06 10:21:04 -04:00
parent d2afe9399c
commit e2897de4ca
5 changed files with 298 additions and 30 deletions

View file

@ -1,34 +1,26 @@
module ahmed.day1 where
module Ahmed.Day1 where
open import Agda.Primitive
open import Data.Nat
open import Data.Fin
open import Data.Product
open import Data.Empty
open import Data.Unit
open import Relation.Nullary using (Dec; yes; no)
data Type : Set where
Bool : Type
_-→_ : Type Type Type
data type : Set where
bool : type
_-→_ : type -> type -> type
data Term (n : ) : Set where
Var : (m : Fin n) Term n
True : Term n
False : Term n
If_Then_Else_ : Term n Term n Term n Term n
λ[_::_]_ : Term n Type Term n Term n
_∙_ : Term n Term n Term n
data term : Set where
true : term
data isValue (n : ) : Term n Set where
TrueValue : isValue n True
FalseValue : isValue n False
LambdaValue : (x : Term n) (τ : Type) (e : Term n) isValue n (λ[ x :: τ ] e)
data ctx : Set where
nil : ctx
cons : ctx -> type -> ctx
Value = (n : ) Σ (Term n) (isValue n)
data substitution : Set where
nil : substitution
cons : substitution -> term -> substitution
data evaluationContext : (n : ) Set where
dot : evaluationContext 0
EIf_Then_Else_ : {n : } evaluationContext n Term n Term n evaluationContext n
EAppLeft : {n : } evaluationContext n Term n evaluationContext n
EAppRight : {n : } Value evaluationContext n evaluationContext n
data isValidValueForType (n : ) (t : Type) : (e : Term n) Set where
TrueV : isValidValueForType n Bool True
isGoodSubstitution : (Γ : ctx) -> (γ : substitution) -> Set
isGoodSubstitution nil nil =
isGoodSubstitution nil (cons γ x) =
isGoodSubstitution (cons Γ x) nil =
isGoodSubstitution (cons Γ x) (cons γ x₁) = {! !}

77
ahmed/day1.fst Normal file
View file

@ -0,0 +1,77 @@
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()

View file

@ -372,3 +372,106 @@ $V_k db(tau_1 arrow tau_2) = {lambda (x : tau_1) . e | forall (j lt.eq k, v in V
$Epsilon_k db(tau) = { e | forall (j < k, e') arrow.r.double e op(mapsto)^j e' and "irreducible"(e') arrow.r.double e' in V_(k-j) db(tau)}$
What $k$ doesn't matter because the entire relations are universally quantified over all $k$s.
#pagebreak()
== Lecture 3
Step indexing history
- 2001: TOPLAS Andrew Appel https://dl.acm.org/doi/pdf/10.1145/504709.504712
- 2004: Mutable Refs
https://iris-project.org/
*Proof.* Prove the fundamental property for fold.
Case:
#tree(
axi[$Gamma tack.r e : subst(alpha, mu alpha . tau, tau)$],
uni[$Gamma tack.r "fold" e : mu alpha . tau$]
)
Show: $Gamma tack.r.double "fold" e : mu alpha . tau$
- Suppose $k >= 0$. Suppose $gamma in G_k db(Gamma)$
Need to show: $gamma ("fold" e) in Epsilon_k db(mu alpha . tau)$
This is $"fold" (gamma (e)) in Epsilon_k db(mu alpha . tau)$
- Suppose $"fold" (gamma (e)) op(mapsto)^(j < k) e' and "irreducible"(e')$
We need to show $e' in V_(k- j) db(mu alpha. tau)$
By operational semantics, $gamma(e) op(mapsto)^(j_1 <= j) e_1 and "irreducible"(e_1)$
By IH, $Gamma tack.r.double e : subst(alpha,mu alpha. tau , tau)$.
Instantiate this using our $k$ and $gamma in G_k db(Gamma)$: $gamma(e) in Epsilon_k db(subst(alpha ,mu alpha. tau, tau))$
However, we said it would, so instantiate the earlier with $gamma(e) mapsto e_1$, which is irreducible after $j_1$ steps.
$e_1 in V_(k-j_1) db(subst(alpha,mu alpha. tau, tau))$
Since $e_1$ is in a value relation, it's a value.
By operational semantics, $"fold" (gamma(e)) op(mapsto)^(j_1) "fold"(v_1)$. But from earlier supposition, $j = j_1$.
Now just need to show $"fold"(v_1)$ belongs to $V_(k-j) db(mu alpha. tau)$
- Using the rule, we have to show that $forall j' < k - j$, that $v_1 in V_(j') db(subst(alpha,mu alpha. tau , tau))$
Need monotonicity to prove this. If something behaves like a type for $k$ steps, it also behaves like that for fewer steps.
*Lemma (monotonicity / downward closure).*
$ v in V_k db(tau) => forall j <= k . v in V_j db(tau)
$
Prove this by induction on $V$.
*Homework.* Do the proof of monotonicity on the function case.
*Homework.* Prove the fundamental property with step indexing for lambda.
=== Mutable Refs
$tau ::= 1 | "bool" | tau_1 arrow tau_2 | "ref" tau$
$S : "Loc" harpoon C "Val"$
$e ::= angle.l angle.r | ... | "new" e | !e | e_1 := e_2$
$v ::= ... | l$
$E ::= ... | "new" E | ! E | E ::= e | v ::= E$
--
Operational semantics
- $(S , l := v) mapsto (S[l mapsto v], angle.l angle.r)$
- $(S "new" v) mapsto (S[l mapsto v])$
In java, you can't change the type of a storage cell. To prevent safety problems / getting stuck
=== Non-terminating program example with assignment
$"let" x = "new" (lambda (z : bb(1)) . z) \
"let" f = lambda (z : bb(1)) . (!x) z \
x := f ; \
f () ;
$
"Landin's Knot"
"Strong update" - language allows you to update a value of a cell with a different type.
Type = ${ I in P ( "CValue")}$
Type = ${ I in "Nat" -> P("CValue")}$
(CValue = Closed values)
$V_(k, S) db("ref" tau) = { l | l in V_(k-1) db(tau) }$

View file

@ -460,6 +460,8 @@ $Gamma$ can be multi-modal. This is how top-level declarations can be re-used.
https://www.cs.cmu.edu/~fp/papers/tocl07.pdf
https://arxiv.org/pdf/2402.01428v1
Need to enforce independence, that $Gamma tack.r e : A_m$ means $Gamma >= m$
Pointer:

View file

@ -472,6 +472,8 @@ Show these are the same by applying denesting and sliding.
=== Net KAT
https://www.cs.cornell.edu/~jnfoster/papers/frenetic-netkat.pdf
Net KAT is a special KAT. Think of networks as boxes the only thing they can do is get packets in, change something about the packet, and then sends the packet on.
Packets are records of fields $f_1, ..., f_k$ mapping to values $v_1, ..., v_k$. Program actions ($p = f arrow.l n$) and tests ($f = n$) come in pairs.
@ -491,3 +493,95 @@ For example:
Using KAT, you can perform network reachability.
]
#pagebreak()
== Lecture 4
NetKAT
- $f <- n$
- $f = n$
- "dup" (prev. known as observation) - takes a snapshot of what the packet looked like, so you can remember where it went throughout its lifetime
- (sw $<- 2 dot$ dup $dot$ sw $<- 5$)
- make claims like "an SSH packet never visited switch 3" by checking the trace
$db(.) : P -> 2^P$
- $db(f <- n)(pi) = { subst(f, n, pi) }$
- $db(f = n)(pi) = cases(emptyset "if" pi(f) eq.not n, {pi} "else")$
- $db(e + e')(pi) = db(e)(pi) union db(e')(pi)$
- $db(e\;f)(pi) = union.big_(pi' in db(e)(pi)) db(e')(pi')$
#let At = "At"
#let dup = "dup"
For NetKAT, $At tilde.equiv P $
=== Packet axioms
NetKat = KAT + Packet axioms:
- $f <- n ; f <- m equiv f <- m$
- $f <- n ; g <- m equiv g <- m ; f <- n$
- $f <- n ; g = m equiv g = m ; f <- n$
- $f <- n ; f = n equiv f <- n$
- $f = n ; f <- n equiv f = n$
- $sum_(n in "Val") f = n equiv 1$
- Says that every field has a value in it, but cannot have 2 values
- This is where finiteness of "Val" is important
- $f = n ; f = m equiv 0$
- $f = n ; dup equiv dup ; f = n$
With these axioms, you can prove:
$ db(e) = db(f) <=> e equiv f $
=== Match Action Table
Example:
#table(
columns: (auto, auto),
[Test], [Action],
[type = SSH], [drop],
[dst = 3], [pt $<-$ 5 + pt $<-$ 3],
)
Each of these can be written down as a NetKAT expression. This table is a big sum of tests and actions
The NetKAT expression corresponding to its behavior is
$ "sw" = k dot sum_e t_e ; a_e $
(This is an oversimplification, since the test order matters)
=== Network definition using NetKAT
- $"link"_(k j) = "sw" = k ; "pt" = 1 ; "sw" <- j ; "pt" <- 2$
- $"topology" = sum_"link" l_(k j)$
- $"switch" = sum_"sw" s_k$
- $"network" = ("topology" ; "switch")^*$
This is the definition of the entire network
=== Networking queries
==== Reachability queries
Ask for $"sw" = A ; ... ; "sw" = B$
Either A and B are directly connected by the topology, or take several steps and get to B.
$ "sw" = A ; "top" ; ("switch" ; "top")^* ; "sw" = B $
If this expression is $equiv 0$, then I know that A is not connected to B.
==== Forwarding Loop
This is when a packet goes in a cycle between nodes. Normally this is stopped with a TTL, which is decreased, and when it reaches 0 then the packet is ejected.
Instead, with NetKAT you can check if you have a forwarding loop.
$ alpha ; ("top" ; "switch") ; ("switch" ; "top")^* ; alpha $
- Temporal NetKAT for temporal properties https://www.cs.princeton.edu/~dpw/papers/temporal-netkat-pldi-2016.pdf