D1

Success stories:

ironfleet
rustbelt
fscq	File system	MIT	Coq
sel4
certikos
compcert	C compiler
cakeml	Compiler for ML subset		HOL
bedrock2
iris

Monadic => effectful

—

What does it mean for two monadic computations to be equivalent?

Imp

Syntax
Memory
Semantics
- One way: Give an interpreter. ie, denosem
  - Can't define straightforwardly ∵ of while termination not being evident.
  - Problem: Partiality
- Another way: relational operational semantics
  - Currently going with large step
  - small step also possible?? cf: SF book

Cons of large step:

Recursion for while is not defined on the structure of term syntax. Have to use a diff kind of reasoning
Is partial
Isn't executable
Is a deep embedding => can't use coq's meta-theory. Got to roll our own.

denosem attempt and big-step: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html
small-step: https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html

a := n 
   | a + a
   | a - a
   | a * a

b := true | false
   | ¬b
   | b ∧ b 
   | a = a | a ≠ a
   | a ≤ a | a > a

c := skip
   | x := a
   | c ; c
   | if b then c else c end
   | while b do c end

⟦n⟧ = n
⟦a1 + a2⟧ = ⟦a1⟧ + ⟦a2⟧
⟦a1 - a2⟧ = ⟦a1⟧ - ⟦a2⟧
⟦a1 * a2⟧ = ⟦a1⟧ * ⟦a2⟧

⟦true⟧ = true
⟦false⟧ = false
⟦¬b⟧ = ¬⟦b⟧
⟦b1 ∧ b2⟧ = ⟦b1⟧ ∧ ⟦b2⟧
⟦a1 = a2⟧ = ⟦a1⟧ == ⟦a2⟧
⟦a1 ≠ a2⟧ = ¬(⟦a1⟧ == ⟦a2⟧)
⟦a1 ≤ a2⟧ = ⟦a1⟧ <= ⟦a2⟧
⟦a1 > a2⟧ = ⟦a1⟧ > ⟦a2⟧

(* st is state *)
⟦skip⟧(st) = st
⟦x := a⟧(st) = st[x ↦ ⟦a⟧]
⟦c1; c2⟧(st) = ⟦c2⟧(⟦c1⟧(st))
⟦if b then c1 else c2⟧(st) = if ⟦b⟧==true then ⟦c1⟧(st) else ⟦c2⟧(st)
⟦while b do c end⟧(st) = if ⟦b⟧==true then ⟦c;(while b do c end)⟧(st) else st

⟦while⟧ is not well founded.

Operational semantics (big-step, aka natural semantics):


--------------
(σ, skip) ⇓ σ


    a⇓ₐv
------------------
(σ, x:=a) ⇓ σ[x↦v]


(σ1,c1)⇓σ'  (σ',c2)⇓σ2
----------------------
   (σ1, c1;c2)⇓σ2


  b⇓true          (σ,c1)⇓σ'          b⇓false          (σ,c2)⇓σ'     
------------------------------     ------------------------------     
(σ, if b then c1 else c2) ⇓ σ'     (σ, if b then c1 else c2) ⇓ σ'     


    b⇓false     (σ,c)⇓σ'
-------------------------------
  (σ, while b do c end) ⇓ σ'



    b⇓true     (σ,c)⇓σ'   (σ', while b do c end)⇓σ''
-----------------------------------------------------
          (σ, while b do c end) ⇓ σ''

Monad

states
state monads

Think of monad as a generalized let.

'Well-behaved sequential composition'
Monad laws were not placed inside the Monad type class in the example shown. Why?
- In Coq it's considered good practice unbundle proof component. Facilitates extraction for one thing.

Common monads

identity
option: None, Some
non-deterministic choice: set

Monad laws:

sequence op is associative

D2

Monad laws

m: M A kb: A → M B kc: B → M C

x <- ret a; kb x ≈ kb a
x <- m; ret x ≈ m
x <- (y <- m; kb y); kc x ≈ y <- m; x <- kb y; kc x

(Think of monad being a box and <- as unboxing.)

–

A bunch of equational theory for the monadic rules which can then be used as rewrite rules to prove semantic equality of two programs.

put s1; put s2 ≈ put s2 ???
put s; get ≈ put s; ret s
s1 <- get; s2 <- get; k s1 s2 ≈ s <- get; k s s

Looping programs and diversions => itrees. Will see later.

–

Free monads
Freer monads

Extensible language

Expression problem: Lack of modularity/extensability.

Add new features like new operator => lot of changes
Datatype à la carte: Parametrize expr with a type representing operations/features

Inductive expr (opr: Type): Type :=
| Val: nat -> expr opr
| Do (op: opr) (k: nat -> expr opr).
(* k: a continuation accepting nat.
   Assuming that we deal only with nat ops *)

Inductive plus: Type :=
| Add: nat -> nat -> plus.

We could write stuff like:

Do (Add 2 3) (fun n => Val n)
(* 5 *)

Evaluation (naïve version):

Fixpoint eval {opr: Type} (e: expr opr): nat :=
  match e with
  | Val n => n
  | Do op k =>
      match op with
      | Add n1 n2 => eval (k (n1 + n2))
      end
  end.

Comment: This means weird syntax, but no gain

Evalution (via a handler):

(* eval_fold *)
Fixpoint evalf {opr: Type} (h: opr -> nat) (e: expr opr): nat :=
  match e with
  | Val n => n
  | Do op k => evalf h (k (h op))
  end.

(* Handler for [plus] *)
Definition hplus (op: plus): nat :=
  match op with
  | Add n1 n2 => n1 + n2
  end.

Compute evalf hplus (Do (Add 2 3) (fun n => Val n)).
(* 5 *)

—

Sequential composition:

Fixpoint seq {opr: Type} (e: expr opr) (k: nat -> expr opr): expr opr :=
  match e with
  | Val n => k n
  | Do op h => Do op (fun n => Do op (seq (h n) k))
  end.
Notation "x <- e1;; e2 " := (seq e1 (fun x => e2)).

Operations as triggerable events:

Do op and return its value as an expr ??

Definition trigger {opr: Type} (op: opr): Expr opr :=
  Do op (fun n => Val n).

Example uses:

eval (trigger (Add 2 3))
(* 5 *)

eval (
  x <- trigger (Add 2 3);;
  y <- trigger (Add 4 5);;
  trigger (Add x y)
)
(* 14 *)

Let's try adding another operation: Subtr.

Inductive subtr: Type :=
| Subtr: nat -> nat -> subtr.

Fixpoint hsubtr (op: subtr): nat :=
  match op with
  | Subtr n1 n2 => n1 - n2
  end.

evalf hsubtr (trigger (Subtr 5 3))
(* 2 *)


evalf hsubtr (
  x <- trigger (Subtr 5 3);;
  y <- trigger (Subtr 2 1);;
  trigger (Subtr x y)
)
(* 1 *)

—

Multiple operations:

Notation "opr1 +' opr2" := ((opr1 + opr2)%type).

(* Handler for add and sub *)
Definition hsum {opr1 opr2: Type} (h1: opr1 -> nat) (h2: opr2 -> nat)
  (op: opr1 +' opr2): nat :=
  match op with
  | inl op' => h1 op'
  | inr op' => h2 op'
  end.

evalf (hsum hadd hsubtr) (
  x <- trigger (inl (Add 2 3));;
  y <- trigger (inr (Subtr x 3));;
  trigger (inl (Add y 1))
)
(* 3 *)

Note: The Add and inl are duplicate essentially. Typeclasses to help it figure out could come in handy.

Free monads

Generalizing instead of specializing results to nat.

(*
 - E: opr ?? 
 - R: final return type ??
*)
Inductive FFree (E: Type -> Type) (R: Type): Type :=
| Ret: R -> FFree E R
| Do: forall {X: opr},
    E X -> (X -> FFree E R).

E X: E produces an X, which will be fed in to the continuation.

~~Same as expr from earlier,~~ ~~except for nat being generalized~~.

itree

Inductive itree
| Ret: R -> itree
| Tau: itree
| Vis {Ans: Type} (event: E Ans) (k: Ans -> itree).

const5 := Ret 5. double := Vis Input (fun n > Ret 2*n). silentloop : Tau silentloop

(* Result from event given to the system is the index Type *)
Inductive IOEvent: Type -> Type :=
| Out: nat -> IOEvent unit
| Inp: IOEvent nat.

CoFixpoint inoutloop :=
  Vis Inp (fun n =>
    Vis Out (fun _ => inoutloop)).

Inductive empty: Type -> Type :=
| Empty: fail void.

Definition fail :=
  Vis empty (fun v => match x with end).

(* subst *)
CoFixpoint subst (x: itree) (k: X -> itree): itree :=
  match x with
  | Ret v => k v
  | Vis ev kk => Vis ev (fun x => subst (kk x) k)
  | Tau t => subst t k
  end.

Iter

left => keep looping
right => loop over

{inty rty: Type} 
iter (t: itree) (k: inty -> itree) (init: inty)

   x <- k init;;
   match x with
   | inl nval => Tau (iter t' k nval)  (* init is like the initial state (like loop exit condition??) nval is the new state *)
   | inr nval => Ret nval
   end

fact (n: nat) :=
  iter (fun n => fact (n-1)

D3

Delay monad

itree E R: promises to deliver a value of type R

irrefutable pattern matching

Equivalence of itrees

strong bisimulation: structure has to be exactly the same
- t1 ~ t2
weak bisimulation: tau is 'flattened' out
- 'equailty up to taus' (eutt):
- t1 ≈ t2

Monad laws hold upto strong bisimulation.

weak bisimulation sats monad laws too.

Nested coinductive inductive sth

Kleisli

DBT: bimap

https://github.com/Zdancewic/oplss2024/blob/main/terse/ITreesEquiv.html (slide-5)

Imp deno sem with itrees

DBT: Why variant for MemE?

D4

Unary hoare logic, relational hoare logic
Sequence rule in hoare logic

FA attempt

State:
- 1: option bool = last output
- 2: real state
Input: A
Output: option bool

Desired function: S -> Inp -> (S, Out)

Inp: Input type
S: state = (oldout, real)
Out: Output type

itree E R
| Vis: forall X, E X -> (X -> itree E R)
| Tau: itree E R

Dbts

L1

could compcert have used itree?
difference ctree and itree
Coq to slides
concept of fixpoint
why is fnal existentionality considered sub-optimal?