Tony's Wiki

Osiris

2 min read

Osiris:Formal Semantics and Program Logics for a Fragment of OCaml

  • .ml OCaml AST — generate ⇒ Rocq shallow embedding
  • use Iris to prove properties about rocq

Design Constraints

  • expressive (concurrency, algebraic effects)

  • aesthetic (modular)

  • compatible with iris

  • small step rules, not aesthetic

  • denotational semantics iTrees, not expressive e.g. algebraic effects

Our semantic style

  • monadic definitional interpreter
    • “monadic combinator API”
  • micro monad - underlying monadic primitives (actual immplementation and stepping semantics)

1st thing, what is the interpreter lloks like

  • eval : env -> epr -> micro val exn
    • env-based, subst-based
    • as we are dealing with anuntyped language, the semantics is untyped and requires as_bool dynamic checks
    • please_eval provided by the monad, to evaluate potentially non-terminating recursive calls in divergence
  • algebraic effects in OCaml
    • match e with exception/effect
    • perform e
    • continue k e
    • dicontinue k e
  • very straightforward library of monadic functions handle perform resume …

Question eval_branch how eval page 10

micromonad

  • is an inductive definition of Ret/Throw/Crash/Stop/Par/Handle computational outcomes
  • a small step reduction over micromonad computation representations, with tracking heaps recording values + counter number of continuations

Semantics please_eval eta e := Stop CEval (eta, e) inject2 ← just stop codes with trivial continuations so please_eval has to be mutually defined with eval

Move to Iris

  • first monadic syntax

  • then reasoning rules in the surface syntax

  • Hoare-Style Reasoning rule about Pure programs

    • in style of small-step stepping + weakest prerecondition
pure m pre post
implies
EWP {{pre}} m {{post}}

With Rocq trusted extraction executive semantics and can be compared to the actual OCaml compiler

Graph View