Ficus

This Rocq development accompanies the POPL 2027 paper Building Extensible Program Logics through Effect Handlers.

A specific guideline for the artifact evaluation is at AE.md.

Building the development

The development is known to compile with

• Rocq 9.1.0
• std++ 1.13.0
• Iris 4.5.0
• Autosubst dev

It has been tested on Linux x86-64, macOS arm64, and Windows x64 with MSYS2.

The recommended way to install the dependencies is through opam.

Step 1. Install opam if not already installed (a version greater than 2.0 is required).

Step 2. Create a new switch and link it to the project.

opam switch create ficus 4.14.4
opam switch link ficus .

Step 3. Add the Rocq and Iris opam repositories.

opam repo add rocq-released https://rocq-prover.org/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam update

Step 4. Install the right version of the dependencies as specified in the opam files.

opam install . --deps-only

Step 5. Update environment variables.

You can either restart the shell or run a shell-specific command to refresh the current shell session. For example, the command for a typical UNIX-like shell is

eval $(opam env)

And the command for Windows PowerShell is

(& opam env) -split '\r?\n' | ForEach-Object {Invoke-Expression $_ }

Step 6. Build the development.

dune build --profile dev --display=short

Please be aware that this step can take more than an hour on a single core machine, and each Rocq process can take up to 1.5 GiB of memory. The dune build command uses all available cores to build in parallel by default, but if the memory is limited, use the -j <n> flag to limit the number of parallel jobs.

Using the development as a dependency

This repository contains two opam packages:

• rocq-ficus: the development of Ficus, which also includes RelFicus, a complete port of Iris HeapLang, the proofmode support for custom effects, and all effects and worlds used by the case studies of the paper.
• rocq-pureficus: the development of PureFicus. The primary goal of this package is to show that the two primitive effects in FicusLang can be eliminated, but the package itself lacks many features supported by Ficus, notably, it does not contain the relational logic, the proofmode, and effects about crash-recovery and distributed systems. We therefore do not recommend using this package as a dependency.

To use the rocq-ficus package, add this to the depends field of your opam file:

"rocq-ficus" { (= "dev") }

Since this package is not published to the Rocq opam repository, you also need to add an opam pin to the URL of the repository or a local directory containing the development.

To pin to the URL of the repository, add this to the pin-depends field:

["rocq-ficus.dev" "git+https://github.com/u8cat/ficus.git#<commit>"]

where <commit> is the hash of the commit you wish to use.

To pin to a local directory, run

opam pin add --no-action rocq-ficus.dev <directory>

where <directory> is the path of the directory containing the development.

Code structure

• The development of Ficus is at the theories/ directory, and the development of PureFicus is at the theories_pure/ directory. Both follow the same structure.
  • language/*.v: the definition of (Pure)FicusLang
  • language/effects/*.v: the protocols and client-side reasoning rules of effects
  • language/effects/impl/: the handlers of effects and their specifications
  • language/worlds/: the definition and reasoning rules of worlds
  • language/lib/: various library functions; for FicusLang, it includes a full port of the HeapLang standard library
  • program_logic/: the development of Ficus/PureFicus logic
    • transformer.v: the extensible protocol aligning algorithm based on typeclasses
    • tactics.v: the implementation of the ewp_apply tactic
  • rel_logic/: the development of RelFicus logic
  • typing/: definitions of several type systems
  • client_languages/: closed languages modeled by (Pure)Ficus
• Additional end-to-end results are at the case_studies/ directory.
  • yield.v: the proof that yield refines () under run_conc, justifying the soundness of the Ficus concurrency model
  • prophheap.v: the implicit prophecies technique discussed in §5
  • durable_state.v: a closed program using the durable pair mentioned in §6.3
  • ironfleet.v: the proof that yield refines () under run_distr, justifying the soundness of the IronFleet-style distributed execution model
  • hw_queue.v: a port of HeapLang's Herlihy-Wing queue example
  • predet/: the soundness proof of the pre-deterministic model used by PureFicus

A detailed list linking each paper claim to the corresponding Rocq code is at AE.md.

Notation table

Language (§2.1 and §9)

Paper	Rocq	Note
do e	do: e
try e with v k ⇒ e1 | ret v ⇒ e2	shallow-try: e with effect (λ: "v" "k", e1) | return (λ: "v", e2) end	The handler and return clauses are functions.
deep handler	deep-try: e with effect h | return r end
effect tags read, fork, …	EFF_READ, EFF_FORK, …	Tags are integer constants.
§(N)[v]	Eff v N	N is a list of frames.
cont N	ContV N
N[e], K[e]	fill N e, fill K e
pick	Pick	In PureFicusLang, pick is the function Pick and is invoked as Pick #().
observe e	Observe e
label z	Label z	Only in PureFicusLang.
e →* e'	rtc erased_step ([e], ()) ([e'], ())

Protocols, worlds, and ewp (§2.2 and §3)

Paper	Rocq	Note
Ψ(v, Φ)	iEff_car Ψ v Φ
⊥ (protocol)	⊥
Ψ1 ⊕ Ψ2	Ψ1 <+> Ψ2
Ψ1 ⊑ Ψ2	Ψ1 ⊑ Ψ2
tags(Ψ) ⊆ T	tagged_iEff Ψ T	Instead of requiring t ∉ tags(Ψ), some rules remove the tags T from Ψ with T ∖> Ψ.
∃x. v = w ∗ P ∗ (∀y. Q −∗ Φ(r))	>> x >> S! w {{ P }}; << y << R? r {{ Q }}	A syntactic sugar for the basic form of protocols.
ewp e ⟨Ψ⟩ {v. Φ}	EWP e <| Ψ |> {{ v, Φ }}	Both worlds are ⊥. Omitting <| Ψ |> means the protocol is ⊥.
ewp_{W1,W2} e ⟨Ψ⟩ {v. Φ}	EWP e @ W1, W2 <| Ψ |> {{ v, Φ }}
ewp_W e ⟨Ψ⟩ {v. Φ}	EWP e @ W <| Ψ |> {{ v, Φ }}
W1 ⊕ W2	W1 <+> W2
⊥ (world)	⊥
W1 ⊑ W2	W1 ⊑ W2
W1 |⇛W2 P	|=⟨W1,W2⟩=> P
|⇛W P	|=⟨W⟩=> P
P^N (invariant)	inv N P
Tok_I(E)	InvEn E
S^γ(x)	state γ x
ℓ ↦ v	l ↦ v

Relational reasoning (§4)

Paper	Rocq	Note
espec_W e ⟨Ψ⟩	spec_prot e W Ψ
espec^{γ;t}_W e ⟨Ψ⟩	spec_thread_prot γ t e W Ψ
spec^γ_t(e)	spec_thread γ t e
CTX^γ(W, Ψ)	W_SPEC_CTX γ W Ψ
M, C (thread types)	IsMain, IsChild
ℓ ↦s v	l ↦ₛ v
Θ | Γ ⊢ e : τ	Γ ⊢ₜ e : τ	Type variables are de Bruijn indices, so Θ is implicit.
⟦τ⟧^V	interp τ Δ	Δ interprets the type variables.
⟦τ⟧^E(e1, e2)	REL e1 << e2 <| Ψ1; Ψ2 |> : interp τ Δ
Θ | Γ ⊨ e1 ≲ e2 : τ	{Δ;Γ} ⊨ e1 ≤log≤ e2 : τ
e1 ≲ctx^H e2 : τ	Γ ⊨@⟨H⟩ e1 ≤ctx≤ e2 : τ
e1 ≃ctx^H e2 : τ	Γ ⊨@⟨H⟩ e1 =ctx= e2 : τ

Case studies (§5–§7)

Paper	Rocq	Note
primProph(v)	primitive_proph vs
proph(p, v)	proph p vs	The prophesied values are pairs.
♦P	♦P
Tok_C(Rc)	CBrwEn E Rc	E is the set of enabled crash borrows.
\boxed{P | R}	cbrw N P R	N is the namespace of the crash borrow.
ℓ ↦d [vc] v	l ad↦[vc] v	The points-to of the synchronous disk underneath is l d↦ v.
t ⇝ M	t n↦ M	Its persistent lower bound is t n↦ˡᵇ M.
specn^γ_t(e)	spec_node γ t e

Axioms

The only directly used axiom is classic in implementing the OBSERVE effect for PureFicus.

Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ P

The Autosubst dependency uses functional_extensionality_dep.

FunctionalExtensionality.functional_extensionality_dep :
  ∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
    (∀ x : A, f x = g x) → f = g

This affects theorems in theories/typing/ and case_studies/{yield,ironfleet}.v.

License

This Rocq development is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. The text of the license is in COPYING.LESSER, and the text of the GNU General Public License, which it builds on, is in COPYING.

Many files in this repository are also available under the BSD 3-Clause “New” or “Revised” License. Please refer to the header of each file for details. The text of the BSD 3-Clause License is at BSD-3-Clause.txt.