From be266049f0d723806b6bbde7d25953e32af498a9 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 10 Jun 2024 22:56:36 -0400
Subject: [PATCH] more progress on proof

---
 ahmed/day1.agda     | 176 ++++++++++++++++++++++++++++++--------------
 ahmed/notes.typ     |  39 +++++++++-
 bourgeat/notes.typ  |  10 ++-
 chong/notes.typ     |   4 +
 holtzen/notes.typ   | 138 ++++++++++++++++++++++++++++++++++
 stoughton/example1  |  19 +++++
 stoughton/notes.typ |   6 ++
 zdancewic/Day1.agda |  30 ++++++++
 zdancewic/Day1.v    |  20 +++++
 zdancewic/notes.typ |  23 ++++++
 10 files changed, 407 insertions(+), 58 deletions(-)
 create mode 100644 chong/notes.typ
 create mode 100644 holtzen/notes.typ
 create mode 100644 stoughton/example1
 create mode 100644 stoughton/notes.typ
 create mode 100644 zdancewic/Day1.agda
 create mode 100644 zdancewic/Day1.v
 create mode 100644 zdancewic/notes.typ

diff --git a/ahmed/day1.agda b/ahmed/day1.agda
index c2594e8..d5fbe05 100644
--- a/ahmed/day1.agda
+++ b/ahmed/day1.agda
@@ -1,79 +1,143 @@
 {-# OPTIONS --prop #-}
 module Ahmed.Day1 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)
 import Relation.Binary.PropositionalEquality as Eq
+open import Agda.Builtin.Sigma
+open import Data.Bool
+open import Data.Empty
+open import Data.Fin
+open import Data.Maybe
+open import Data.Nat
+open import Data.Product
+open import Data.Sum
+open import Data.Unit
+open import Relation.Nullary
+
 open Eq using (_≡_; refl; trans; sym; cong; cong-app)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
+
+id : {A : Set} → A → A
+id {A} x = x
 
 data type : Set where
   bool : type
   _-→_ : type → type → type
 
-data ctx : ℕ → Set where
-  nil : ctx zero
-  _,_ : ∀ {n} → ctx n → type → ctx (suc n)
+data term : Set where
+  `_ : ℕ → term
+  `true : term
+  `false : term
+  `if_then_else_ : term → term → term → term
+  `λ[_]_ : (τ : type) → (e : term) → term
+  _∙_ : term → term → term
 
-data term : (n : ℕ) → Set where
-  `_ : ∀ {n} → (m : Fin n) → term n
-  true : ∀ {n} → term n
-  false : ∀ {n} → term n
-  λ[_]_ : ∀ {n} → (τ₁ : type) (e : term (suc n)) → term n
-  _∙_ : ∀ {n} → term n → term n → term n
+data ctx : Set where
+  nil : ctx
+  cons : ctx → type → ctx
 
-postulate
-  lookup : ∀ {n} → Fin n → ctx n → type
--- lookup {n} Γ 
+lookup : ctx → ℕ → Maybe type
+lookup nil _ = nothing
+lookup (cons ctx₁ x) zero = just x 
+lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
 
-data typing : ∀ {n} {Γ : ctx n} → term n → type → Set where
-  `_ : ∀ {n Γ τ} → (m : Fin n) → lookup m Γ ≡ τ → typing {n} {Γ} (` m) τ
-  true : ∀ {n Γ} → typing {n} {Γ} true bool
-  false : ∀ {n Γ} → typing {n} {Γ} false bool
+data sub : Set where
+  nil : sub
+  cons : sub → term → sub
 
-data is-value : ∀ {n} → (e : term n) → Set where
-  true : ∀ {n} → is-value {n} true
-  false : ∀ {n} → is-value {n} false
-  λ[_]_ : ∀ {n} → (τ : type) → (e : term (suc n)) → is-value {n} (λ[ τ ] e)
+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)
 
-value = ∀ {n} → Σ (term n) (is-value)
+data value-rel : type → term → Set where 
+  v-`true : value-rel bool `true
+  v-`false : value-rel bool `false
+  v-`λ[_]_ : ∀ {τ e} → value-rel τ (`λ[ τ ] e)
 
-lift-term : ∀ {n} → term n → term (suc n)
-lift-term {n} (` m) = ` (suc m)
-lift-term {n} true = true
-lift-term {n} false = false
-lift-term {n} (λ[ τ₁ ] e) = λ[ τ₁ ] lift-term e
-lift-term {n} (e ∙ e₁) = lift-term e ∙ lift-term 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 τ) γ
 
-subst : ∀ {n} → (e : term (suc n)) → (v : term n) → term n
-subst {n} (` zero) v = v
-subst {n} (` suc m) v = ` m
-subst true v = true
-subst false v = false
-subst (λ[ τ ] e) v = λ[ τ ] subst e (lift-term v)
-subst (e₁ ∙ e₂) v = subst e₁ v ∙ subst e₂ v
+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)
 
-data step : ∀ {n} → term n → term n → Set where
-  β-step : ∀ {n τ e e₂} → step {n} ((λ[ τ ] e) ∙ e₂) (subst e e₂)
+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''
 
--- irreducible : ∀ {n} → (e : term) → ∃[ e' ] mapsto e'
+data well-typed : ctx → term → type → Set where
+  type-`true : ∀ {ctx} → well-typed ctx `true bool
+  type-`false : ∀ {ctx} → well-typed ctx `false bool
+  type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
+    → well-typed ctx e bool
+    → well-typed ctx e₁ τ
+    → well-typed ctx e₂ τ
+    → well-typed ctx (`if e then e₁ else e₂) τ
+  type-`x : ∀ {ctx x}
+    → (p : Is-just (lookup ctx x))
+    → well-typed ctx (` x) (to-witness p)
+  type-`λ : ∀ {ctx τ τ₂ e}
+    → well-typed (cons ctx τ) e τ₂
+    → well-typed ctx (`λ[ τ ] e) (τ -→ τ₂)
+  type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
+    → well-typed ctx e₁ (τ₁ -→ τ₂)
+    → well-typed ctx e₂ τ₂
+    → well-typed ctx (e₁ ∙ e₂) τ₂
 
--- type-soundness : ∀ {e τ} → 
+_⊢_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
+Γ ⊢ e ∶ τ = (well-typed Γ e τ) × (∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e'')
 
-value-relation : ∀ {n} → (τ : type) → (e : term n) → Set
-expr-relation : ∀ {n} → (τ : type) → (e : term n) → Set
+irreducible : term → Set
+irreducible e = ¬ (∃ λ e' → step e e')
 
-value-relation bool true = ⊤
-value-relation bool false = ⊤
-value-relation (τ₁ -→ τ₂) ((λ[ τ ] e) ∙ v) = expr-relation τ₂ {!   !}
-value-relation _ _ = ⊥
- 
-expr-relation {n} τ 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
 
-semantic-soundness : ∀ {n} (Γ : ctx n) → (τ : type) → (e : term n) → Set  
--- semantic-soundness {n} Γ τ e = (γ : substitution n) → expr-relation τ {!   !}
\ No newline at end of file
+_⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
+_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-relation τ e
+
+fundamental : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Γ ⊨ e ∶ τ
+fundamental {Γ} {`true} {bool} type-sound γ good-sub = e-term λ e' steps irred →
+  [ id , (λ exists → ⊥-elim (irred exists)) ] (snd type-sound e' steps)
+fundamental {Γ} {`false} {bool} type-sound γ good-sub = e-term λ e' steps irred →
+  [ id , (λ exists → ⊥-elim (irred exists)) ] (snd type-sound e' steps)
+fundamental {Γ} {`λ[ τ ] e} {τ₁ -→ τ₂} 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)) ] (snd type-sound e' steps)
+
+fundamental {Γ} {`if e then e₁ else e₂} {τ} type-sound γ good-sub = e-term f
+  where
+    f : {n : ℕ} (e' : term) → steps n (`if e then e₁ else e₂) e' → irreducible e' → value-rel τ e'
+    f .(`if e then e₁ else e₂) zero irred =
+      let
+        ts : well-typed Γ (`if e then e₁ else e₂) τ
+        ts = fst type-sound 
+        ts2 = snd type-sound 
+      in ⊥-elim (irred {!   !})
+    f e' (suc n x steps₁) irred = {!   !}
+fundamental {Γ} {` x} {τ} type-sound γ good-sub = {!   !}
+fundamental {Γ} {e ∙ e₁} {τ} type-sound γ good-sub = {!   !}
+
+-- fundamental {Γ} {`true} {τ -→ τ₁} type-sound γ good-sub = e-term f
+--   where
+--     el : ∀ {A} → well-typed Γ `true (τ -→ τ₁) → A
+--     el ()
+--     f : {n : ℕ} (e' : term) → steps n `true e' → irreducible e' → value-rel (τ -→ τ₁) e'
+--     f e' steps irred = el (fst type-sound)
+-- fundamental {Γ} {`false} {τ -→ τ₁} type-sound γ good-sub = e-term f
+--   where
+--     el : ∀ {A} → well-typed Γ `false (τ -→ τ₁) → A
+--     el ()
+--     f : {n : ℕ} (e' : term) → steps n `false e' → irreducible e' → value-rel (τ -→ τ₁) e'
+--     f e' steps irred = el (fst type-sound)
\ No newline at end of file
diff --git a/ahmed/notes.typ b/ahmed/notes.typ
index 354270a..bca2717 100644
--- a/ahmed/notes.typ
+++ b/ahmed/notes.typ
@@ -481,4 +481,41 @@ $V_(k, S) db("ref" tau) = { l | l in V_(k-1) db(tau) }$
 
 == Lecture 4
 
-$V_k db(ref tau) = { l | S(L) in V db(tau)}$
\ No newline at end of file
+$V_k db(ref tau) = { l | S(L) in V db(tau)}$
+
+#pagebreak()
+
+== Lecture 5
+
+Talking about relations between pairs of values.
+
+$V db(tau) = { (v_1, v_2) | ... }$ \
+$Epsilon db(tau) = { (e_1, e_2) | ... }$
+
+Proofs of contextual equivalences are difficult to do. FOr example, consider this case:
+
+$lambda x. ... [ ] ...$
+
+Tough to reason about holes inside of a lambda, even with induction on contexts.
+
+Instead, set up a binary logical relation, and prove:
+
+$Gamma tack.r e_1 approx e_2 : tau = forall gamma_1, gamma_2 in G db(tau) ==> (gamma_1 (e_1) , gamma_2 (e_2)) in Epsilon db(tau)$
+
+Not just useful for relations between programs in the same language, but also programs in two different languages.
+
+To do step indexing, you can only count steps on one side. Then in that case, it would only be an approximation relation. To prove equivalence, you would have to show that one side approximates the other and vice versa separately.
+
+Logical relations using step indexing with no types:
+
+$ V_k = &{ "true" , "false" } \
+union &{lambda x.e | forall j < k , forall v in V_j => subst(x,v,e) in Epsilon_j} \
+$
+
+This is sound because the step index is going down.
+
+https://www.khoury.northeastern.edu/home/amal/papers/next700ccc.pdf
+
+https://www.khoury.northeastern.edu/home/amal/papers/impselfadj.pdf
+
+Matthews-Findler '07: https://users.cs.northwestern.edu/~robby/pubs/papers/popl2007-mf-color.pdf
\ No newline at end of file
diff --git a/bourgeat/notes.typ b/bourgeat/notes.typ
index b83fc7e..00539cf 100644
--- a/bourgeat/notes.typ
+++ b/bourgeat/notes.typ
@@ -99,4 +99,12 @@ Compose $M_1$, $M_2$, and $M_3$ into a bigger module.
 #tree(
   axi[$(m, f("arg"), m') in "enq"_M$],
   uni[$m."deq"("arg") --> m'$],
-)
\ No newline at end of file
+)
+
+#pagebreak()
+
+== Lecture 2
+
+- Language Definition
+- Compilation to circuits
+- Example weak simulation + refinement theorem
diff --git a/chong/notes.typ b/chong/notes.typ
new file mode 100644
index 0000000..f14d030
--- /dev/null
+++ b/chong/notes.typ
@@ -0,0 +1,4 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("Language-Based Security", doc)
+
diff --git a/holtzen/notes.typ b/holtzen/notes.typ
new file mode 100644
index 0000000..bfb1923
--- /dev/null
+++ b/holtzen/notes.typ
@@ -0,0 +1,138 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("Probabilistic Programming", doc)
+#import "@preview/simplebnf:0.1.0": *
+
+#let prob = "probability"
+#let tt = "tt"
+#let ff = "ff"
+#let tru = "true"
+#let fls = "false"
+#let ret = "return"
+#let flip = "flip"
+#let real = "real"
+#let Env = "Env"
+#let Bool = "Bool"
+#let dbp(x) = $db(#x)_p$
+#let dbe(x) = $db(#x)_e$
+#let sharpsat = $\#"SAT"$
+#let sharpP = $\#"P"$
+
+- Juden Pearl - Probabilistic graphical models
+
+*Definition.* Probabilistic programs are programs that denote #prob distributions.
+
+Example:
+
+```
+x <- flip 1/2
+x <- flip 1/2
+return x if y
+```
+
+$x$ is a random variable that comes from a coin flip. Instead of having a value, the output is a _function_ that equals
+
+$ 
+db( #[```
+  x <- flip 1/2
+  x <- flip 1/2
+  return x if y
+```]
+) 
+=
+cases(tt mapsto 3/4, ff mapsto 1/4) $
+
+tt is "semantic" true and ff is "semantic" false
+
+Sample space $Omega = {tt, ff}$, #prob distribution on $Omega$ -> [0, 1]
+
+Semantic brackets $db(...)$
+
+=== TinyPPL
+
+Syntax
+
+$
+#bnf(
+  Prod( $p$, annot: $sans("Pure program")$, {
+    Or[$x$][_variable_]
+    Or[$ifthenelse(p, p, p)$][_conditional_]
+    Or[$p or p$][_conjunction_]
+    Or[$p and p$][_disjunction_]
+    Or[$tru$][_true_]
+    Or[$fls$][_false_]
+    Or[$e$ $e$][_application_]
+  }),
+)
+$
+
+$
+#bnf(
+  Prod( $e$, annot: $sans("Probabilistic program")$, {
+    Or[$x arrow.l e, e$][_assignment_]
+    Or[$ret p$][_return_]
+    Or[$flip real$][_random_]
+  }),
+)
+$
+
+Semantics of pure terms
+
+- $dbe(p) : Env -> Bool$
+- $dbe(x) ([x mapsto tt]) = tt$
+- $dbe(tru) (rho) = tt$
+- $dbe(p_1 and p_2) (rho) = dbe(p_1) (rho) and dbe(p_2) (rho)$
+  - the second $and$ is a "semantic" $and$
+
+env is a mapping from identifiers to B
+
+Semantics of probabilistic terms
+
+- $dbe(e) : Env -> ({tt, ff} -> [0, 1])$
+- $dbe(flip 1/2) (rho) = [tt mapsto 1/2, ff mapsto 1/2]$
+- $dbe(ret p) (rho) = v mapsto cases(1 "if" dbp(p) (rho) = v, 0 "else")$
+// - $dbe(x <- e_1 \, e_2) (rho) = dbp(e_2) (rho ++ [x mapsto dbp(e_1)])$
+- $dbe(x <- e_1 \, e_2) (rho) = v' mapsto sum_(v in {tt, ff}) dbe(e_1) (rho) (v) times db(e_2) (rho [x mapsto v])(v')$
+  - "monadic semantics" of PPLs
+  - https://homepage.cs.uiowa.edu/~jgmorrs/eecs762f19/papers/ramsay-pfeffer.pdf
+  - https://www.sciencedirect.com/science/article/pii/S1571066119300246
+
+Getting back a probability distribution
+
+=== Tractability
+
+What is the complexity class of computing these? #sharpP
+
+- Input: boolean formula $phi$
+- Output: number of solutions to $phi$
+  - $sharpsat(x or y) = 3$
+
+https://en.wikipedia.org/wiki/Toda%27s_theorem
+
+This language is actually incredibly intractable. There is a reduction from TinyPPL to #sharpsat
+
+Reduction:
+
+- Given a formula like $phi = (x or y) and (y or z)$
+- Write a program where each variable is assigned a $flip 1/2$:
+
+  $x <- flip 1\/2 \
+  y <- flip 1\/2 \
+  z <- flip 1\/2 \
+  ret (x or y) and (y or z)$
+
+How hard is this?
+
+$#sharpsat (phi) = 2^("# vars") times db("encoded program") (emptyset) (tt)$
+
+*Question.* Why do we care about the computational complexity of our denotational semantics?
+_Answer._ Gives us a lower bound on our operational semantics.
+
+*Question.* What's the price of adding features like product/sum types?
+_Answer._ Any time you add a syntactic construct, it comes at a price.
+
+=== Systems in the wild
+
+- Stan https://en.wikipedia.org/wiki/Stan_(software)
+- https://www.tensorflow.org/probability Google
+- https://pyro.ai/ Uber
\ No newline at end of file
diff --git a/stoughton/example1 b/stoughton/example1
new file mode 100644
index 0000000..4235220
--- /dev/null
+++ b/stoughton/example1
@@ -0,0 +1,19 @@
+type key. (* encryption keys, key_len bits *)
+type text. (* plaintexts, text_len bits *)
+type cipher. (* ciphertexts *)
+
+module type ENC = {
+  proc key_gen(): key
+  proc enc(k: key, x: text): cipher
+  proc dec(k: key, c: cipher): text
+}
+
+module Cor (Enc: ENC) = {
+  proc main(x: text): bool = {
+    var k: key; var c: cipher; var y: text;
+    k <@ Enc.key_gen();
+    c <@ Enc.enc(k, x);
+    y <@ Enc.dec(k, c);
+    return x = y;
+  }
+}
\ No newline at end of file
diff --git a/stoughton/notes.typ b/stoughton/notes.typ
new file mode 100644
index 0000000..0e354bc
--- /dev/null
+++ b/stoughton/notes.typ
@@ -0,0 +1,6 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("The Real/Ideal Paradigm", doc)
+
+https://formosa-crypto.gitlab.io/projects/
+
diff --git a/zdancewic/Day1.agda b/zdancewic/Day1.agda
new file mode 100644
index 0000000..5279089
--- /dev/null
+++ b/zdancewic/Day1.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --prop #-}
+
+module Zdancewic.Day1 where
+
+open import Data.Bool
+open import Data.Nat
+open import Data.String
+
+mem = String -> ℕ
+
+infixl 20 _∙_
+
+data aexp : Set where
+data bexp : Set where
+data com : Set where
+  `_:=_ : String → ℕ → com
+  `if_then_else_ : bexp → com → com → com
+  `skip : com
+  _∙_ : com → com → com
+
+beval : mem → bexp → Bool
+
+denote : com → mem → mem
+denote `skip st = st
+denote (`if x then c else c₁) st = if beval st x then denote c st else denote c₁ st
+denote (` x := n) st = λ y → if x == y then n else st x
+denote (c ∙ c₁) st = denote c₁ (denote c st)
+
+data ceval : com → mem → mem → Prop where
+  E_skip : ∀ {st} → ceval `skip st st
\ No newline at end of file
diff --git a/zdancewic/Day1.v b/zdancewic/Day1.v
new file mode 100644
index 0000000..98a7af3
--- /dev/null
+++ b/zdancewic/Day1.v
@@ -0,0 +1,20 @@
+Require Import Coq.Strings.String.
+
+Module Day1.
+
+Inductive aexp : Type :=
+.
+
+Inductive bexp : Type :=
+.
+
+Inductive com : Type :=
+  | CSkip
+  | CAssign (x : string) (a : aexp)
+  | CSeq (c1 c2 : com)
+  | CIf (b : bexp) (c1 c2 : com)
+  | CWhile (b : bexp) (c : com)
+.
+
+Fixpoint aeval (m : mem) (a : aexp) : nat :=
+.
\ No newline at end of file
diff --git a/zdancewic/notes.typ b/zdancewic/notes.typ
new file mode 100644
index 0000000..51029a9
--- /dev/null
+++ b/zdancewic/notes.typ
@@ -0,0 +1,23 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("Steve Zdancewic", doc)
+
+- Reasoning about monadic programs in Coq
+- 
+
+Imp
+
+```
+Inductive com : Type :=
+  | CSkip
+  | CAssign (x : string) (a : aexp)
+  | CSeq (c1 c2 : com)
+  | CIf (b : bexp) (c1 c2 : com)
+  | CWhile (b : bexp) (c : com)
+.
+```
+
+"Relationally defined operational semantics"
+
+State monad
+