feat: add itree paper review

Author: RangHo

paper-itree/assets/asm-flow.png

@@ -0,0 +1,378 @@
+#+title: Interaction Trees
+#+subtitle: Representing Recursive and Impure Programs in Coq
+#+author: Juhun Lee
+#+date: <2025-08-07 Thu>
+#+options: timestamp:nil toc:nil num:nil
+
+#+reveal_head_preamble: <style>
+#+reveal_head_preamble:   .reveal { word-break: keep-all; }
+#+reveal_head_preamble:   .reveal hgroup p { font-size: var(--r-heading3-size); }
+#+reveal_head_preamble: </style>
+
+#+reveal_plugins: (highlight math)
+#+reveal_talk_url: https://talking.rangho.me/paper-verdi/
+#+reveal_title_slide: <hgroup><h1>%t</h1><p>%a</p></hgroup><p>%d</p>
+#+options: reveal_width:"90%"
+
+* Introduction
+Let there be a Lisp-like programming language with two operators:
+- ~(+ n m)~ :: Addition of ~n~ and ~m~.
+- ~(- n m)~ :: Subtraction of ~n~ and ~m~.
+
+In this programming language, we want to verify the following expression:
+
+#+begin_src scheme
+  (+ 1 2) ; => 3
+#+end_src
+
+** Traditional Formal Verification
+The most straightforward method of verifying would look like:
+
+#+begin_src coq
+  Inductive exp : Type :=
+  | Num (n : nat)
+  | Add (e1 e2 : exp)
+  | Sub (e1 e2 : exp).
+
+  Fixpoint eval (e : exp) : nat :=
+    match e with
+    | Num n => n
+    | Add e1 e2 => (eval e1) + (eval e2)
+    | Sub e1 e2 => (eval e1) - (eval e2)
+    end.
+#+end_src
+
+** Formal Semantics
+Formal verification is, essentially, *analyzing the meaning of the program*.
+
+- If it makes sense, *verified*.
+- If it does not, *unverified*.
+
+** Operational Semantics
+The expression is evaluated /as a whole/.
+
+#+begin_src coq
+  Fixpoint eval (e : exp) : nat :=
+    match e with
+    | Num n => n
+    | Add e1 e2 => (eval e1) + (eval e2)
+    | Sub e1 e2 => (eval e1) - (eval e2)
+    end.
+#+end_src
+
+This models the whole operation.
+
+*Operational semantics*.
+
+** What If...
+- ...I add more operators?
+- ...I add loop constructs?
+- ...I express the "same" logic in different programming language?
+- ...I target the "same" program for a different environment?
+
+** Abstraction!
+We need an abstraction model that is both:
+
+- language-independent, and
+- environment-independent.
+
+If a theory is independent of everything, is the theory meaningful at all?
+
+** Abstraction?
+To keep a theory relevant, a central question is necessary.
+
+*What is a program?*
+
+* Interaction Trees
+A program is *a sequence of interactions*.
+
+A program can:
+
+1. return a value and terminate,
+2. transition to a different program, or
+3. interact with the environment.
+
+** The ITree
+#+begin_src coq
+  CoInductive itree (E : Type -> Type) (R : Type) : Type :=
+  | Ret (r : R)
+  | Tau (t : itree E R)
+  | Vis {A : Type} (e : E A) (k : A -> itree E R).
+#+end_src
+
+ITree is defined as a coinductive type to model non-terminating programs.
+
+** ITree Parameters
+#+begin_src coq
+  CoInductive itree (E : Type -> Type) (R : Type) : Type :=
+  | Ret (r : R)
+  | Tau (t : itree E R)
+  | Vis {A : Type} (e : E A) (k : A -> itree E R).
+#+end_src
+
+- ~E : Type -> Type~ :: The type of external interaction.
+- ~R : Type~ :: The type of the result (i.e. return value).
+
+** ITree Constructors 
+- ~Ret (r : R)~ :: Terminate the program by returning value ~r~.
+- ~Tau (t : itree E R)~ :: Perform internal calculation by transitioning to new program ~t~.
+- ~Vis {A : Type} (e : E A) (k : A -> itree E R)~ :: Interact with environment by triggering event ~e~. Based on the result, transition to new program generated by ~k~.
+
+** Example: Modeling I/O
+Imagine a system where you can input or output a natural number.
+
+#+begin_src coq
+  Inductive IO : Type -> Type :=
+  | Input : IO nat
+  | Output : nat -> IO unit.
+#+end_src
+
+- ~Input~ will bring a natural number to you from the user input.
+- ~Output~ will grab a natural number from you and show it to the user.
+
+*** Echo
+#+begin_src coq
+  CoFixpoint echo : itree IO void :=
+    Vis Input (fun x => Vis (Output x) (fun _ => echo)).
+#+end_src
+
+1. Interact with environment by receiving ~Input~.
+2. From the result of the interaction, transition to a new program.
+3. The new program will interact with environment by calling ~Output~ with the result.
+4. The new program will transition back to 1.
+
+*** Spin
+#+begin_src coq
+  CoFixpoint spin : itree IO void :=
+    Tau spin
+#+end_src
+
+1. Perform internal calcuation.
+2. Transition to 1.
+
+*** Kill9
+#+begin_src coq
+  CoFixpoint kill9 : itree IO unit :=
+    Vis Input (fun x => if x =? 9 then Ret tt else kill9).
+#+end_src
+
+1. Interact with environment by receiving ~Input~.
+2. From the result of the interaction, transition to a new program.
+3. The new program checks the number is equal to 9.
+   1. If it is, the new program is returning ~tt~ (nothing).
+   2. If it is not, the new program is going back to 1.
+
+** Composing ITrees as Monads
+Basic operations for interaction trees are follows:
+
+#+begin_src haskell
+  itree E A :: Type
+  Tau :: itree E A -> itree E A
+  Ret :: A -> itree E A
+  Vis :: {R} (E R) -> (R -> itree E A) -> itree E A
+  bind :: itree E A -> (A -> itree E B) -> itree E B
+  trigger :: E A -> itree E A
+#+end_src
+
+Since ~itree E~ is a monad for any ~E~, we can compose ITrees according to functional programming rules.
+
+*** Monad?
+Monad is a type wrapping another type, useful for:
+
+1. structuring sequences of operations on values,
+2. representing delayed computations, and
+3. many more.
+ 
+*** Example: IO Monad
+Recall the I/O example before.
+It is also a monad wrapping a ~Nat~:
+
+#+begin_src haskell
+  data IO a = ...
+
+  getNat :: IO Nat
+  putNat :: Nat -> IO ()
+#+end_src
+
+*** Binding Values
+For a wrapper to be a monad, you must be able to bind a value to another function.
+
+#+begin_src haskell
+  (>>=) :: IO a -> (a -> IO b) -> IO b
+
+  echo :: IO ()
+  echo =
+    getNat -- IO wrapper with Nat value
+    >>=    -- Take out Nat from IO wrapper
+    putNat -- Give the Nat as a parameter, resulting in an IO wrapper with empty value
+#+end_src
+
+For ITree, this binding operator is a function called ~bind~.
+
+*** Binding Values with Names
+Imagine a case where we put a lambda function instead of a defined function.
+
+#+begin_src haskell
+  echo' = getNat >>= (\x -> putNat x)
+#+end_src
+
+This is, essentially, taking a value out of the wrapper and giving it a name ~x~.
+
+#+begin_src haskell
+  echo' = do
+    x <- getNat
+    putNat x
+#+end_src
+
+For ITree, this example would have been written as ~x <- getNat ;; putNat x~.
+
+*** Returning Values
+Also, you must be able to make a regular value into a wrapped value.
+
+#+begin_src haskell
+  return :: a -> IO a
+
+  putOne = do
+    x <- return 1
+    putNat x
+#+end_src
+
+For ITree, this "return" function is called ~ret~, which is a shorthand for the ~Ret (r : R)~ constructor.
+
+*** Rewriting Echo Example
+From this information, we can rewrite the ~echo~ program as a composition of basic ITree operations:
+
+#+begin_src coq
+  CoFixpoint echo : itree IO void :=
+    Vis Input (fun x => Vis (Output x) (fun _ => echo)).
+
+  CoFixpoint echo2 : itree IO void :=
+    x <- (trigger Input) ;; trigger (Output x) ;; Tau echo2.
+#+end_src
+
+1. Trigger ~Input~ event and bind the result as ~x~.
+2. Then, trigger ~Output~ event with ~x~.
+3. Then, transition to step 1.
+
+** Equivalence between ITrees
+There are two types of equivalence relations between ITrees \( t_{1} \) and \( t_{2} \):
+
+- Strong bisimulation \( t_{1} \cong t_{2} \) :: Two ITrees have /exactly/ same shape.
+- Weak bisimulation \( t_{1} \approx t_{2} \) :: Two ITrees have same interactions and same return values.
+
+** KTrees: Continuation Trees
+KTree is the type that determines which program to run after an interaction.
+
+(cf. ~Vis {A : Type} (e : E A) (k : A -> itree E R)~)
+
+#+begin_src coq
+  Definition ktree (E : Type -> Type) (A B : Type) : Type :=
+    A -> itree E B.
+
+  Definition eq_ktree {E} {A B : Type} : ktree E A B -> ktree E A B -> Prop :=
+    fun h1 h2 => ∀a, h1 a ≈ h2 a.
+#+end_src
+
+* Semantics of Events and Monadic Interpreters
+- In ITree, an *event handler* is an object of type \( E \leadsto M \).
+  - Event ~E~ is a monadic operation in ~M~.
+- An *interpreter* folds such event handler over an ITree.
+  - Good interpretation preserves the monadic structure of ~itree E~.
+
+** Example: Semantics of States
+Imagine a set of events getting and putting values into a state.
+
+#+begin_src coq
+  Variant stateE (S : Type) : Type -> Type :=
+    | Get : stateE S S
+    | Put : S -> stateE S unit.
+#+end_src
+
+** Event into Monad
+We can define a transformer that turns this event into a monad.
+
+#+begin_src coq
+  Definition stateT (S : Type) (M : Type -> Type) (R : Type) : Type :=
+    S -> M (S * R).
+  Definition getT (S : Type) : stateT S M S :=
+    fun s => ret (s, s).
+  Definition putT (S : Type) : S -> stateT S M unit :=
+    fun s' s => ret (s', tt).
+#+end_src
+
+~stateT~ takes a state and returns a monad of new state and resulting value.
+
+** Event Handler
+Then, we can actually define a handler that repackages events.
+
+#+begin_src coq
+  Definition h_state (S : Type) {E} : (stateE S) ~> stateT S (itree E) :=
+    fun _ e =>
+      match e with
+      | Get => getT S
+      | Put s => putT S s
+      end.
+#+end_src
+
+Note that ~stateT S (itree E)~ is ~S -> itree E (S * R)~, where it takes a state and returns an ITree with event ~E~ and result type of new state and return value.
+
+** Monadic Interpreter
+Finally, we can define an interpreter that will traverse the ITree.
+
+#+begin_src coq
+  Definition interp_state {E S} : itree (stateE S) ~> stateT S (itree E) :=
+    interp h_state.
+#+end_src
+
+Here, ~interp~ is a generic interpreter provided by ITree that walks the whole ITree while applying event handler in every step.
+
+* Case Study: Verified Compilation of IMP to ASM
+Consider the IMP langauge from /Software Foundations/ volume 1.
+
+Let there be a simple instruction set called ASM.
+
+We can devise a compiler and verify its correctness.
+
+** Semantics of IMP
+The semantics given to ~imp~ (a ~com~ in /SF/) is shown below.
+
+[[file:assets/imp-semantics.png]]
+
+** Semantics of ASM
+The semantics given to ~asm~ is shown below.
+
+[[file:assets/asm-semantics.png]]
+
+** Control-flow Graph of ASM
+The semantics of ASM is rearranged to form a composable linking combinators.
+
+[[file:assets/asm-flow.png]]
+
+** Compilation
+Statements in IMP are matched with ASM linking combinators to compile.
+
+#+begin_src coq
+  Fixpoint compile (s : stmt) {struct s} : asm 1 1 :=
+    match s with
+    | Skip => id_asm
+    | Assign x e => raw_asm_block (after (compile_assign x e) (Bjmp l1))
+    | Seq l r => seq_asm (compile l) (compile r)
+    | If e l r => if_asm (compile_expr 0 e) (compile l) (compile r)
+    | While e b => while_asm (compile_expr 0 e) (compile b)
+    end.
+#+end_src
+
+If the IMP program and corresponding ASM program have bisimulational relationship, then two programs are equivalent.
+
+#+begin_src coq
+  Theorem compile_correct (s : stmt) : equivalent s (compile s).
+#+end_src
+
+* Conclusion
+*ITree* forms a basis on which to represent impure recursive programs with Coq.
+
+Its denotational approach allows highly expressive represntation of programs.
+
+* Further Works
+- Automation of proofs using interaction tree?
+- Porting this logic to proof assistants other than Coq/Rocq?