A read-only coherence skim across the project (the contract edits
themselves verified code-true, INDEX bijection exact, all pins green)
surfaced two pre-existing drifts — both predating this audit, neither
from the contract pass. Fixed in the same conservative style.
1. Model 0008 (ownership-totality) §1+§2 narrated the `Implicit`
leak in the PRESENT tense, contradicting the file's own STATUS
header (Implicit deleted via #55, 76b21c0), contract 0008 ("There
is no `Implicit`"), and the live fixture. §1 claimed "This is
documented intentional behaviour today ... the fixture asserts
`live = 1`"; the `rc_let_implicit_returning_app.ail` fixture now
asserts `live = 0` (its own comment marks the `live = 1` lane as
"Pre-0062"). §2 claimed "the typechecker already treats
`Implicit ≡ Own` (`ParamMode::mode_eq`)"; that variant and fn no
longer exist. Rewrote both to past tense (the leak the cutover
fixed). The STATUS header had been updated at cutover; these two
bodies had not. The design argument (§2-§8) is untouched — the
header frames it as the whitepaper's reasoning and points readers
to the contract for current state.
2. Contract 0010 (scope-boundaries) referenced 18 example fixtures as
`examples/*.ail.json` — files that exist only as `.ail` since the
form-A-default migration (JSON is derived in-process; only the
twelve carve-outs remain `.ail.json` on disk). All 18 → `.ail`
(every target verified present). Same single stale file-path ref in
model 0001 §3 (`list_map_poly`) corrected; model 0001's other two
`.ail.json` mentions are intentional references to the canonical
JSON *form* (the whitepaper's subject) and were left.
Honesty sweep clean; design_index_pin / docs_honesty_pin /
effect_doc_honesty_pin green; no dangling example path remains.
The 0008 totality core shipped via #55 (spec 0062, 76b21c0), but both
model whitepapers still claimed "nothing here is shipped" — drift the
architect would flag.
- 0008: STATUS now "partially realised". Records what landed (binary
ParamMode, value-type trivial-own, no mode-polymorphism, the hash
reset) and points at the contract ledger for current-state facts.
Marks §3.4/Q3 naming as resolved (verbal own/borrow kept, user
decision); leaves the return-side escape axis (§5.1-5.2), multi-return
(§5.3), and Q2/Q4 as the genuine remainder. escape.rs is named as the
opt-only stack-promotion pass, not the §5.2 reachability check.
- 0009: STATUS stays "nothing shipped" (true), but the runtime-axis-dual
paragraph now notes 0008's annotation axis landed, so 0009's
precondition is met rather than hypothetical; the §8-Q3 coupling to
0008's unshipped return-escape pass is flagged as still ahead.
Contract 0008-memory-model.md needed no change — already current.
A design discussion on 0008 surfaced four refinements; this records them
in the exploratory model. Still design exploration, not a spec commitment.
- §3.4 (new): the keywords are adjectival, not verbal. `own`/`borrow`
are acquisition verbs — native on a parameter (the callee acquires),
backwards on a return (the callee disposes; §3.1's own text switches
feet between the two readings). Naming the mode adjectivally
(`owned`/`borrowed`) describes the value the receiver holds and is
position-independent, strengthening §3's uniformity rather than
breaking it. Carries a safety stake, not only readability: a wrong
`own` is the double-free (§6), and the verb form is a mis-annotation
pump pointed that way. Notes the corroborating `ret_mode: ParamMode`
type-name smell (a return mode is a covariant promise, not a
contravariant param demand).
- §4.4: "fixed modes suffice" is contingent on the point-free cut, not a
standalone theorem. Adds the structural discriminator — today's HOFs
control both ends of their seam, so the seam mode is determinate; only
the wire-two-black-boxes kind (point-free) needs a mode variable.
- §5.1–5.3 (new): a tuple question exposed that `ret_mode` is flat but
ownership is a tree over the type — a single top-level `Own` on a
mixed Pair (owned field + borrowed field) decs borrowed data on drop.
Resolved to regime A (borrows may not escape into an escaping heap
structure → transitive ownership → flat `ret_mode` sound), not a
per-field mode tree (regime B = lifetimes). For compound returns,
verification is constitutive of the flat representation's meaning, not
a separable phase — sharpening Q2 to "must" there. Multi-return is the
ownership-honest return path (flat per-position modes, no reachability
pass) but does not subsume the typed boxed aggregate; the boxing point
is the ownership commit.
- §7: Q2 sharpened (compound returns force it), Q3 rewritten (adjectival
keywords + the pre-cutover timing, since a post-cutover rename is a
second irreversible hash reset), Q4 added (multi-return adoption);
resolved-footer extended with regime A and multi-return≠tuple.
- §8 (new): relation to Rust. Concedes the primitive-level convergence
(own/borrow ≈ move/borrow, regime A ≈ Rust's escape rule, unboxed
product ≈ tuple, RC ≈ Rc/Arc), then names what AILang drops and why:
no lifetime polymorphism (the point-free cut removes the pressure that
makes Rust carry it), no `&mut`/shared-XOR-mutable (no shared mutable
refs; mutation rides uniqueness, the Clean lineage), no elision (§2's
no-defaults is the opposite of Rust's elision). Scoped to the
totality-relevant divergences; the broader memory-model lineage is
cross-referenced to 0004 rather than duplicated.
Exploratory model that converges the direction sparked by the
typed-MIR fieldtest Implicit-return leak (spec 0061). It is not
current state and not an approved milestone — the surface still
defaults ParamMode::Implicit; the file fixes a future shape before
committing it to specs.
The converged shape:
- Ownership is authored, never defaulted. Implicit is removed from
the authorable surface; every parameter and return carries
own/borrow. A default cannot be half-removed, so totality is the
only coherent stopping point.
- Value types take trivial-own; borrow over a value type is an
error. The surface stays uniform so the author needs no knowledge
of which types are heap.
- No mode-polymorphism. A type-variable position is never a hole
under fixed modes — it takes a concrete own/borrow. Mode variables
would only remove duplication, and the reuse-across-modes need is
confined to point-free combinators (cut by the language identity)
and the consume-vs-preserve container duality (better expressed as
two named functions). Structurally, AILang iterates via tail-app,
not passed-function combinators, so the higher-order own/borrow
clash does not arise. ParamMode stays binary {Own, Borrow}.
Left open: cutover shape, verification sequencing, glossary naming.
The one irreversible consequence — a corpus-wide module-hash reset
once Implicit stops eliding the mode fields from canonical JSON — is
named for deliberate sign-off.
Brummel