Specify provenance and accounting for mixed typed occurrence indexing

This commit is contained in:
2026-09-24 03:48:12 -07:00
parent 29e4f67206
commit 7cfdd13d3a
4 changed files with 276 additions and 0 deletions
+13
View File
@@ -536,3 +536,16 @@ be reserved before copying or retention. Revisit the split if actual ownership
work shows sites cannot be retained without duplicated models or repeated parsing.
Public source8, mixed editing, checked-save and root reconciliation remain later
dependencies, not capabilities delivered by this design decision.
## 2026-09-24 — preserve mixed bundle authority through index construction
Adopt the [mixed typed-index contract](analysis-mixed-index-contract-20260924.md):
consume the sealed complete-Project witness into a distinct read-only owner and
reuse private structural/token verification, with aggregate retained-ledger
accounting. A copied verifier would duplicate correction work; reparsing into
the old numeric-source Index would discard bundle/profile authority. The
[independent review](analysis-mixed-index-review-20260924.md) resolved storage
domain and completeness-proof ambiguities before adoption. This is a bounded
implementation decision, not runtime acceptance or full editing parity. Revisit
if a concrete verifier invariant prevents reuse or multiple retained owners
become necessary; no generic public indexing framework is justified now.
+5
View File
@@ -214,6 +214,11 @@ the semantic boundary implemented by the separate private checkpoint below.
Published private complete-Project source
**aaec78fcc9b273d1485497126392afdd1fb2e54e** retains the original syntax, bundle,
budgets and limits while resolving/admitting the complete ordinary/typed model.
The next [mixed typed-index contract](analysis-mixed-index-contract-20260924.md)
is accepted after source review and resolved accounting/completeness findings;
it has no implementation or runtime acceptance yet. It consumes the sealed
Project witness, reuses private index verification and keeps old updater
authority separate. Complete mixed editing and public source8 remain required.
Its [Windows evidence](experiments/analysis-mixed-project-20260924/README.md)
distinguishes runtime source **71cadfa0cd0e112caa29588d2494753301f3cb6c** from
the formatting-only aaec successor. Strict core all-target Clippy, actual listing
@@ -0,0 +1,197 @@
# Mixed typed occurrence index: successor contract
Accepted bounded implementation contract, 2026-09-24, after parent source
inspection and [independent critique](analysis-mixed-index-review-20260924.md).
This is a design decision, not an implemented or verified index. Implementation facts refer to
`aaec78fcc9b273d1485497126392afdd1fb2e54e`, not the Windows prerelease.
This continues the [complete-Project contract](analysis-mixed-project-contract-20260923.md),
especially section 7, and the [original-span composition review](analysis-original-span-review-20260923.md).
Issue 7 owns scope/status; issue 37's frozen source is unaffected.
The requested end state remains complete graphical/textual/API parity for
quantities, calculations and constraints, with preservation, checked persistence
and usable workflows. A private typed occurrence index is a dependency, not that
end state. Ordinary occurrence indexing, update composition, public source8,
structural editing, migration, UI and transport acceptance remain required.
## Current evidence and problem
- `language/analysis_source/mixed/project.rs:18` owns one admitted complete
Project, original `ParsedMixedSyntax`, warnings, static limits/usage, retained
expression/occurrence arenas and their aggregate storage ledger. Only Project
and warnings are exposed read-only. It does not provide an editing index.
- `language/analysis_source/mixed.rs:39` retains the exact borrowed SourceBundle,
caller ProjectLimits, canonical file table, full-buffer tokens, original typed
declarations and ordinary syntax positions. Numeric file keys belong to this
table; equal offsets in different files are unrelated locations.
- Existing typed-only `analysis_source/index.rs:122-243` owns names and occurrence/
expression maps but borrows a caller numeric source map. Its private builder
combines an ordinary Project with separate Lowered model maps. Feeding the
complete mixed Project into that path unchanged duplicates typed globals.
Its local map-size checks do not account for the retained mixed ledger.
- `analysis_source/update.rs` accepts the typed-only Index in its standalone
Plan and opaque Composition/OriginalEdits adapter. Those APIs do not establish
complete SourceBundle entry/path/profile authority for mixed input.
- Public `source_project.rs:93-117` exposes mutable bundle/model/index fields;
`update_bundle_with_identity_map` recompiles and compares all three before
editing (640 onward). Its ordinary collector applies edits, then runs the
structural updater, then recompiles and compares the complete intended Project
(868 onward). This later-coordinate structural pass cannot be relabeled as
original-coordinate mixed composition. That public contract is unchanged here.
## Accepted choice
Criteria are exact original ownership, complete semantic coverage within the
declared index scope, aggregate resource accounting, compatibility and avoiding
two divergent implementations of structural verification.
| Candidate | Evidence / tradeoff |
| --- | --- |
| Shared private verification/maps with distinct provenance wrappers | Reuses the existing structural-path, token, owner and call-label checks. Requires explicit source/declaration/site views and storage reservations. Preferred if the extraction remains small and typed-only behavior is preserved. |
| Separate copy of the typed index for mixed input | Simpler initial access to mixed fields, but duplicates the nontrivial syntax-edge and call-label verifier and would need every later correction twice. Reject unless extraction exposes a concrete incompatible invariant. |
| Reparse mixed fragments into the old numeric-map Index | Loses complete bundle/profile authority, repeats accounting and can lose original coordinates. Reject. No substring, masked-source or canonicalized bridge. |
Adopt the first candidate with the consumed mixed wrapper below. The critique's
two findings are resolved here: storage domains are fixed by the existing
contract, and reference completeness is distinguished from runtime expression
verification. Revisit only for a demonstrated incompatible verifier invariant
or a concrete requirement for multiple independently retained index owners.
Do not add a public generic indexing framework. Shared helpers may consume
private borrowed inputs only inside the authenticated constructors. There must
be no public or sibling-callable API that treats arbitrary Lowered sites and
caller-replaced token/location maps as an authenticated mixed index.
## Ownership and construction invariant
The proposed mixed constructor consumes `ResolvedMixedProject<'s>` and returns
an opaque `IndexedMixedProject<'s>` owning that witness plus its index maps.
Names are illustrative API identifiers. The output borrows the original bundle
through its retained witness; it contains no self-references. Its read-only
views borrow the output. Construction either succeeds completely or returns
diagnostics with no usable partial index.
Consuming the witness prevents creating multiple independently retained indexes
while charging only one to its ledger. If a borrowed-construction alternative is
chosen, it must prove reservation lifetime/release and simultaneous-index bounds;
extra reservation lease machinery is not justified without a demonstrated need.
The mixed wrapper must not dereference/convert to the old Index or implement an
adapter accepted by old `Plan::renames`, `Plan::apply` or `Composition::renames`.
Read-only access to names/locations does not grant edit authority. A later
compositor must bind the full original entry, file set, canonical paths, bytes,
limits/profile and complete target, not merely compare touched file bytes.
Build from retained full-file tokens/declarations and the existing expression/
occurrence arenas without reparsing, lowering again or duplicating Project
records. Iterate typed declarations with their canonical numeric file keys;
do not clone them into old owned Units. Derive global names exactly once from
the complete Project, including project, definitions, elements, relations,
diagrams, placements, artifacts and traces. Add calculation parameters under
`(calculation_id, parameter_id)`; a parameter UUID reused by another calculation
or a global remains distinct. Parameter spelling is calculation scoped.
Reuse existing expression/occurrence key semantics: file-qualified locations,
owner, binding field, structural child path, token role and qualified target.
Headers and all typed reference roles must be included. Ordinary targets may
appear in the catalog and typed references, but this view does not invent an
ordinary declaration/reference occurrence index. Document that distinction in
the read-only API and tests.
Verify owner containment, UTF-8 source boundaries, exact token spelling and
token classification, uniqueness of physical token ownership and qualified
keys, parent-before-child/path/depth rules, and call-target/parameter-label
agreement. Check structural edges against retained authored syntax, not only
internally consistent arena claims. Keep file ownership when reporting errors;
use an explicit invariant-error location fallback when no one file is justified.
## Live storage and failure policy
Continue the retained ledger and Budget/profile; do not initialize a fresh
permissive budget or recharge original source/token/exact-number parsing.
Reserve checked aggregate additions before allocation, combining the existing
syntax/sites/warnings baseline with new retained maps and all live scratch.
The implementation must inventory names and owned name bytes, occurrence and
expression map entries, unique persistent Path nodes, and temporary owners,
physical locations, path lookup vector, call map, global/parameter spelling
lookups, syntax-site lookup and iterative walk slots. An Arc clone shares a path
node but still occupies its enclosing map/vector slot. No copied path vectors
are needed to construct keys. If `Project::identities()` is used, account for
its temporary Vec (`model.rs:1763`); a streaming traversal avoids that allocation.
Retained lowerer occurrences and newly retained occurrence-map entries coexist.
Preserve the preceding contract's dimensions: lowerer occurrence records retain
their occurrence-slot reservations; new index map/vector/set entries and unique
Path nodes consume entry slots. Separately owned names consume text bytes.
Both representations count once in their respective domains; neither record
is charged twice merely because it is called an occurrence. Do not reset or
release the old arena's reservation while its vectors remain live. Release scratch reservations only
after the corresponding allocations are dropped. Preserve prior logical-slot
scope: this is not an allocator-capacity/RSS or raw model/validator-heap bound.
For the current three-map design let G be complete global-plus-scoped names,
H typed declaration headers, O retained lowerer occurrences, E expression sites,
and P nonroot expression sites. Added retained storage is entry slots
`G + (H + O) + E + P`, occurrence slots zero, and text bytes the sum of copied
names' UTF-8 lengths. The prior baseline still contains E raw expression entries
and O occurrence slots. One Path Step is allocated per nonroot expression; any
additional retained representation requires an explicit additional reservation.
Peak scratch additionally includes owner map H, physical-token set H+O,
arena-position/path/depth vector E, call-site map C, borrowed reverse-name maps
G, syntax-site lookup E and live iterative walk slots W. Count any allocated
file/declaration adapter table too. Drop owners/physical tokens after occurrence
validation, and paths/calls after argument-child validation before syntax-edge
work where possible; otherwise sum their overlapping reservations. A popped
work item releases one logical slot. The scalar visited count consumes no
allocated entry per visited node. Path-node reservations survive dropping the
temporary vector while retained map keys still share those nodes.
Budget errors abort construction. Existing depth checks may update deepest-frame
usage; this is not reparsing or Exact-work recharge. Warning retention and prior static admission
metadata stay unchanged. Neither indexing nor failure recovery repeats complete
model admission or constructs replacement source. Rejection and destruction must
retain the existing bounded-stack policy; no production depth128 enablement is
implied by a narrow private test.
## Required evaluators before implementation acceptance
1. Hand-enumerated OA and SA mixed bundles: entire name catalog plus every typed
declaration/reference/expression key, full-file span and spelling. Include
interleaved ordinary declarations, cross-file references in both semantic
directions, Unicode/CRLF and coincident offsets. The expected index must not
be generated by the builder, formatter or lowerer under test.
2. Reuse the complete-Project repeated/reordered-call fixture with shared
parameter UUIDs in distinct calculations; compare all qualified labels and
structural paths, including repeated identical expression text.
3. Internal corruption controls: swapped file ownership, wrong owner/field,
parent cycle/forward edge, structurally wrong but internally consistent child,
duplicate physical token, missing/extra expression, duplicate occurrence,
wrong call label/target, missing required argument label, and wrong token
classification/spelling. Every control must reach its intended existing
structural/token check rather than an unrelated earlier parse refusal.
Complete reference occurrence emission remains an invariant of the sealed
lowerer, tested by the independent exhaustive oracles in items 1 and 2.
The existing syntax-edge checker verifies the expression arena; it does not
prove all parameter-declaration or non-expression type-reference occurrences
are present. Do not claim arbitrary omitted occurrences are runtime-rejected
or introduce an unreviewed duplicate full syntax-reference verifier.
4. Hand-counted live-storage cap and cap-minus-one cases: retained baseline plus
names/paths/maps, peak overlapping scratch, copied-name bytes, and simultaneous
occurrence representations. Check unchanged parse/numeric counters and exact
intended refusal phase; no success by clearing the baseline.
5. Read-only provenance and lifecycle: exact entry/path/file/byte retention,
unchanged whole Project/warnings/admission metadata, no old-updater-compatible
conversion, and no usable failed result. Exercise complete success/drop and
representative late rejection/drop on the existing small-stack harness.
6. Existing typed-only index/update/export tests and full inherited compatibility
dispositions must remain accounted for after shared-helper extraction.
Strict core Clippy and current-source checks remain required. Private full
library source8 failures are not to be suppressed or called passed.
After this dependency, integrate real ordinary and typed original-coordinate
edit producers, combined preflight/emission, output recompile/admission and
whole intended-Project equality. Extend to structural edits, identity changes,
missing-ID stabilization and checked-save/history before claiming the required
editing parity. This proposal does not authorize a smaller final product.
@@ -0,0 +1,61 @@
# Mixed typed-index seam: independent source/design critic
2026-09-24. Source-only review of clean private source `aaec78fcc9b273d1485497126392afdd1fb2e54e`; source paths below are relative to `crates/oa-core/src/`. Read root mixed-Project contract section 7, original-span proposal and accepted review, and parent's draft `harness/analysis-mixed-index-contract-20260924.md`. The reviewer performed no compiler, source/build/Gitea mutation, or runtime check. Parent subsequently verified and resolved the findings and adopted the revised [contract](analysis-mixed-index-contract-20260924.md). Initial findings and final disposition are preserved below. Prerelease #37 is unaffected.
## Assessment and two precise draft refinements
The consumed wrapper plus shared private verifier is the smallest sound next slice. It preserves original complete-bundle authority without claiming an ordinary occurrence index or enabling editing. Separate mixed verifier duplication offers no demonstrated benefit over narrow borrowed-input extraction. Parent's draft is implementable after settling these two points explicitly:
1. **Set accounting dimensions in the contract, not during implementation.** Existing mixed-Project contract section 3 assigns map/vector/work entries and expression sites to entry slots; occurrence slots cover lowerer occurrence records. Consequently every new index-map entry, including an occurrence-map entry, charges `entry_slots`; retained `lower::Occurrence` records keep their existing `occurrence_slots`. Owned copied names charge text bytes separately. Parent draft lines 115–119 currently leave this choice open. Applying the old `Index::insert` local `lowering_occurrences(map.len())` check would not satisfy that inherited aggregate policy (`analysis_source/index.rs:643`).
2. **Separate runtime damage checks from completeness by sealed origin.** Parent draft lines 138–144 list missing/extra occurrences among corruption controls. The existing verifier does not independently enumerate all expected syntax references: its own module header states that occurrence completeness trusts the lowerer (`index.rs:1–5`). `check_syntax_edges` only traverses expression structure (`:478–632`). Deleting an isolated parameter-declaration occurrence or a non-expression type reference can leave all runtime checks satisfied. Do not promise arbitrary omission rejection without adding a separate reviewed reference-syntax verifier. For this minimal slice, retain sealed parse/lower completeness, use hand-enumerated full occurrence output as the independent oracle, and restrict mandatory runtime omission rejection to checks actually present (missing expression, missing call label for an existing argument child). This is not a reason to widen scope or expose fabrication APIs.
## Concrete ownership/API candidate
A private constructor consumes `ResolvedMixedProject<'s>` and returns `IndexedMixedProject<'s> { resolved, data }`. `resolved` owns the unchanged accepted Project, syntax, warnings, admission metadata, raw sites and Ledger (`mixed/project.rs:16–32`, `:535–543`). `data` owns names and the typed expression/occurrence maps. Read-only methods return views borrowing the wrapper; a view may expose canonical file/path/source lookup and qualified keys, but no mutable fields, raw-site constructor or old `Index` conversion. No extra lifetime is needed for self-references because `data` owns its copied name Strings and keys rather than borrowing fields of `resolved`.
During construction, narrowly split borrows of retained immutable syntax/project/sites, mutable Budget (for the existing depth check), and mutable Ledger. These borrows exist only inside the builder and end before returning the owner. The retained `SourceBundle` borrow outlives the wrapper and prevents safe mutation while it is live; identical lifetimes alone are not provenance, so neither source nor file table is a separately supplied parameter. Keep the constructor in the witness's module boundary or expose only a constructor-authenticated private view to the shared verifier.
Do not reconstruct `BTreeMap<usize, String>` from mixed files. `ParsedMixedSyntax.files` already fixes canonical ordering, original source strings and tokens (`mixed.rs:36–58`, `:370–376`). A borrowed file lookup can return `(original_source, token_slice)` for either existing typed-only inputs or the mixed file table. Typed declaration iteration should yield `(file_key, &Declaration)` over retained vectors; site inputs are borrowed expression/occurrence slices. Avoid allocating cloned `Unit` declarations, relexing, rebuilding Lowered model maps, rerunning admission or generating replacement source.
The old nominal `Index<'s>` remains the only input to `Plan` and `Composition` (`update.rs:15–27`, `:238–245`). A shared private `IndexData`/verification implementation does not justify a generic update trait, `Deref<Index>`, `AsRef<Index>`, or a public adapter. Keep the old `sources: &BTreeMap<usize, String>` authority in its wrapper (`index.rs:122–128`) and preserve typed-only checks/semantics. Mixed-only aggregate reservations must not be accidentally imposed on legacy tests via an unreviewed policy change.
## Reuse boundary and scope
Reuse structural key/path semantics (`index.rs:15–120`), owner/physical-token checks (`:246–283`, `:635–675`), expression-parent/path construction (`:288–359`), qualified roles and call-label checks (`:360–472`), and original-syntax expression-edge verification (`:478–632`). Extract these algorithms with small private input/storage adapters, rather than introduce a public generic indexing framework.
Replace the current name-construction assumption only for mixed input. It currently enumerates ordinary identities and then separate Lowered definitions/elements (`index.rs:209–241`); mixed resolution already moved those models into the complete Project (`mixed/project.rs:439–459`). Iterate every complete Project global once, then scoped parameters once. Global categories include Project, definitions, elements, relations, diagrams and placements, artifacts, and traces (`model.rs:1763–1783`). A streaming borrowed walk avoids `Project::identities()`'s temporary Vec; otherwise reserve that Vec before calling it. Names include ordinary globals for resolution/namespace purposes, but indexed declarations/references remain typed-owned. Ordinary references to typed targets are preserved in syntax/model but not supplied by this view.
A separate mixed-index implementation would duplicate roughly the whole path/call/syntax-edge verifier and its damage tests; later fixes could diverge. Reconsider only if extraction exposes an actual incompatible invariant, rather than because mixed fields require private access. The distinct wrappers already express the genuine provenance difference.
## Aggregate storage inventory and release points
Continue `Ledger::reserve`'s checked totals and inherited Budget (`mixed/project/accounting.rs:43–70`), including retained syntax, warnings, expression sites and occurrences. Never start from zero. One consumed owner prevents repeated retained indexes using one accounting baseline.
For a successful simple implementation let G be complete global-plus-scoped name count, H typed headers, O retained lower occurrences, E expression sites, P nonroot expression sites, and C calls. The added retained logical storage is **entry slots = G + (H + O) + E + P; occurrence slots = 0; owned text = sum of the copied names' UTF-8 lengths**. The existing baseline already contains E raw-site entry slots and O raw-occurrence slots. P counts each allocated shared Path Step once; Arc clones do not allocate another Step but their map/vector records still count. This formula assumes exactly the current three maps and one Step per nonroot expression; any added representation must be listed separately.
Scratch must additionally reserve before growth:
- typed owner map H; physical-token set H + O;
- arena-position/path/depth vector E; call-site map C;
- borrowed reverse-name maps G; syntax-site lookup E; iterative syntax work slots W;
- any allocated file/declaration view table, error mapping retained in success, or identity-visitor scratch.
Borrowed reverse-name strings cost no new text bytes. Work-pop releases its logical slot; this remains a logical live-element policy, not retained Vec capacity/RSS metering. Scalars such as `visited` are not a separately allocated entry per visited expression.
Explicitly drop/release owners and physical-set storage after occurrence validation, then paths/calls after argument-child validation and before syntax-edge work where possible. Otherwise all remain live and must be summed at that peak. Retained Path Steps remain charged even after dropping the temporary path vector, because expression/occurrence maps share them. Failure drops the entire consumed owner; no partial reusable success or stale reservation lease escapes. Preserve iterative Path destruction (`index.rs:68–79`). `Path::edges` allocates a Vec (`:82–90`) and currently has test-only call sites; do not turn it into a new unmetered production materialization API.
## Discriminating acceptance cases
1. Independently enumerate complete names and all typed key/location/spelling tuples in OA and SA mixed files with Unicode/CRLF, ordinary prefixes and coincident offsets across canonical paths. Compare every tuple and original whole bundle, Project, warnings and admission metadata; do not generate expectations by the builder/lowerer. Include a parameter UUID equal to a global and reused in two calculations.
2. Reordered repeated calls must retain distinct parent paths, correct callee-scoped labels and original argument order. Corrupt a label to an existing other callee with the same parameter UUID/spelling so token/catalog checks cannot mask the intended call-site rejection (`index.rs:426–469`).
3. Runtime negatives: missing/extra expression; forward/cyclic parent; cross-file/owner/field location; internally consistent but syntax-wrong child edge; duplicate physical token or qualified occurrence; non-Word/partial/UTF-8-split token; missing call label with an argument child. Record which exact check rejects. For arbitrary reference omission, the full authored oracle must fail; do not label this builder rejection unless new syntax completeness logic exists.
4. Hand-count a retained baseline plus the formula above and peak scratch: exact cap succeeds, cap minus one fails at the intended reservation before growth. Separate copied-name-byte pressure and overlapping temporary maps. A case where old baseline and new maps each fit alone but their sum does not catches ledger reset; retain both raw and indexed representations throughout. No parse byte/token/entry/reference or Exact-work recharge is permitted; inspect control flow as well as counters. The existing `Budget::frame` may update deepest-frame usage while checking depth (`budget.rs:118–121`); this is not another parse.
5. Type/API inspection must establish no old-updater-compatible conversion and no replaceable bundle/table/profile inputs; wrong-session composition is a later compositor negative, not an invented runtime API in this read-only slice. Test original provenance through views and success/late-failure cleanup on the existing small-stack harness. Re-run legacy Index/update/export oracles after extraction.
## Dependencies deliberately still open
This slice neither authenticates a complete ordinary occurrence set nor authorizes rename emission. Subsequent work must derive both edit producers and complete rename intent from the same witness/target; define the precise supported ordinary diff/compound-edit normalization; aggregate and validate original-coordinate edits; emit once; recompile/admit the actual complete result; compare the whole independently intended Project; and preserve atomic history/save behavior. Full parity still requires typed subtree and parameter edits, repaired deletion/reidentity, file movement/ownership, missing-ID stabilization/reindexing, migration/public dispatch, and editor/root reconciliation. These remain delivery requirements, not reasons to expand this next read-only dependency.
## Revised parent draft disposition
Re-read the updated contract's live-storage and evaluator clauses after parent revision. Both requested refinements are now explicit: new map/vector/set/Path storage uses entry slots while retained lower occurrences keep occurrence slots, and runtime expression/token/call checks are separated from complete occurrence emission guaranteed by sealed lowering and independently enumerated output tests. Those changes resolve the two design ambiguities identified above. No remaining blocking source/design finding for this bounded implementation proposal. The concrete retained-storage formula and failure cases in this report are implementation guidance, not measured results or a final accepted decision. Parent retains adoption and gate authority.