more progress on proof

2024-06-10 22:56:36 -04:00 · 2024-06-10 22:56:36 -04:00 · be266049f0
parent 100db8f8f0
commit be266049f0
10 changed files with 407 additions and 58 deletions
--- 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 τ {!   !}
+_⊨_∶_ : (Γ : 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)
--- 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)}$
+$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
--- 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'$],
-)
+)
+
+#pagebreak()
+
+== Lecture 2
+
+- Language Definition
+- Compilation to circuits
+- Example weak simulation + refinement theorem
--- a/chong/notes.typ
+++ b/chong/notes.typ
@ -0,0 +1,4 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("Language-Based Security", doc)
+
--- a/holtzen/notes.typ
+++ 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
--- a/stoughton/example1
+++ 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;
+  }
+}
--- a/stoughton/notes.typ
+++ 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/
+
--- a/zdancewic/Day1.agda
+++ 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
--- a/zdancewic/Day1.v
+++ 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 :=
+.
--- a/zdancewic/notes.typ
+++ 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
+