Brummel
eaa52ff64f
Second tranche of the contracts-against-code audit. Two threads, both applied conservatively under the over-correction guards in docs_honesty_pin.rs (the self-labelled tiebreaker in 0008 and the Diverge-reserved anchor in 0010 are deliberate honest content and were left untouched; design rationale that explains a present-state design principle — semantic-locality, the reuse-as-wrapper reasons — was also preserved). Honesty-rule (0007): demote clear change/deletion narration to present tense. - 0008: drop "they were promoted from ... to ... Recorded here so"; strip the "Iter A"/"Iter B" iteration labels (the descriptive titles carry the meaning); drop "(no longer a carve-out)". - 0001: "were rewired to use ... was deleted at the same time" -> present tense. (The substance was already correct: `pretty.rs` holds only the diagnostic helpers; an audit agent had misread the line as "pretty.rs was deleted" — the file exists, the printer code does not.) - 0012: drop "Per the tail-call survey of existing fixtures" and "Migration of existing fixtures is partial" -> present-state description of which corpus fixtures carry the tail marker. Ratifier integrity: a contract that names a test which does not ratify it is itself a form of the dishonesty this ledger forbids. - 0014 named `bench/architect_sweeps.sh`, which sweeps honesty-anchors and ratifies none of the six verification mechanisms; and claim 5 cited `tests/expected/`, which never existed (git log empty). Point claim 5 at the real golden mechanism (`crates/ail/tests/snapshots/` via `ir_snapshot.rs`) and the footer at each mechanism's actual test. - 0015's four constraints are guaranteed by absence (no thunk/`ref`/ `IORef` node, non-recursive `let`); the named uniqueness in-source tests only count RC consumes, never the constraints. State the by-construction guarantee and point the ratifier at `ast.rs` (the single source of truth for which nodes exist). - INDEX ratifying-test column updated for both to match. All ledger pins green (docs_honesty_pin, design_index_pin incl. every_contract_names_a_resolvable_ratifying_test, effect_doc_honesty_pin, carve_out_inventory); architect honesty sweep clean. Deferred, recommend-only: 0016-method-dispatch carries no invariant absent from 0013 (merge candidate), but a contract-file merge touches INDEX, the retired-counter convention, and cross-refs — a structural call left for explicit direction. Minor history phrasing in 0008's Type::Con.name hash-shift paragraph (§"FnDef.suppress") also left.
46 lines
2.2 KiB
Markdown
46 lines
2.2 KiB
Markdown
# Language-design constraints (binding)
|
||
|
||
## Language-design constraints (binding)
|
||
|
||
The four constraints below are necessary preconditions for RC to
|
||
be sound and complete *without* a cycle-collector backstop. The
|
||
[memory model](0008-memory-model.md) relies on all four:
|
||
|
||
1. **Strict evaluation.** Every `Term::App` (see
|
||
[Data model](0002-data-model.md)) argument is fully
|
||
evaluated before the call. No laziness, no thunks. (Already
|
||
true.)
|
||
2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
|
||
`EXPR` in a scope where `x` is *not* bound. Recursion is
|
||
exclusively via `Term::LetRec` (which binds a fn, not a value)
|
||
and module-level fn defs. (Already true.)
|
||
3. **No shared mutable refs.** Values are immutable once
|
||
constructed. There is no `ref`, `IORef`, `Mutex`, or any
|
||
primitive that allows a value to be mutated from a position
|
||
outside its allocation. (Already true.)
|
||
4. **ADTs are acyclic by construction.** Strict evaluation +
|
||
no-recursive-value-bindings + no-shared-mutable-refs together
|
||
guarantee that any value graph reachable from a binding is a
|
||
DAG. The reference graph has no cycles. (Follows from 1–3.)
|
||
|
||
Laziness, recursive value bindings, shared mutable state, or any
|
||
feature that creates cycles is rejected at design time unless the
|
||
proposal proves the cycle is collectible by an extension (e.g.
|
||
linear ownership).
|
||
|
||
These constraints are the precondition for the
|
||
[memory model](0008-memory-model.md): a sound RC implementation without
|
||
a cycle-collector backstop requires the reference graph to be a
|
||
DAG, which constraint 4 establishes from 1–3. They are also the
|
||
load-bearing structural reason behind several rejections under the
|
||
[feature-acceptance](0004-feature-acceptance.md) bug-class-reintroduction
|
||
discriminator (notably iterated-mutable-state reasoning).
|
||
|
||
Guaranteed by construction, not by a positive test: the AST has no
|
||
thunk, `ref`, or `IORef` node, and `(let x EXPR ...)` binds `x` only
|
||
in the body, never in `EXPR` — there is no construct that could
|
||
violate constraints 1–3, and constraint 4 follows from them. The
|
||
binding force is the design-time
|
||
[feature-acceptance](0004-feature-acceptance.md) gate, which rejects
|
||
any proposal that would reintroduce one of them.
|