class: title-slide <style> .title-slide .nus-logo img { width: 200px; display: block; margin: 0; float: left; } </style> .nus-logo[] # Automated Verification of Effectful Higher-order Programs <!-- .subtitle[*Thesis Defence*] --> Darius Foo .aligned[ **Advisor**: A/P Chin Wei Ngan **Panel**: A/P Ilya Sergey<br>Prof. Olivier Danvy ] --- # Pure higher-order functions .center-code[ ```ocaml let foldr f xs acc = match xs with | [] -> acc | x :: t -> f x (foldr f t acc) ``` ] Say we want to prove that `foldr (fun x t -> x + t) xs 0` computes the sum of `xs`. --- # Two approaches - __Approach 1__: view <img class="math-inline" src="2bb96d8995686123.svg" alt="\m{foldr}" style="vertical-align: -2.835pt" /> as a mathematical function and prove this directly <img class="math-display" src="e1ce3f158939ba3d.svg" alt="\foldr\ (\vlambda{x\,t}{x + t})\ \xs\ 0 = \psum{\xs}" /> The proof goes straightforwardly by induction on <img class="math-inline" src="52f06aefdff3f535.svg" alt="\xs" style="vertical-align: -0.131pt" />. -- - __Approach 2__: view `foldr` as a program and use a program logic <img class="math-display" src="6821b7cda2e42706.svg" alt="\htripleres{\vtrue}{\,\m{foldr}\ (\vlambda{x\,t}{x + t})\ \xs\ 0}{r}{r = \psum{\xs}}" /> We need a triple for `foldr`, but given one, this can be proved in many tools, e.g. Why3. --- # Imperative higher-order functions Suppose we wanted to prove that this program also computes the sum of `xs`. .center-code[ ```ocaml let l = ref 0 in foldr (fun x () -> l := x + !l) xs (); !l ``` ] -- - __Approach 1__: .fg-red[inapplicable]; <img class="math-inline" src="2bb96d8995686123.svg" alt="\m{foldr}" style="vertical-align: -2.835pt" />'s argument isn't a mathematical function -- - __Approach 2__: this works, via the following separation logic triple <img class="math-display" src="cb3abb94a8d3280d.svg" alt="\htripleres{\heapto{l}{v}}{\m{foldr}\ (\vlambda{x\,\vunit}{...})\ \xs\ \vunit}{\res}{\heapto{l}{(v{+}\psum{\xs})} \sep \hpure{\m{res}{=}\vunit}}" /> -- We still need a triple for `foldr`. Let's see how this is done, starting with the pure case. --- layout: true # The pure case (Why3) --- ```why3 let rec foldr `(ghost inv : list 'a -> 'b -> bool)` (f:'a -> 'b -> 'b) (xs: list 'a) (acc: 'b) : 'b `requires { inv Nil acc }` `requires { forall acc x ys.` `inv ys acc -> inv (Cons x ys) (f x acc) }` `ensures { inv xs result }` = match xs with | Nil -> acc | Cons x t -> `f` x (foldr `inv` f t acc) end ``` .code-span-faded[1, 2, 3, 4, 5, 7] .code-span-hlr[6] --- count: false ```why3 let rec foldr `(ghost inv : list 'a -> 'b -> bool)` (f:'a -> 'b -> 'b) (xs: list 'a) (acc: 'b) : 'b `requires { inv Nil acc }` `requires { forall acc x ys.` `inv ys acc -> inv (Cons x ys) (f x acc) }` `ensures { inv xs result }` = match xs with | Nil -> acc | Cons x t -> f x (foldr `inv` f t acc) end ``` .code-span-faded[2, 3, 4, 5] --- count: false ```why3 let rec foldr `(ghost inv : list 'a -> 'b -> bool)` (f:'a -> 'b -> 'b) (xs: list 'a) (acc: 'b) : 'b `requires { inv Nil acc }` `requires { forall acc x ys.` `inv ys acc -> inv (Cons x ys) (f x acc) }` `ensures { inv xs result }` = match xs with | Nil -> acc | Cons x t -> f x (foldr `inv` f t acc) end ``` .code-span-faded[3, 4, 5] --- count: false ```why3 let rec foldr `(ghost inv : list 'a -> 'b -> bool)` (f:'a -> 'b -> 'b) (xs: list 'a) (acc: 'b) : 'b `requires { inv Nil acc }` `requires { forall acc x ys.` `inv ys acc -> inv (Cons x ys) (f x acc) }` `ensures { inv xs result }` = match xs with | Nil -> acc | Cons x t -> f x (foldr `inv` f t acc) end ``` .code-span-faded[5] --- class: foldr-invariant-slide count: false ```why3 let rec foldr (ghost `inv` : list 'a -> 'b -> bool) (`f`:'a -> 'b -> 'b) (xs: list 'a) (acc: 'b) : 'b requires { inv Nil acc } requires { forall acc x ys. inv ys acc -> inv (Cons x ys) (`f` x acc) } ensures { inv xs result } = match xs with | Nil -> acc | Cons x t -> f x (foldr inv f t acc) end ``` -- .label-code-span3[`f`, a program fragment, is treated as a mathematical function. <br> We can only do this because it is pure.] <style>.foldr-invariant-slide .label-code-span3 { --label-gap: 1em; --label-shift: 5em; }</style> .arrow[ 2 -> 3 ] --- layout: true # The imperative case (Iris) --- <img class="math-display" src="eaba7afe8335d31f.svg" alt="\begin{array}{l} \all{\inv\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> --- count: false <img class="math-display" src="3dfd4b11335481fe.svg" alt="\begin{array}{l} \all{\hlo{\inv}\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \hlo{\inv\ []\ \acc}\ \sep \\ & \all{x\,\acc\,\ys} \{ \hlo{\inv\ \ys\ \acc} \}~f\ x\ \acc~\{ r.\ \hlo{\inv\ (x{::}\ys)\ r} \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \hlo{\inv\ \xs\ \res} \} \end{array} \end{array}" /> <img class="math-inline" src="ded8614b3a4aa6cd.svg" alt="\m{Inv}" style="vertical-align: -0.131pt" /> is now a _separation logic_ invariant, which can express state changes. --- count: false <img class="math-display" src="e110388e1128ae03.svg" alt="\begin{array}{l} \all{\inv\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \hlb{\{ \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \}} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> <img class="math-inline" src="076fb1de630d4392.svg" alt="\inv" style="vertical-align: -0.131pt" /> is now a _separation logic_ invariant, which can express state changes. <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> is now treated as a program. A nested triple is used to say that <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> preserves <img class="math-inline" src="076fb1de630d4392.svg" alt="\inv" style="vertical-align: -0.131pt" />. --- count: false <img class="math-display" src="28825e449a7039c8.svg" alt="\begin{array}{l} \all{\hlg{\inv}\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> <img class="math-inline" src="076fb1de630d4392.svg" alt="\inv" style="vertical-align: -0.131pt" /> is now a _separation logic_ invariant, which can express state changes. <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> is now treated as a program. A nested triple is used to say that <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> preserves <img class="math-inline" src="076fb1de630d4392.svg" alt="\inv" style="vertical-align: -0.131pt" />. Invariant needed: <img class="math-inline" src="9f0d6508c81ed265.svg" alt="(\vlambda{\m{suff}\,r}{\heapto{l}{(\psum{\m{suff}})}\sep\hpure{r=\vunit}})" style="vertical-align: -2.835pt" /> --- layout: false # A problem > Different clients may instantiate _foldr_ with some very different functions, hence it can be hard to give a specification for _f_ that is reasonable and general enough to support all these choices. In particular knowing when one has found a good and provable specification can be difficult in itself. .cite[Lecture Notes on Iris] <!-- — --> --- # A problem Suppose we wanted <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> to rely on a property of the individual list elements. <img class="math-display" src="b9927983c5807e9e.svg" alt="\begin{array}{l} \all{\inv\,P\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \hpure{\m{all}\ P\ \xs} \sep \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \hpure{P\ x} \sep \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> --- count: false # A problem Suppose we wanted <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> to rely on a property of the individual list elements. <img class="math-display" src="eb815c5df662376b.svg" alt="\begin{array}{l} \all{\inv\,\hlg{P}\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \hlg{\hpure{\m{all}\ P\ \xs}} \sep \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \hlg{\hpure{P\ x}} \sep \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> -- We have to propagate it outwards using <img class="math-inline" src="8f0691efdd1d43d2.svg" alt="\m{all}" style="vertical-align: -0.131pt" />. Moreover, the unary form of <img class="math-inline" src="0683df3ba66239ed.svg" alt="P" style="vertical-align: -0.024pt" /> is fixed. --- # A problem Suppose we wanted to rely on a property of consecutive elements of the list. <img class="math-display" src="897cc26b59816765.svg" alt="\begin{array}{l} \all{\inv\,\hly{P_1}\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \hly{\hpure{P_1\ \xs}} \sep \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> We would need a new specification with a property parameterised over <img class="math-inline" src="52f06aefdff3f535.svg" alt="\xs" style="vertical-align: -0.131pt" />. --- # A problem What if we passed the argument <img class="math-inline" src="b8ed8feab5422408.svg" alt="(\vlambda{x\,t}{\m{assert}\ x \ge t; x + t})" style="vertical-align: -2.406pt" />? <img class="math-display" src="0a5220491fe8e509.svg" alt="\begin{array}{l} \all{\inv\,\hlr{P_2}\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \hlr{\hpure{P_2\ x\ \acc}} \sep \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \} \end{array} \end{array}" /> This would require a binary property <img class="math-inline" src="71f593086b77aefb.svg" alt="P_2" style="vertical-align: -1.819pt" /> relating each element and suffix-sum. Again, neither <img class="math-inline" src="0683df3ba66239ed.svg" alt="P" style="vertical-align: -0.024pt" />, <img class="math-inline" src="0c21ddc2b565e446.svg" alt="P_1" style="vertical-align: -1.819pt" />, nor <img class="math-inline" src="076fb1de630d4392.svg" alt="\inv" style="vertical-align: -0.131pt" /> would be sufficient. --- # Another problem What if we passed the argument <img class="math-inline" src="b8fa9bfd4a8381b6.svg" alt="(\vlambda{x\,t}{\m{raise}\ E})" style="vertical-align: -2.406pt" />? We would need a creative encoding in either the program (e.g. monad) or logic (e.g. exceptional postcondition)... <img class="math-display" src="a9b14a30d877f21d.svg" alt="\begin{array}{l} \all{\inv\,\hlb{Q_E}\,f\,\xs\,\acc} \\ \quad \begin{array}{c} \biggl\{\, \begin{aligned} & \inv\ []\ \acc\ \sep \\ & \all{x\,\acc\,\ys} \{ \inv\ \ys\ \acc \}~f\ x\ \acc~\{ r.\ \inv\ (x{::}\ys)\ r \}\ \hlb{\{ E.\ Q_E\ E \}} \end{aligned} \,\biggr\} \\ \m{foldr}\ f\ \xs\ \acc \\ \{ \res.\ \inv\ \xs\ \res \}\ \hlb{\{ E.\ Q_E\ E \}} \end{array} \end{array}" /> Approach 2 really only supports effects _that can be represented in the underlying logic_. --- # A conundrum To recap, - **Approach 1**: almost automated for pure functions, but .fg-red[inapplicable] to effectful ones - **Approach 2**: requires creativity to come up with specification _and_ instantiate it; "one-spec-per-use problem"; relies on underlying logic being able to represent effects -- .morph-element.morph-table[ | | pure | effectful | | ---------- | ------------------ | ------------------ | | Approach 1 | ✔ | ✘ | | Approach 2 | ✔^\*\*\* | ✔^\*\*\* | ] --- # Towards a solution Can we find a version of Approach 1 which overcomes the downsides of Approach 2? .morph-element.morph-table[ | | pure | effectful | | ---------- | ------------------ | ------------------ | | Approach 1 | ✔ | .hlr[✘] | | Approach 2 | ✔^\*\*\* | ✔^\*\*\* | ] --- # Thesis .center[Staged logic is an effective means of automating the <br>verification of higher-order effectful programs.] --- # Outline - __Staged logic and higher-order functions__ - Effect handlers and shift/reset - Implementation and mechanisation - Conclusion --- # Outline - __Staged logic and higher-order functions__ 1. How staged logic works (on the <img class="math-inline" src="fc4839c012bfda35.svg" alt="\foldr" style="vertical-align: -2.835pt" /> example) 2. Two more case studies 3. How automation works - Effect handlers and shift/reset - Implementation and mechanisation - Conclusion --- # Staged logic <img class="math-display" src="c799e9767ac0bcd6.svg" alt="$\begin{array}{r@{\ \,}ll} \flow ::= & \sreq{H} \mid \sens{H} & \text{Specifications} \\ % \mid & f(v,r) \mid \flow_1; \flow_2 \mid ... & \text{Program elements} \\ \mid & \vlambda{x}{\flow} \mid \flow_1 \app \flow_2 \mid \flow_1\bind{r} \flow_2 \mid \sreturn{v} \mid ... & \text{Program elements} \\ \mid & \flow_1 \vee \flow_2 \mid \flow_1 \wedge \flow_2 \mid \ex{x} \flow \mid \all{x} \flow & \text{Logical connectives} \end{array}$" /> .gap-sm[] -- - Syntactically, a lambda calculus with specifications and logical connectives -- - <img class="math-inline" src="ca9462695fb637bb.svg" alt="\req" style="vertical-align: -2.811pt" /> and <img class="math-inline" src="6bf4fd89d2391bee.svg" alt="\ens" style="vertical-align: -0.137pt" /> are separation logic _assume_/_consume_/_exhale_ and _assert_/_produce_/_inhale_ --- class: staged-logic-slide # Staged logic as a program logic - Staged logic generalises Hoare logic .gap-sm[] .cols-2[ .anchored[ .two.label.at-tl[History] .two.label.at-br[Behaviour] <img class="math-display" src="7578ef4090f63cdc.svg" alt="\htriple{\hlb{\flow}}{e}{\hlo{\flow}}" /> ] <img class="math-display" src="57130afcaf694a27.svg" alt="\htriple{P}{e}{Q} \defeq \htriple{\sens{P}}{e}{\sens{Q}}" /> ] -- .gap-sm[] - Key to the design is the rule for application of unknown functions <img class="math-display" src="3488638cfe99ab86.svg" alt="\inferrule*[right=App]{ }{\htriple{\flow}{f\ v}{\flow; f\ v}}" /> <style> .staged-logic-slide .two.label.at-tl { --dx: -1.5em; } .staged-logic-slide .two.label.at-br { --dx: 2.5em; } </style> --- class: staged-logic-slide # Staged logic as a program logic - In the rule of consequence, _refinement_ relates staged logic terms <img class="math-display" src="49afe1cf41fa5352.svg" alt="\inferrule*[right=Conseq]{\htriple{\flow_3}{e}{\flow_4} \\ \flow_1 \stagesubs \flow_3 \\ \flow_4 \stagesubs \flow_2}{\htriple{\flow_1}{e}{\flow_2}}" /> -- - When working with refinement, staged logic can also be seen as a higher-order IVL .gap-sm[] .anchored[ .one.label.at-tl[Higher-order IVL] .one.label.at-br[Specification] <img class="math-display" src="2880861f7f33a30c.svg" alt="\hlg{\flow} \stagesubs \hlr{\flow}" /> ] .gap-md[] <img class="math-display" src="6ad50dace95d458c.svg" alt="\htriple{P}{e}{Q} \defeq \m{translate}\ e \stagesubs \sreq{P}; \sens{Q}" /> <style> .staged-logic-slide .one.label.at-tl { --dx: -6.5em; } .staged-logic-slide .one.label.at-br { --dx: 5em; } </style> --- # A specification for _foldr_ .cols-2[ ```ocaml let foldr f init xs = match xs with | [] => init | h :: t => f h (foldr f init t) ``` <img class="math-display" src="73edbd89c23f5be8.svg" alt="\begin{array}{l} \foldr\ f\ \init\ \xs \defeq \\ \quad \sens{\xs{=}[]; \sreturn{\init}} \\ \quad \vee\ \exists h\,t. \sens{\xs{=}h{::}t}; \foldr\ f\ \m{init}\ t \bind{r} f\ h\ r \end{array}" /> ] -- Given `let g x () = l := x + !l`, we would like to prove: <img class="math-display" src="daa5c6fc6a7a8792.svg" alt="\inferrule{g\ x\ \vunit \stagesubs \ex{v}\sreq{\heapto{l}{v}};\sensr{r}{\heapto{l}{(v{+}x)}\sep[r{=}\vunit]}}{\foldr\ g\ \vunit\ \xs \stagesubs \ex{v}\sreq{\heapto{l}{v}}; \sensr{r}{\heapto{l}{(v{+}\psum{\xs})} \sep [r = \vunit]}}" /> --- # Stateful _foldr_ **Inductive case** <img class="math-display" src="faf8ceb745d55a19.svg" alt="\begin{array}{rl@{\hspace{1.5em}}l} & \sens{\xs{=}h{::}t};\ \foldr\ g\ \vunit\ t \bind{r}\, g\ h\ r \\ \stagesubs & \sens{\xs{=}h{::}t};\ \big(\ex{v_1}\sreq{\heapto{l}{v_1}};\sensr{r}{\heapto{l}{(v_1{+}\psum{t})}\sep[r{=}\vunit]}\big) \bind{r}\, g\ h\ r & \text{Ind. hyp.} \\ \stagesubs & \sens{\xs{=}h{::}t};\ \ex{v_1}\sreq{\heapto{l}{v_1}};\sensr{r}{\heapto{l}{(v_1{+}\psum{t})}\sep[r{=}\vunit]}; \\ & \quad \ex{v_2}\sreq{\heapto{l}{v_2}};\sensr{r_1}{\heapto{l}{(v_2{+}h)}\sep[r_1{=}\vunit]} & \text{Unfold } g \\ \stagesubs & \ex{v}\sreq{\heapto{l}{v}};\sensr{r_1}{\heapto{l}{(v{+}\psum{\xs})}\sep[r_1{=}\vunit]} & \textsc{NormEnsReq} \end{array}" /> -- The final step relies on biabduction to symbolically execute the <img class="math-inline" src="ca9462695fb637bb.svg" alt="\req" style="vertical-align: -2.811pt" /> and <img class="math-inline" src="6bf4fd89d2391bee.svg" alt="\ens" style="vertical-align: -0.137pt" /> away. <img class="math-display" src="23f12b11c258cb93.svg" alt="\infrule{H_A \sep H_1 \vdash H_2 \sep H_F}{\sens{H_1}; \sreq{H_2} \stagesubs \sreq{H_A}; \sens{H_F}}{NormEnsReq}" /> --- # Stateful _foldr_ This proof ultimately comes down to <img class="math-display" src="77df88cb33d059a0.svg" alt="(v_2{=}v_1{+}\psum{t}) \sep \heapto{l}{(v_1{+}\psum{t})} \sep [r{=}\vunit] \vdash \heapto{l}{v_2} \sep [r{=}\vunit]" /> and <img class="math-display" src="a2477b1f35180e41.svg" alt="\xs{=}h{::}t \implies (v_1 + \psum{t}) + h = v_1 + \psum{\xs}" /> <!-- ... both of which can be discharged by existing provers. --> --- # Key idea: maintaining precision Approach 2 forces us to commit to an _abstraction_ of the behaviour of an unknown function <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> (e.g. an invariant-parameterised triple) _before we even know what <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> is_. Any choice is necessarily _imprecise_ (wrt the operational semantics) because <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" />'s behaviour depends on things external to <img class="math-inline" src="2bb96d8995686123.svg" alt="\m{foldr}" style="vertical-align: -2.835pt" />, i.e. its callers. --- # Key idea: maintaining precision Being able to leave <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> in specifications allows us to precisely track its behaviour, effects, and their ordering, without abstraction. Consequence: proofs stay _syntactic_, making them possible to automate. To keep things tractable, we do, however, want to abstract once we can. <img class="math-display" src="2a28f8b718373047.svg" alt="\m{foldr}\ \m{f}\ 0\ \xs \stagesubs \underbrace{f\ x_1\ ...;\ f\ x_2\ ...;\ ...}_{\text{precise, but very concrete}} \stagesubs \underbrace{\sreq{...};\sens{...}}_{\text{once $f$ is known, abstract}}" /> --- # Case study: Landin's knot Recursion via a mutable ref holding a closure: <img class="math-display" src="dee6426a93a82745.svg" alt="\m{fact_f}\ \m{self}\ r\ n \defeq \sens{n{\le}0};\sreturn{1} \vee \sens{n{>}0}; \m{self}\ r\ (n{-}1)\bind{k}\sreturn{n{\cdot}k}" /> -- <img class="math-display" src="89704815cc31c4f0.svg" alt="\m{knot}\ r\ n \defeq \ex{p}\sreq{\heapto{r}{p}};\sens{\heapto{r}{p}};\ \m{fact_f}\ p\ r\ n" /> -- <img class="math-display" src="c6b45582f57321e5.svg" alt="\m{landin}\ n \defeq \ex{r}\ \heapto{r}{\m{id}};\ \heapto{r}{\m{knot}};\ \m{knot}\ r\ n" /> -- The approach: symbolically execute to expose the recursion before doing induction: <img class="math-display" src="ca00d79dd99dc76c.svg" alt="\begin{array}{rl@{\hspace{1.5em}}l} & \m{landin}\ n \\ \stagesubs & \ex{r}\heapto{r}{\m{knot}};\m{knot}\ r\ n & \text{cancel } \heapto{r}{\m{id}} \\ \stagesubs & \ex{r\,v}\heapto{r}{v};\sreturn{n!} & \text{induction on $n$} \end{array}" /> --- # Case study: _foldl_ A classic question: how do _foldr_ and _foldl_ relate? <img class="math-display" src="89fa9861bdcbcee1.svg" alt="\inferrule{f\ x\ y \stagesubs f\ y\ x \qquad f\ x\ y;r.\,f\ r\ z \;\stagesubs\; f\ y\ z;r.\,f\ x\ r}{\m{foldl}\ f\ a\ \xs \stagesubs \m{foldr}\ f\ a\ \xs}" /> It suffices that <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> is commutative and associative. Note that <img class="math-inline" src="f795e30f7fc76447.svg" alt="f" style="vertical-align: -2.835pt" /> is arbitrarily stateful. -- This needs two lemmas: <img class="math-display" src="faf07e1ded05bcf0.svg" alt="\m{foldr}\ f\ \init\ \ys \bind{r} f\ y\ r \stagesubs \m{foldr}\ f\ \init\ (y{::}\ys)" /> <img class="math-display" src="518525a50d37e165.svg" alt="f\ \init\ v \bind{r} \m{foldr}\ f\ r\ \xs \stagesubs \m{foldr}\ f\ \init\ \xs \bind{r} f\ v\ r" /> (The other direction is symmetric) --- # Flavours of proof rules 1\. Reduction <img class="math-display" src="d1baa5534110ce56.svg" alt="\begin{mathpar} \inferrule*{ }{(\flow_1 \bind{x} g_1) \bind{y} g_2 \stagesubs \flow_1 \bind{x} (g_1(x) \bind{y} g_2)} \inferrule*{ }{\m{ret}\ v \bind{x} g \stagesubs g\ v} \end{mathpar}" /> 2\. Rewriting <img class="math-display" src="ebe4d3b72b2b814d.svg" alt="\begin{mathpar} \inferrule*{(\sreq{\hpure{P}};\flow_1) \stagesubs \flow_2}{\flow_1 \stagesubs (\sens{\hpure{P}};\flow_2)} \inferrule*{ }{\sens{\hpure{\vfalse}};\flow \stagesubs \flow_1} \end{mathpar}" /> 3\. Entailment <img class="math-display" src="b951f2154ebcced1.svg" alt="\begin{mathpar} \inferrule*{\all{x}(\flow \stagesubs g\ x)}{\flow \stagesubs \all{x}g\ x} \inferrule*{P \\ \flow_1 \stagesubs \flow}{\sens{\hpure{P}};\flow_1 \,\stagesubs\, \flow} \inferrule*{\flow_1 \stagesubs \flow_3 \\ \flow_2 \stagesubs \flow_3}{\flow_1 \vee \flow_2 \stagesubs \flow_3} \end{mathpar}" /> --- # Proof search Applications of three rule families are interleaved in a syntax-directed loop: - Simplifications - Reduction never loses information and is confluent and terminating - Safe entailment and rewriting, e.g. intro, trivial asserts, symbolic execution -- - Search with bounded depth - Unsafe entailment/rewriting rules - User-provided lemmas - Heuristics for quantifiers --- # Outline - Staged logic and higher-order functions - __Effect handlers and shift/reset__ - Implementation and mechanisation - Conclusion <!-- - .morph-element.morph-effects-title[Effect handlers] --> --- # Outline - Staged logic and higher-order functions - __Effect handlers and shift/reset__ 1. Effect handlers and how to reason about them 2. The problem of multishot continuations 3. Shift and reset in staged logic - Implementation and mechanisation - Conclusion --- # Effect handlers <!-- # .morph-element.morph-effects-title[Effect handlers] --> .cols-2[ .col[ ```ocaml type _ Effect.t += XCHG: int -> int Effect.t let exchange n = perform (XCHG n) ``` ```ocaml let client () = exchange (exchange 42) ``` ] ```ocaml let main () = let p = ref 0 in try client () with | v -> v | effect XCHG n, k -> let p0 = !p in p := n; continue k p0 ``` ] --- # Key questions 1. What should we do at `perform`? <img class="math-inline" src="a4f2b92469089e95.svg" alt="\inferrule*{ ? }{\htriple{P}{\m{perform}\ E\ v}{Q}}" style="vertical-align: -2.835pt" /> 2. What should we do at handlers? <img class="math-inline" src="4efc19652c6f3f56.svg" alt="\inferrule*{ \htriple{?}{e_b}{?} }{\htriple{P}{\m{try}\ e\ \m{with}\ E\ k \to e_b}{Q}}" style="vertical-align: -2.769pt" /> --- # Existing work 1. What should we do at `perform`? __Require a user-provided _protocol___ <img class="math-inline" src="39456b401ec23cba.svg" alt="\Psi" style="vertical-align: -0.036pt" />.fn[1] <img class="math-inline" src="cba405a1c0bbad2d.svg" alt="\inferrule*{\Psi = E\ \#\ !\hbrace{P}. ? \hbrace{Q}}{\htriple{P}{\m{perform}\ E\ v}{Q}\langle \Psi \rangle}" style="vertical-align: -2.835pt" /> 2. What should we do at handlers? __A user-provided _handler invariant_.fn[2] serves as the postcondition of `continue` and must be re-established at the end of the handler__ .footnote[.fn[1] A Separation Logic for Effect Handlers, de Vilhena et al., POPL 2021 <br> .fn[2] A Framework for the Automated Verification of Algebraic Effects and Handlers, Soares et al., CoRR 2023] --- # Protocols .cols-2[ .col[ ```ocaml type _ Effect.t += XCHG: int -> int Effect.t let exchange n = perform (XCHG n) (* ensures !p = x && reply = old !p *) ``` ```ocaml let client () = exchange (exchange 42) (* ensures result = 42 *) ``` ] .col[ ```ocaml let main () = let p = ref 0 in (* invariant: !p = old !p && result = 42 *) try client () with | v -> v | effect XCHG n, k -> (* assume: true *) let p0 = !p in p := n; (* prove: !p = x && p0 = old !p *) continue k p0 (* re-establish invariant *) ``` ] ] --- # Problem: the need to abstract handlers The protocol and handler invariant similarly force an upfront abstraction of every handler the effect will be used under, similar to spec for <img class="math-inline" src="fc4839c012bfda35.svg" alt="\foldr" style="vertical-align: -2.835pt" />. - Both are nontrivial to synthesise, as they are parametrised over higher-order properties - Multiply so for _multishot_ continuations, as the handler invariant must work for any number of resumptions --- # Staged logic 1. What should we do at `perform`? __Treat the effect as unknown__ <img class="math-inline" src="8a5818c618cfadee.svg" alt="\inferrule*{ }{\htriple{\flow}{\m{perform}\ E\ v}{\flow; E\ v}}" style="vertical-align: -2.835pt" /> 2. What should we do at handlers? __Internalise handlers and symbolically execute them away__ --- # Exchange in staged logic Model the both programs: <img class="math-display" src="075f1e8c56c9a7b9.svg" alt="\begin{array}{rl} \m{client} \defeq & \xchg{42}\bind{r}{\xchg{r}} \\ \m{main} \defeq & \ex{p}\sens{\heapto{p}{0}}; \stagetry{\m{client}}{\xchg{n}}{k}{} \\ & \quad (\ex{o}\sreq{\heapto{p}{o}};\sens{\heapto{p}{n}}; k\ o) \end{array}" /> We then prove: <img class="math-display" src="d652988fe66f4d24.svg" alt="\m{main} \stagesubs \ex{p} \sensr{r}{\heapto{p}{0}\wedge r{=}42}" /> --- # Proof The proof in this case is automated by symbolic execution. <img class="math-display" src="87a1b09478f6568f.svg" alt="\begin{array}{rl@{\hspace{1.5em}}l} & \sens{\heapto{p}{0}}; \stagetry{\m{client}}{\xchg{n}}{k}{...} \\ \stagesubs & \sens{\heapto{p}{0}}; & \text{Handle} \\ \phantom{\stagesubs} & \sens{k{=}(\vlambda{x}{\stagetry{\xchg{x}}{\xchg{n}}{k}{...}})} \\ \phantom{\stagesubs} & \ex{o}\sreq{\heapto{p}{o}}; \sens{\heapto{p}{42}}; k\ o \\ \stagesubs & \sens{k{=}(\vlambda{x}{\stagetry{\xchg{x}}{\xchg{n}}{k}{...}})}; & \text{Biab} \\ \phantom{\stagesubs} & \sens{\heapto{p}{42}}; k\ 0 \\ \stagesubs & \sens{\heapto{p}{42}}; \stagetry{\xchg{0}}{\xchg{n}}{k}{...} & \text{Simplify} \\ \stagesubs & \sens{\heapto{p}{42}}; \ex{o}\sreq{\heapto{p}{o}};\sens{\heapto{p}{n}}; k\ o & \text{Handle} \\ \stagesubs & \sensr{r}{\heapto{p}{0}\wedge r{=}42} & \text{Biab} \\ \end{array}" /> Maintaining precision significantly simplifies the problem. --- # Multishot continuations ```ocaml let call b = b := 0; f (); b := !b + 1; assert (!b = 1) ``` --- # Multishot continuations .cols-2[ ```ocaml let call b = b := 0; perform E; b := !b + 1; assert (!b = 1) ❌ ``` ```ocaml let main () = try client () with | effect E n, k -> continue k (); continue k () ``` ] --- # Multishot continuations .inline-children[ ```ocaml let call b = b := 0; perform E; b := !b + 1; assert (!b = 1) ``` .gap-lg[] .gap-lg[] .gap-lg[] .gap-lg[] .gap-lg[] <img class="math-display" src="0a9f297ddf191a58.svg" alt="\begin{align*} \stagetry{\m{call}}{E}{k}{-1} & \stagesubs \all{b} \sensr{r}{\heapto{b}{0} \wedge r{=}-1} \\ \stagetry{\m{call}}{E}{k}{k ()} & \stagesubs \all{b} \sensr{r}{\heapto{b}{1}\wedge r{=}\vunit} \\ \stagetry{\m{call}}{E}{k}{k (); k ()} & \stagesubs \sreq{\vfalse} \end{align*}" /> ] - Staged logic: all can be proved by symbolic execution -- - The protocol approach.fn[1]: 287 LoC using Iris, involving an intricate ghost state construction.fn[2] for threading an invariant through the protocol to track the value of the location across calls to the continuation .footnote[.fn[1] Hazel, case_studies/song_et_al_icfp24.v; .fn[2] a history of replies in an auth RA, and one-shot RA for the shared location] --- # Shift and reset .inline-children[ ```ocaml let do_toss () = shift k. k true + k false ``` ```ocaml let toss () = reset (if do_toss () then 1 else 0) ``` ] `shift` captures the continuation up to the enclosing `reset` (here, .boxed[`if □ then 1 else 0`]), reifying it as a function `k`. The result of using `k` twice is `1 + 0` <img class="math-inline" src="4f5b285a4cc6b9c6.svg" alt="=" /> `1`, the number of `true` tosses. --- # Reasoning about shift and reset 1. Encode as effect and use a protocol, parameterised over an "answer postcondition" <img class="math-display" src="7f421b785789245f.svg" alt="\begin{align*} \sshiftz{k}{e_b} & \approx \mathbf{perform}\ \m{Shift} \\ \sreset{e} & \approx \stagetry{e}{\m{Shift}}{k}{e_b} \end{align*}" /> 2. Non-context-local triples.fn[1] <img class="math-display" src="e4ed8bd4e4e88282.svg" alt="\inferrule*{\htriple{P}{C[v]}{Q}}{\htriple{P}{C[\sshift{k}{(k\ v)}]}{Q}}" /> 3. Staged logic (next) .footnote[.fn[1] Mechanized Relational Verification of Concurrent Programs with Continuations, Timany et al., ICFP 2019] --- layout: true # Case study: tossing many coins --- .center-code[ ```ocaml let rec do_toss_n n = if n = 0 then true else let r1 = do_toss () in let r2 = do_toss_n (n-1) in r1 && r2 ``` ] `do_toss_n` tosses <img class="math-inline" src="7774ce1796b85f71.svg" alt="n" style="vertical-align: -0.131pt" /> coins and takes the conjunction of all the results, i.e. it returns `true` if all the coin tosses give `true`. ??? <img class="math-display" src="d0c6eb5e8302ccd4.svg" alt="\begin{array}{l} \m{do\_toss_{n}}\ n \defeq \\ \quad \sens{\hpure{n = 0}}; \sreturn{\vtrue} \\ \quad \vee\ \sens{\hpure{n \neq 0}}; \m{do\_toss}\ () \bind{r_1} \\ \qquad \m{do\_toss_{n}}\ (n{-}1) \bind{r_2} \\ \qquad \sreturn{(r_1 \wedge r_2)} \end{array}" /> --- .center-code[ ```ocaml let rec toss_n n = reset (if do_toss_n n then 1 else 0) ``` ] `toss_n` enumerates all the outcomes, returning the number of all-`true` _sequences_ of tosses. There should be only one such sequence: <img class="math-display" src="d4521d98402fdb3d.svg" alt="\m{toss_{n}}\ n \stagesubs \sreturn{1}" /> ??? <img class="math-display" src="2f88eb0952ab5408.svg" alt="\begin{array}{l} \m{toss_{n}}\ n \defeq \\ \quad \sreset{\m{do\_toss_{n}}\ n \bind{r} \\ \qquad (\sens{\hpure{r}}; \sreturn{1} \vee \sens{\hpure{\neg r}}; \sreturn{0})} \end{array}" /> --- For <img class="math-inline" src="04736f2eddbf06e3.svg" alt="n=3" style="vertical-align: -0.137pt" />, `toss_n` explores a binary tree of depth 3. There is only one all-`true` path. <style> svg.toss-tree line { stroke: #b0b6bf; stroke-width: 1.5; } svg.toss-tree line.hl { stroke: #d33; stroke-width: 3; } svg.toss-tree circle { fill: #fff; stroke: #555; stroke-width: 1.5; } svg.toss-tree circle.hl { stroke: #d33; stroke-width: 2.5; } svg.toss-tree text { font-family: inherit; font-size: 14px; text-anchor: middle; dominant-baseline: central; fill: #333; } svg.toss-tree text.leaf { font-size: 13px; } svg.toss-tree text.elabel { font-size: 11px; fill: #666; } </style> <svg class="toss-tree" viewBox="0 0 600 260" style="width:70%;display:block;margin:1em auto"> <!-- depth 1 --> <line x1="300" y1="30" x2="150" y2="95" class="hl"/> <line x1="300" y1="30" x2="450" y2="95"/> <!-- depth 2 --> <line x1="150" y1="95" x2="75" y2="160" class="hl"/> <line x1="150" y1="95" x2="225" y2="160"/> <line x1="450" y1="95" x2="375" y2="160"/> <line x1="450" y1="95" x2="525" y2="160"/> <!-- depth 3 (to leaves) --> <line x1="75" y1="160" x2="40" y2="225" class="hl"/> <line x1="75" y1="160" x2="110" y2="225"/> <line x1="225" y1="160" x2="190" y2="225"/> <line x1="225" y1="160" x2="260" y2="225"/> <line x1="375" y1="160" x2="340" y2="225"/> <line x1="375" y1="160" x2="410" y2="225"/> <line x1="525" y1="160" x2="490" y2="225"/> <line x1="525" y1="160" x2="560" y2="225"/> <!-- edge labels --> <text class="elabel" x="215" y="54">T</text> <text class="elabel" x="385" y="54">F</text> <text class="elabel" x="108" y="118">T</text> <text class="elabel" x="192" y="118">F</text> <text class="elabel" x="408" y="118">T</text> <text class="elabel" x="492" y="118">F</text> <text class="elabel" x="53" y="183">T</text> <text class="elabel" x="97" y="183">F</text> <text class="elabel" x="203" y="183">T</text> <text class="elabel" x="247" y="183">F</text> <text class="elabel" x="353" y="183">T</text> <text class="elabel" x="397" y="183">F</text> <text class="elabel" x="503" y="183">T</text> <text class="elabel" x="547" y="183">F</text> <!-- internal nodes --> <circle cx="300" cy="30" r="10"/> <circle cx="150" cy="95" r="10" class="hl"/> <circle cx="450" cy="95" r="10"/> <circle cx="75" cy="160" r="10" class="hl"/> <circle cx="225" cy="160" r="10"/> <circle cx="375" cy="160" r="10"/> <circle cx="525" cy="160" r="10"/> <!-- leaves --> <text class="leaf" x="40" y="232" fill="#d33"><tspan font-weight="bold">1</tspan></text> <text class="leaf" x="110" y="232">0</text> <text class="leaf" x="190" y="232">0</text> <text class="leaf" x="260" y="232">0</text> <text class="leaf" x="340" y="232">0</text> <text class="leaf" x="410" y="232">0</text> <text class="leaf" x="490" y="232">0</text> <text class="leaf" x="560" y="232">0</text> </svg> --- The proof requires this lemma, itself proved by induction: <img class="math-display" src="d88ea3649c0651a0.svg" alt="\begin{array}{l} \all{n\,\acc} \\ \quad \sreset{\m{do\_toss_{n}}\ n \bind{r} (\sens{\hpure{\acc{\wedge}r{=}\vtrue}}; \sreturn{1} \vee \sens{\hpure{\acc{\wedge}r{=}\vfalse}}; \sreturn{0})} \\ \quad \stagesubs \sens{\hpure{\acc{=}\vtrue}}; \sreturn{1} \vee \sens{\hpure{\acc{=}\vfalse}} \end{array}" /> 1. The statement must be generalised over an accumulator of intermediate results 2. The continuation is applied at both <img class="math-inline" src="b0aa1e4c37beb817.svg" alt="k\ \vtrue" style="vertical-align: -0.131pt" /> and <img class="math-inline" src="4a3476ac4e3da4f2.svg" alt="k\ \vfalse" style="vertical-align: -2.835pt" />, so we need to know the behaviours of both This sort of generalisation is difficult to automate, so this statement is user-provided. --- A stateful variant: suppose we instrument the program to count the number of continuation resumptions, using a global `ref` `x`. .center-code[ ```ocaml let do_toss () = shift k. x := !x+1; let r1 = k true in x := !x+1; let r2 = k false in r1 + r2 ``` ] This counts the number of edges in the tree, which is <img class="math-inline" src="a081100033826ff1.svg" alt="2^{n{+}1}-2" style="vertical-align: -0.036pt" />. --- The statement and lemma are accordingly generalised: <img class="math-display" src="1449409b67eeed7f.svg" alt="\m{toss_{n}}\ n \stagesubs \ex{v}\sreq{\heapto{x}{v}};\sens{\heapto{x}{(v{+}2^{n{+}1}{-}2)}};\sreturn{1}" /> <img class="math-display" src="82f24b27cfb1d101.svg" alt="\begin{array}{l} \all{x\,n\,\acc} \\ \quad \sreset{\m{do\_toss_{n}}\ n \bind{r} (\sens{\hpure{\acc\wedge r=\vtrue}}; \sreturn{1} \vee \sens{\hpure{\acc\wedge r = \vfalse}}; \sreturn{0})} \\ \quad \stagesubs \ex{v} \sreq{\heapto{x}{v}} \\ \qquad \sens{\heapto{x}{v{+}2^{n+1}{-}2}}; (\sens{\hpure{\acc=\vtrue}}; \sreturn{1} \vee \sens{\hpure{\acc = \vfalse}}) \end{array}" /> but this can otherwise be proved the same way, without any new machinery. ??? <img class="math-display" src="3c3cdde05a3eb138.svg" alt="\begin{array}{l} \m{do\_toss}\ () \defeq \sshift{k}{\ex{v}} \\ \quad \sreq{\heapto{x}{v}}; \sens{\heapto{x}{v{+}1}}; k\ \vtrue \bind{r_1} \\ \quad \ex{v_1} \sreq{\heapto{x}{v_1}}; \sens{\heapto{x}{v_1{+}1}}; \\ \quad k\ \vfalse \bind{r_2} \sreturn{(r_1 + r_2)} \end{array}" /> --- layout: false # Outline - Staged logic and higher-order functions - Effect handlers and shift/reset - __Implementation and mechanisation__ - Conclusion --- # Implementation and mechanisation - An SMT-based verifier, Heifer.fn[1] - Two mechanisations in Rocq, based on 1. simple behavioural refinement 2. contextual refinement - Present effort .footnote[.fn[1] Higher-order Effectful Imperative Function Entailments and Reasoning] --- # Heifer Accepts annotated OCaml programs and searches for proofs, assuming user-provided lemmas. Built on Why3 (SMT, non-foundational). Some interactive facilities. .zoom--1.inline-children.align-top[ ```ocaml let [@pure] rec sum (li: int list) : int = match li with | [] -> 0 | x :: xs -> x + sum xs ``` ```ocaml let rec foldr f li acc = match li with | [] -> acc | x :: xs -> f x (foldr f xs acc) ``` ```ocaml let foldr_sum xs k (*@ ens res=sum(xs)+k @*) = let g c t = c + t in foldr g xs k ``` ] --- # Heifer Case studies - foldr and many small higher-order programs - Loop fusion - Regex interpreter - append, times, and toss using shift/reset --- # Mechanisation 1 - Deeply-embedded syntax, `Inductive` big-step semantics - Shallowly-embedded binders (and separation logic) - Function pointers instead of lambda due to positivity restriction - Bubble-up semantics for shift/reset - Associativity of bind fails; experimental fix using bisimulation of bubbles - Some tactic automation --- # Mechanisation 1 - Case studies - All the `foldr` examples - Landin's knot - append using shift/reset (bisimulation) --- class: no-heading-padding # Mechanisation 1 .center.zoom--15[  ] --- # Mechanisation 2 - Lambda calculus fragment with deeply-embedded binders - (Meta-)contextual small-step semantics for shift/reset - Biorthogonal logical relation to define contextual refinement - IxFree for step-indexed relations --- # Towards a unified system in Lean My present effort is a Lean implementation of all three systems. Its metaprogramming and extensibility allow: - A usable, Heifer-like frontend - Abstraction over binder representation - Implementing sophisticated automation --- class: no-heading-padding # Lean: simple behavioural refinement .center[ .zoom--15[] ] --- class: no-heading-padding # Lean: higher-level tactics .center[ .zoom--15[] ] --- class: no-heading-padding # Lean: Heifer (against axiomatization) .center[ .zoom--15[] ] --- # Outline - Staged logic and higher-order functions - Effect handlers and shift/reset - Implementation and mechanisation - __Conclusion__ --- # Thesis .center[Staged logic is an effective means of automating the <br>verification of higher-order effectful programs.] -- Contributions - A novel refinement-based logic for reasoning about higher-order programs with imperative and control effects - Effective: amenable to proof search, with an implementation (Heifer) - Mechanisations of two useful fragments in Rocq --- # Future work - Mechanise the whole framework - True higher-order store - WIP port of indirection theory - A unified verifier in Lean - Effect-based concurrency via (contextual) refinement --- # Thank you! .center.zoom--10[] .center[https://dariusf.github.io/thesis] ---