44 Proofs about effects — writing “what it can do” into the type

44.1 Effects are sets of atoms#

An effect is a set of atoms. It can hold several atoms, as in effects io alloc .. Then there is a natural order — ε₁ ⊑ ε₂ is ε₁ ⊆ ε₂, “ε₁ does less than ε₂”. The subset relation forms a lattice, the join is union, and none (the empty set) is the bottom.

It is the same shape as chapter 40′s type lattice. The same mathematics answers a different problem. And the judgement on small machines becomes one ⊆. Code that allocates must not translate for a machine without a heap (chapter 30), and with effect declarations it is enough to ask “is this op’s effect within the set this tier supports”.

            {io, alloc}
             ▲       ▲
            {io}     {alloc}
             ▲       ▲
              none

 propagation  if f calls g (effects io) and h (effects alloc),
              effects(f) ⊇ {io} ⊔ {alloc} = {io, alloc}      short of it: E-EFFECT
 gating       if the set a heapless board supports has no alloc,
              {io, alloc} ⊄ that set                         it does not translate for that board

A hierarchical lattice splitting io into {read, write} is possible too. This language uses a flat one for now. The precision a hierarchy gives is already available from capabilities, and a flat lattice keeps the ⊆ test simple so the cost is visible. Express precision in two places and the two begin to diverge.

44.2 Four rules the processor enforces#

Rule 1 — propagation. If f calls g, then effects(f) ⊇ effects(g). Otherwise it is E-EFFECT (E-EFFECT-CALC for a fn). It stops an op marked effects none from secretly writing a file (chapter 15).

Rule 2 — purity. A fn writing to the caller’s buffer is E-EFFECT-PURITY. fn computes values and proc does work. If the criterion is the shape of a word, holes appear. At one time an actor’s handlers were counted as pure because they were not proc, so a handler mutating actor state could declare effects none and nobody objected. The same offence was caught on one side and not the other.

Rule 3 — an effects clause is a set of atoms.

module effect_dup .
rem expect: E-EFFECT-DUP

proc shout input out cap io . output u64 . effects io io . do
  return write_out out 1 "hi\n" .
end

$ lowentc --check effect_dup.low
effect_dup.low:4:0 E-EFFECT-DUP: an effect atom appears more than once in the `effects` clause — the row is a SET, not a list. A repeat says nothing the first one didn't, and the reader has to decide it's noise (RFC-0057 E3)

module effect_typo .
rem expect: E-EFFECT-UNDEF

proc ping input out cap io . output u64 . effects netwrok . do
  return 0 .
end

$ lowentc --check effect_typo.low
effect_typo.low:4:0 E-EFFECT-UNDEF: unknown effect (the vocabulary is closed: none/alloc/heap/io/wait/concurrent/lock/atomic/unsafe/device/page_fault/blocking/cancel/detach/panic/state) — a typo here silently declares the op PURE

Writing the same atom twice is rejected. A duplicate in a set means nothing, and the reader has to decide whether it is noise. A nonexistent atom is caught as a typo — as the diagnostic says, a typo passing silently would declare the op pure. The rule looks obvious, but there was a time the implementation read only the first word of the clause. Then effects io alloc registered only io, and atoms from the second on were as good as absent. A defect in the code reading declarations disables the whole declaration system.

Rule 4 — stopping is not an effect. This is the most thought-provoking part of the chapter.

module trap_not_effect .
rem run: pick [1,2,3] 1
rem trap: pick [1,2,3] 7

rem it stops when out of range, but this op is still a pure fn
fn pick input s slice u8 . input i u64 . output u8 . do
  return index s i .
end

$ lowentc --run pick trap_not_effect.low [1,2,3] 1
pick([1,2,3], 1) = 2
  arg0 (written) = [1,2,3]
$ lowentc --run pick trap_not_effect.low [1,2,3] 7
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

index s i stops when out of range. So should pick carry the panic effect? No. panic counts only an explicit panic "…". The possibility of stopping is what contracts speak of, not effects. The danger of index can be removed with requires lt i (len s), and the processor really does remove that check (chapter 41). An effect mark is never removed. Marking something removable as an effect makes the mark permanent, nearly every op ends up with panic, and the mark loses meaning.

 what ends the op              where it is written         can it disappear
 panic "…"  (intended)         effects panic               no — it always stays
 index out of range (breach)   requires lt i (len s)       the check goes once proven

44.3 Capabilities — the partner of effects#

If effects say “what kind of work”, capabilities say “where the right to do it came from”. Writing to the screen requires receiving cap io as an argument; it cannot be pulled out globally from anywhere. This object-capability model gives two things.

• Attenuation. A received right can be narrowed before passing it on. The precision a flat effect lattice lacks is obtained here.
• Local audit. Looking at an op’s signature shows everything it can touch. That there are no hidden global passages is the point.

44.4 Effect soundness — not circular#

module recursive .
rem run: main

proc stars input out cap io . input n u64 . output u64 . effects io .
  requires le n 10 .
do
  if eq n 0 . do
    return write_out out 1 "\n" .
  end
  let w u64 be write_out out 1 "*" .
  return add w (stars out (sub n 1)) .
end

proc main input out cap io . output u8 . effects io .
do
  return narrow u8 (stars out 5) .
end

$ lowentc --run main recursive.low
*****
main() = 6

stars is recursive, calling itself, and declares effects io. At a call site the processor uses the callee’s declaration rather than walking its body again. At first glance this looks circular — a declaration trusts a declaration.

44.5 Optimisations relying on effects are legitimate#

The legitimacy of optimisations stands on effect soundness. At the effect layer, pure pieces may be reordered (pure_calls_commute) or deleted (dropping_pure_is_legal) with the same effects happening. The proof raised to the value layer is LowentOpt.v. In a model with values, state and an output stream, reordering, common subexpression elimination, memoisation and dead code elimination were all four proven legitimate.

The key is one line — a value depends only on the places it reads (value_depends_only_on_reads). And counterexamples showed the premises are not decoration. Reordering effectful pieces changes a value from 14 to 7, and deleting a piece that prints shrinks the output. One theorem, one counterexample — without the counterexample, the theorem would be true even if the condition were overly strict.

44.6 What is not proven#

• That the implementation matches the model is an empirical correspondence backed by tests and back-end cross-checks (chapter 50).
• The rule by which task_group absorbs concurrent is not a ⊆ discipline but discharging a requirement, so it is outside the model.
• In effect-based optimisation, call boundaries (raising the purity judgement to op boundaries) and the moment of stopping are outside.
• The precision limit of a flat lattice. Refinements like io ⊑ {read, write} were not done, and capability attenuation stands in for them, with no argument that the two give the same precision.
• No effect-row polymorphism. An op “inheriting the caller’s effects as they are” cannot be written, so higher-order ops must declare the widest effects.
• Some atoms are vocabulary only. page_fault, blocking, cancel, detach and others can be declared but have no operation producing them yet, so propagation of those atoms is thinly tested in practice.