Error Credits and Approximate Higher-Order Reasoning
Prerequisites. Direct starred prerequisites: chapter 45 and chapter 163. No later core chapter depends on this route.
Consider the program 𝑒≜𝗅𝖾𝗍𝑛=𝗋𝖺𝗇𝖽3𝗂𝗇𝗂𝖿𝑛≤1𝗍𝗁𝖾𝗇𝗍𝗍𝖾𝗅𝗌𝖾𝑒′,𝑒′≜𝗅𝖾𝗍𝑘=𝗋𝖺𝗇𝖽1𝗂𝗇𝗂𝖿𝑛+𝑘≤2𝗍𝗁𝖾𝗇𝗍𝗍𝖾𝗅𝗂𝖿𝑛+𝑘=3𝗍𝗁𝖾𝗇𝖿𝖿𝖾𝗅𝗌𝖾Ω, where 𝗋𝖺𝗇𝖽𝑁 draws uniformly from {0,…,𝑁} and Ω diverges. Enumerating the tree: 𝑛∈{0,1} with probability 1/2 returns 𝗍𝗍; 𝑛=2 with probability 1/4 splits into 𝗍𝗍 and 𝖿𝖿, each of probability 1/8; 𝑛=3 with probability 1/4 splits into 𝖿𝖿 and divergence, each 1/8. So Pr[𝑒returns𝗍𝗍]=58,Pr[𝑒returns𝖿𝖿]=14,Pr[𝑒diverges]=18.
Now try to prove the bound 1/4 by a rule that charges a fixed error at each sampling point. The first draw has four outcomes, two of them leading away from 𝗍𝗍, so a branch-insensitive rule charges 1/2; the second draw has two outcomes, one of them bad, so it charges another 1/2; the total is 1, which asserts nothing. The loss is exactly the information that the error required by the continuation depends on the value drawn: after 𝑛≤1 no error is needed at all, and after 𝑛∈{2,3} an error of 1/2 is needed. Averaging those four values gives 1/4, the true bound.
What must therefore be added to a program logic is a quantity that can be split, spent, and made to depend on an intermediate value — in short, an owned resource. This chapter takes error probability to be such a resource, proves the rules that govern it, and states the adequacy theorem that connects a derivation to the probabilities enumerated above. Because the resource is owned rather than global, the rules compose across function calls and stored higher-order code, which is what a fixed per-call budget cannot do.
The language is 𝜆randref: an untyped call-by-value 𝜆-calculus with pairs, sums, recursion, a higher-order store with allocation, dereference and assignment, and the sampling primitive 𝗋𝖺𝗇𝖽𝑁 for 𝑁∈ℕ, whose reduction chooses uniformly among {0,…,𝑁}. Its operational semantics is a step-indexed distribution over configurations; Prexec𝑒[𝜑] denotes the probability that 𝑒 terminates in a value satisfying the meta-level predicate 𝜑, and a configuration with no reduction and no value is stuck.
The logic is an Iris-style higher-order separation logic over that language: assertions form a step-indexed BI algebra with the separating conjunction ∗, the persistence and later modalities, ghost ownership 𝗈𝗐𝗇𝛾(𝑎) over a resource algebra, invariants, and the fancy update; a Hoare triple {𝑃}𝑒{𝜑} is defined from a weakest precondition 𝖶𝖯𝑒{𝜑} whose sampling clause is a graded lifting modality carrying an error budget. The new assertion is the error credit𝐸(𝜀) for 𝜀∈[0,1].
From chapter 45 this chapter imports the higher-order ghost-state interface: resource algebras, the ownership assertion, the frame-preserving update, and the invariant rules. From chapter 163 it imports the guarded, step-indexed setting in which the weakest precondition is defined by guarded recursion. From chapter 172 it uses 𝖯𝖬𝖪-bind and 𝖯𝖬𝖪-lim: bind of subprobability kernels, and the limit facts proposition 172.24, proposition 172.25 used to define the execution distribution as a supremum of finite unfoldings. No result of chapter 176 or chapter 177 is imported, and none is strengthened by anything proved here.
The three laws are what make the resource behave like error probability. Splitting is additivity of the error budget; weakening discards budget that a proof does not need; and owning a full unit of error is a contradiction, because a claim holding with probability at least 0 says nothing, so any branch that would need a full credit may be discarded outright.
The first rule is the one the opening calculation demanded: the credit required before the draw is the average of the credits required after it, so the budget may be distributed unevenly across outcomes. The second is derived, and its derivation shows the third law of definition 178.2 doing work.
Proof of Lemma 178.4 — Avoiding a list of outcomes
Proof. Apply ht-rand-exp with E2(𝑖)=1 if 𝑖∈𝑥𝑠 and E2(𝑖)=0 otherwise. Its side condition computes 1𝑁+1∑𝑖E2(𝑖)=length(𝑥𝑠)/(𝑁+1), which is the precondition of ht-rand-err. The postcondition is 𝑛.𝐸(E2(𝑛)). In the case 𝑛∈𝑥𝑠 the postcondition is 𝐸(1), which entails False by the third law and hence entails 𝑛∉𝑥𝑠; in the case 𝑛∉𝑥𝑠 the postcondition already gives 𝑛∉𝑥𝑠. Combining the two cases yields {𝐸(length(𝑥𝑠)/(𝑁+1))}𝗋𝖺𝗇𝖽𝑁{𝑛.𝑛∉𝑥𝑠}. ◻
Prove {𝐸(1/4)}𝑒{𝜑} with 𝜑 the postcondition “returns 𝗍𝗍”. First, for the subprogram 𝑒′ under the assumption 𝑛=2 or 𝑛=3, prove {(𝑛=3∨𝑛=2)∗𝐸(1/2)}𝑒′{𝜑}: the draw 𝗋𝖺𝗇𝖽1 has two outcomes, exactly one of which leads away from 𝗍𝗍 — for 𝑛=2 it is 𝑘=1, for 𝑛=3 it is 𝑘=0 — so lemma 178.4 with a singleton 𝑥𝑠 spends 1/2 and rules that outcome out.
Second, for 𝑒 itself, take E2(𝑖)={0𝑖<2,1/2𝑖∈{2,3},143∑𝑖=0E2(𝑖)=14(0+0+12+12)=14, so ht-rand-exp gives {𝐸(1/4)}𝗋𝖺𝗇𝖽3{𝑛.𝐸(E2(𝑛))}, and ht-bind composes it with the two continuations: for 𝑛≤1 the continuation returns 𝗍𝗍 with no credit, and for 𝑛∈{2,3} it is the triple for 𝑒′ just proved. The derived bound 1/4 equals the enumerated probability Pr[𝑒returns𝖿𝖿] exactly; the divergence probability 1/8 is not charged, which is what makes this a partial-correctness statement.
★★☆ Recompute example 178.5 with the branch-insensitive rule that charges length(𝑥𝑠)/(𝑁+1) at every draw with the same 𝑥𝑠 for all outcomes, and show that the derived bound is 1. Identify the exact place where the value dependence is lost.
★★☆ State and derive the analogue of lemma 178.4 in which outcomes in 𝑥𝑠 need not be excluded but require credit 1/2 each, and compute the resulting precondition for 𝑁=3 and |𝑥𝑠|=2.
The adequacy theorem of section 178.3 is a statement about the full language with a higher-order store. For the fragment in which the opening example lives — finitely branching sampling, no store, no recursion except the constant Ω — the same statement can be proved directly, and the proof shows which property of the credit rules carries the bound.
Let the finite fragment have expressions Ω, values 𝑣, 𝗋𝖺𝗇𝖽𝑁, and 𝗅𝖾𝗍𝑛=𝑒1𝗂𝗇𝑒2. Its execution distribution exec𝑒 over values, defined by the finite tree of draws, assigns mass to values and leaves the divergence mass unassigned. A credit derivation of 𝜀⊢𝑒:𝜑 is generated by
Proof of Theorem 178.7 — Adequacy for the finite fragment
Proof. Induction on the derivation.
F-Val.exec𝑣=𝛿𝑣 and 𝜑(𝑣) holds, so the probability of ¬𝜑 is 0.
F-Loop.execΩ assigns no mass to any value, so the probability is 0.
F-Weak, F-Fail. Monotone in 𝜀, and every probability is at most 1.
F-Bind. The execution distribution of the sampling let is the uniform mixture 1𝑁+1∑𝑖exec𝑒2[𝑖/𝑛], by the sampling rule of the operational semantics and example 172.26. Hence Prexec𝑒[¬𝜑]𝑚𝑖𝑥𝑡𝑢𝑟𝑒=1𝑁+1∑𝑖Prexec𝑒2[𝑖/𝑛][¬𝜑]𝐼𝐻,𝑚𝑜𝑛𝑜𝑡𝑜𝑛𝑖𝑐𝑖𝑡𝑦=1𝑁+1∑𝑖𝜀𝑖=𝜀. ◻
The derivation of example 178.5, transcribed into definition 178.6, uses F-Bind at the outer draw with 𝜀0=𝜀1=0 and 𝜀2=𝜀3=1/2, giving 𝜀=1/4; at each inner draw it uses F-Bind with one branch of cost 0 and one of cost 1, giving 1/2. By theorem 178.7 the bound 1/4 is sound. It is also least: the enumerated probability of returning 𝖿𝖿 is exactly 1/4, so no 𝜀<1/4 can be derivable for this 𝑒 and 𝜑 without contradicting the theorem.
Let the carrier be ℝ≥0 with addition as composition and no unit element beyond 0; the authoritative construction of chapter 45 then provides elements ∙𝜀tot and ∘𝜀, with validity of ∙𝜀tot∗∘𝜀 requiring 𝜀≤𝜀tot. Define 𝐸(𝜀)=𝗈𝗐𝗇𝛾err(∘𝜀), for a fixed ghost name allocated once.
Proof of Lemma 178.10 — The interface laws hold in the model
Proof. Splitting is the equation ∘𝜀1⋅∘𝜀2=∘𝜀1+𝜀2 in the resource algebra, which is the additivity of composition, together with the rule that ownership of a composite is the separating conjunction of the ownerships. Weakening is a frame-preserving update from ∘𝜀1 to ∘𝜀2 for 𝜀2<𝜀1: any frame ∘𝑓 compatible with the former, meaning 𝜀1+𝑓≤𝜀tot, is compatible with the latter. For the third law, the weakest precondition is defined so that the authoritative element never exceeds 1; owning ∘1 together with the authoritative element forces 𝜀tot≥1 and leaves no room for the invariant’s own share, so the assertion is inconsistent. ◻
The following are imported at exactly these signatures.
Aguirre et al.’s Theorem 6, adequacy for partial Eris: if ⊢{𝐸(𝜀)}𝑒{𝜑} then Prexec𝑒[¬𝜑]≤𝜀, and moreover the probability that 𝑒 gets stuck is at most 𝜀, so 𝑒 is safe with probability at least 1−𝜀. Neither bound is 0: a diverging trace satisfies every partial specification, and 𝜀 bounds the probability of terminating outside 𝜑.
Their Theorem 7, adequacy for total Eris: if ⊢⟨𝐸(𝜀)⟩𝑒⟨𝜑⟩ in the total logic then Prexec(𝑒,𝜎)[𝜑]≥1−𝜀 for every initial state 𝜎.
Their Theorem 8: let 𝜀≥0; if for all𝜀′>𝜀 the total triple ⊢⟨𝐸(𝜀′)⟩𝑒⟨𝜑⟩ is derivable, then Prexec(𝑒,𝜎)[𝜑]≥1−𝜀. The quantifier over 𝜀′ is in the meta-logic, and the passage from the family of triples to the single conclusion is a continuity argument there, not a rule of the object logic.
Theorem 178.7 is the finite instance proved locally; the imports supply the statements for the full language with higher-order store.
For the opening program, the partial bound is 𝜀𝑝=1/4, charging only the terminating runs that return 𝖿𝖿. The total bound is 𝜀𝑡=3/8, charging in addition the divergent branch of probability 1/8, since a total triple asserts termination with probability at least 1−𝜀𝑡. Indeed Pr[𝑒returns𝗍𝗍]=5/8=1−3/8. The two numbers are different statements about the same program, and neither follows from the other: 𝜀𝑝 cannot be strengthened to 0 merely because the program is almost surely correct on its terminating runs, and 𝜀𝑡 cannot be lowered to 𝜀𝑝 without proving termination.
A Coq development accompanies the source and is pinned in the reference library; it contains the resource algebra of definition 178.9, the weakest precondition with its graded lifting, the rules of definition 178.3, and the three theorems of convention 178.11. Replaying it establishes that those statements have machine-checked proofs against the displayed definitions; it does not establish anything about definition 178.6, which is this book’s own fragment, nor does it substitute for theorem 178.7. When a rule of definition 178.3 is said to be checked, the claim is about a named lemma of that development.
Error credits bound the probability of an incorrect outcome. They are not expected-cost potential: the credit algebra of definition 178.9 is additive in a quantity bounded by 1, while the potential of chapter 177 is an unbounded nonnegative quantity paying for ticks, and the two soundness statements bound different things — a probability there, an expectation here. A comparison between them is a translation to be proved, not an identification; no rule of one system is imported into the other in this book. Likewise, Theorems 7 and 8 of convention 178.11 are a terminal extension: nothing in chapter 176 or chapter 177 is strengthened by them.
★★☆ Give a program that diverges with probability 1 and prove {𝐸(0)}𝑒{𝜑} for every 𝜑 in the finite fragment, using definition 178.6. State which clause of theorem 178.7 makes this sound and why the corresponding total statement fails.
★★☆ Write out the F-Bind case of theorem 178.7 for 𝑁=1, replacing the mixture identity by an explicit two-term computation, and identify where the induction hypothesis is applied.
★★☆ Show that F-Bind with the average replaced by the maximum is sound but derives 1/2 for the opening program, and that with the average replaced by the minimum it is unsound, by exhibiting a program and a false bound.
★★☆ Formulate a total-correctness variant of definition 178.6 in which F-Loop requires 𝜀=1, prove the corresponding adequacy statement Prexec𝑒[𝜑]≥1−𝜀, and derive 3/8 for the opening program.
★★★Practical project.error-credit-arithmetic-checker Build a certificate checker for the finite credit arithmetic of definition 178.6. A certificate is a tree of the five rules; the checker recomputes each rule’s side condition in exact rational arithmetic and reports either the derived bound or the first violated side condition. A second component enumerates the program tree exactly, reporting the three probabilities of returning a value satisfying the postcondition, returning one that violates it, and diverging.
The invariant to maintain is that every credit is a reduced rational in [0,1], that F-Bind recomputes the average rather than accepting a supplied value, and that the enumerator’s three probabilities sum to exactly 1.
The concrete result is the pair of verdicts for the program of the chapter opening. The acceptance test is decidable and exact: the checker must accept the partial certificate at 𝜀=1/4; it must reject every strictly smaller rational bound for the same certificate, reporting the recomputed average 1/4; it must accept the total certificate of exercise 178.10 at 𝜀=3/8 and reject it at 1/4; and the enumerator must report exactly 5/8, 1/4, 1/8. Replaying the pinned Coq development is separate mechanization evidence for convention 178.11; the arithmetic checker establishes theorem 178.7 for the certificates it accepts and does not prove adequacy for the full language.