An Enumerable Effect Surface: G8 Boundary Audit, Boundary Policy and an Authority-Drift Gate

Pitch

If every emission and host-code crossing of a composition sits on one authoritative, proved-enumerable table, then a diff of that table is an authority-drift gate and a policy over it is an absolute floor, and neither needs a reviewer to read the code.

Abstract

Code that is regenerated by a tool, whether a template engine, a refactoring pass or a language model, can stay type-correct while quietly gaining new reach: a new service call, a new piece of host code, a loosened sandbox bound. Review of the diff does not scale, and tests of correctness do not see it. We describe the effect surface of revl, a language whose compiler produces one per-component boundary table (guarantee G8) listing every emission call site and every host extern a component reaches, with an unclassified extern refused at parse. A Lean development proves the table is complete and sound over a classified statement lattice. Three gates read the same audit graph: admission (do consumers still hold), revl audit --diff (did the new generation add or loosen a crossing, failing unless acknowledged, never failing on removals), and an operator boundary policy (allow and deny rules by capability, component pattern and realm, plus cross-tenant disjointness) that refuses admission with a named chain. A profile tool diffs declared reach against an observed run, names over-declared authority and proposes the least-authority declaration. The drift diff also covers secrets, environment bounds, confinement reach, backends, recovery inverses, register floors and cardinality ceilings. We report what is shipped and tested, and list the evaluation still needed: precision of the drift gate over real regeneration traces and comparison with manifest-permission diffing.

Problem and claim

Existing change-control for authority is either manifest-based (the author lists permissions; a tool diffs the list) or runtime-based (a sandbox enforces whatever it is configured with). A manifest can disagree with the code, and a sandbox policy says nothing about what changed between two versions. In a setting where components are regenerated often, the dangerous change is a widening that still passes every contract check (docs/audit-diff.md, "Authority vs. admission").

The claim: because the language makes the boundary surface a computed, proved-enumerable artifact of the code rather than a declared list, a set difference over stable crossing tokens is a sound drift check for what the surface covers, and a policy over the same table gives an absolute floor. Loosening authority is the direction that fails: a new crossing, a new or loosened secret or environment binding, or a reach weakening on a crossing that stays. Removing authority never needs review.

Contributions

1. G8 as a theorem: the audited surface contains every reached crossing and only declared crossings (formal/RevL/Theorems/G8_ClassifiedBoundary.lean:74,86), with the earlier marker-level form kept and labelled weaker because it scores an effect carrying an emission as empty by definition (formal/RevL/Theorems/G8_Boundary.lean:63-82, formal/STATUS.md:170-171).
2. An authority-drift gate: revl audit --diff over stable crossing tokens (emit:, host:, secret:, env:), failing on unacknowledged additions, with --accept / --accept-all, and extra differs for reach weakening, capability scopes, backends, recovery inverses, register floors and cardinality (docs/audit-diff.md; src/revl/audit_diff.py:300-678).
3. A boundary policy as the third gate leg: allow and deny by capability, component glob and realm, tenant disjointness, an agent-sandbox profile, with a why-trace on refusal and a rule that an unnameable * reach satisfies no named allow-list (docs/boundary-policy.md:8-60).
4. Profile-based over-declaration detection and a least-authority repair patch derived from an observed run, proposed and never applied (docs/revl-profile.md sections 1 and 7).
5. Mandatory extern classification so host code is on the surface: an unclassified extern does not parse (docs/syntax-2.0.md:598-603).

Related work

Evidence on main

Numbers that exist

• Formal: G8 row is "3 + 9" theorems in formal/STATUS.md:55, with an S8 oracle row per reconstructed statement and a coverage ratchet; the exact corpus count is printed by the gate and was not run for this draft.
• Test function counts by grep: 37 in tests/test_audit_diff.py, 23 in tests/test_policy.py, 10 and 9 in the profile test files. These are not measurements of the system.
• No false-positive rate, no regeneration-trace study, no latency number exists in the tree.

Paper outline

1. Introduction: regenerated code and the invisible widening.
2. The surface: crossings, tokens, extern classification, * for the unnameable.
3. G8 formalised: marker-level versus lattice form, what the oracle checks.
4. Three gates: admission, drift, policy; why they are orthogonal.
5. Drift beyond emissions: secrets, env bounds, confinement reach, registers, cardinality, backends.
6. Profile and repair patch: over-declaration from observed use.
7. Evaluation.
8. Related work.
9. Limits.

Threats to validity and limits

• The surface is complete for what the checker classifies; host-code bodies are not analysed, so a crossing hidden inside a classified pure extern is trusted by classification (docs/syntax-2.0.md:596-603). The syntax document says the place full fluency is wanted is exactly the place checking was never promised (docs/syntax-2.0.md:605-607); the surface says a host block exists and what class it has, not what it does.
• A drift diff compares two audits, so a baseline captured from a bad version blesses its authority.
• The profile tool's patch rests on one trace; the doc says re-running the gate is the backstop.
• --accept-all is an escape hatch whose use is a process question, not a technical one.
• Policy-diff over a WAL is withheld when scope is not captured (src/revl/policy_diff.py:7-18); it does not preview real runs today.
• The marker-level Lean G8 theorem is weak; the paper cites the lattice form and says why.
• No user study and no adoption data are in the tree. Still to evaluate: drift-gate precision on real regeneration episodes against a manifest-diff baseline, a seeded-widening benchmark, and policy usability.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 40 checked, 5 corrected.

Cite this draft

@misc{revlp40,
  author       = {Thomas Moussajee},
  title        = {An Enumerable Effect Surface: G8 Boundary Audit, Boundary Policy and an Authority-Drift Gate},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P40.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.