152 lines
9.7 KiB
Markdown
152 lines
9.7 KiB
Markdown
# Private actual-output rename acceptance
|
|
|
|
Baseline `29417130c71f70c4eaefe8ed4c879efba78eb72c`. Select the complete pending
|
|
owner borrow, actual-output equality bound and moved model/warning outcome after
|
|
independent design, domain and ownership critiques. This connects the verified
|
|
emitter and named parser producers; it is no longer another fixture-only
|
|
continuation. The surrounding mixed implementation remains private experimental
|
|
source. Public source8, installation/history and release integration are separate.
|
|
|
|
## Authority and result
|
|
|
|
Add a consuming verification operation on opaque PendingRename. Its only normal
|
|
constructor remains validated consumed emission. No production constructor may
|
|
accept an arbitrary bundle/model/Slots/profile tuple. Add CarriedInput::from_pending
|
|
accepting a shared reference to that complete pending owner; derive bundle,
|
|
exact Limits/ProjectLimits and retained O from the same owner. Both backing and
|
|
guard retain a complete pending reference, not just numeric counters. Keep enum
|
|
variants private and expose only narrow immutable pending views to carried code.
|
|
|
|
Prefer `&'s PendingRename<'s>` inside the existing single-lifetime backing, using
|
|
the immutable desired reference's covariance to shorten a longer desired borrow
|
|
to the verification borrow. Actual Rust compilation must establish that relation.
|
|
Do not thread a second lifetime through every parser owner, duplicate full policy
|
|
inside guards, introduce a heap wrapper or permit mutation while the guard lives.
|
|
The existing fixture constructors and old parser entry points keep their behavior.
|
|
The new continuation is the sole emitter-connected entry into the combined text
|
|
and retained-entry producer route, including actual zero metadata if applicable.
|
|
|
|
On success return a non-self-referential owning AcceptedRename with the actual
|
|
SourceBundle, actual resolved Project, mapped warnings, exact inherited policies
|
|
and final retained Slots. Preserve scalar verification Usage and numeric work
|
|
separately from original-snapshot work; no cumulative reinterpretation. The
|
|
accepted type has private fields and read-only accessors, with no unchecked or
|
|
mutable constructor, borrowed syntax or borrowed desired model. Source, desired
|
|
and pending may be dropped before the accepted result is inspected.
|
|
|
|
This result does not itself save files, edit history, install a model or enable
|
|
repeated carried-source emission. Later adoption must jointly preserve its
|
|
graph/source/diagnostic relationship; no separate mutable extraction is added.
|
|
No-op remains the existing explicit unchanged-owner branch.
|
|
|
|
## Actual verification and equality
|
|
|
|
Parse the actual complete pending bundle under its exact policy using both named
|
|
producer modes. Propagate its located parse diagnostics. Consume the resulting
|
|
syntax through the existing resolver and complete model admission, preserving O
|
|
through all parser/resolver stages. Never default policy, substitute intended
|
|
tokens/model, drop untouched files, re-emit bytes for comparison or reset carry.
|
|
|
|
After actual model admission reserve `E_actual = resolved.expressions.len()`
|
|
entry slots against that resolved owner's full live ledger, which includes O,
|
|
syntax and mapped warnings. Compare the entire actual Project with desired using
|
|
its established PartialEq, including aliases, parameter names, all maps and
|
|
historical payloads. Do not use rename::same_project, which exempts names. Release
|
|
the equality frontier after comparison. A mismatch returns a small static
|
|
invalid_source diagnostic at entry/default span0..0, not a formatted model.
|
|
|
|
The independently reviewed bound follows every reachable actual Expr root:
|
|
calculation body, property base, case overrides and check predicate. Each actual
|
|
node has a source expression-site entry. Iterative Expr equality's live pairs
|
|
correspond to distinct nodes of its actual left operand; list/call shape checks
|
|
precede child queueing, and no nested equality frontier remains live. Whole-model
|
|
comparisons visit roots sequentially. E_actual0 cannot invoke an allocating Expr
|
|
comparison from a nonexistent actual root. Existing signed-zero PartialEq remains
|
|
semantic equality, not bitwise equality. Revisit the proof when payload types or
|
|
lowering/equality implementations change. Original pending E is provenance only;
|
|
the new implementation must use the current resolved arena for its reservation.
|
|
|
|
## Mapped warnings and ownership transfer
|
|
|
|
Retain the mapped warnings by moving them, together with the actual resolved
|
|
Project, after successful equality. The model remains in its existing excluded
|
|
model-allocation domain and has already passed admission. Mapped warnings remain
|
|
in the selected auxiliary domain. Do not clone a model, warning, path or vector.
|
|
|
|
Compute warning inventory W with a checked borrowed loop over the actual records:
|
|
one entry per warning, zero occurrences, and UTF-8 lengths of path, code, optional
|
|
field and message. Require current mapper invariants: every related vector empty
|
|
and no Error severity. Unexpected shapes fail before producing accepted authority;
|
|
do not silently ignore newly introduced fields/related locations. The diagnostic
|
|
field accounting should be exhaustive enough that schema changes demand review.
|
|
|
|
W already participates in the full resolver ledger. Do not charge it twice during
|
|
equality or transfer. Compute final O+W with checked arithmetic, verify it is a
|
|
componentwise subset of the still-live ledger, and check its exact inherited
|
|
ceilings while Budget exists. This is a destination-inventory check, not an early
|
|
release: keep full coexistence accounting until all temporary owners actually
|
|
drop. Move Project/warnings to locals, drop all verification syntax/guard,
|
|
expression/occurrence/catalog owners, then move the pending bundle/policy into
|
|
AcceptedRename. Rust must enforce that no pending borrow survives that move.
|
|
Final retained counts exclude released syntax and equality scratch but include
|
|
all surviving mapped warnings. Failure returns only diagnostics and destroys
|
|
the consumed pending output and partial verification state.
|
|
|
|
## Explicit remaining scratch decision
|
|
|
|
Choose the existing logical retained domain plus the named decode/equality
|
|
temporaries; do not expand it into universal parser/all-heap accounting. Existing
|
|
traversal, delimiter, ordinary-open, Pratt and duplicate-name scratch retain their
|
|
independent file/edge/token/grammar controls and are excluded from carried W.
|
|
Significant-token storage retains its independent token ceiling; M counts the
|
|
separate token-end representation once. No new output-verification collection
|
|
may be hidden under an old exclusion.
|
|
|
|
File count/source-text limits do not tightly bound copied traversal path bytes.
|
|
Path folding/canonicalization and include target/location copies can occur before
|
|
edge refusal; retain that known limitation explicitly. Open-declaration depth is
|
|
bounded by declaration events, not typed-value depth. Pratt frames are not native
|
|
stack bytes. Decoder/numeric internals, raw model/validator allocation, allocator
|
|
capacity/overhead and native stack remain their established separate domains.
|
|
Do not claim aggregate admission before every allocation or process-memory bounds.
|
|
This resolves the earlier scratch-domain choice without waiving selected retained
|
|
producer timing, actual output admission, equality or returned ownership.
|
|
|
|
## Finite acceptance
|
|
|
|
Use unchanged inherited profiles from original parse/index/plan through emission
|
|
and verification. Never tighten an admitted owner to manufacture a late failure.
|
|
Minimal project p→next emits81 bytes, O=(1,0,105), T11. Entries17 and bytes152
|
|
admit the full pipeline; bytes151 reaches output UUID decode at37..38, line2
|
|
column27, after scanner peak141 and emission peak114. Entry16 fails emission
|
|
first and is not a later verifier cap. Assert the entire independent expected
|
|
Project/bundle, empty warnings, final O, exact policy and separate snapshot Usage.
|
|
|
|
Retain a real warning-bearing rename with an independently authored full
|
|
diagnostic and exact final O+W. Distinguish final retention counts from greater
|
|
earlier peaks; do not invent a final-only cap-minus-one boundary. Reuse emitter
|
|
OA/SA/cross-file/Unicode/CRLF/swap byte oracles and whole expected models where
|
|
valid, checking returned warning paths/spans against the actual returned bytes.
|
|
The [empty-name warning oracle](analysis-mixed-acceptance-design-20260925/WARNING-ORACLE.md)
|
|
uses unchanged entries18 and bytes161/160: old emission peaks159 bytes, actual
|
|
output warning mapping161, and accepted O+W=(2 entries,0 occurrences,157 text).
|
|
Its negative warning-map diagnostic retains the full project-header11..69 span,
|
|
unlike the parser's one-byte token-start transport. These are expectations to
|
|
verify, not results inferred from source arithmetic.
|
|
|
|
Equal-byte test-only corruption can cover wrong-but-admissible alias/name,
|
|
malformed source and model-invalid output while preserving O. A length-changing
|
|
corruption must first be rejected by an explicitly selected inventory check or
|
|
use independently verified actual-O fixture provenance, never stale counts.
|
|
Include greater actual expression count than old E, wide/deep comparison,
|
|
target-only mismatch and signed-zero cases. Label internal inventory/shape faults
|
|
as such; do not relabel them as authentic emitted histories. Check true owning
|
|
lifetime by returning success out of a scope that drops original input/desired.
|
|
|
|
Preserve all previous tests, failure bodies and format disposition; run focused
|
|
new cases, full core library, strict all-target Clippy and format comparison.
|
|
Exercise meaningful scoped128KiB verify/drop cases with prerequisites prepared
|
|
outside the worker, preserve all old stack controls and inspect changed
|
|
prologues. Do not enlarge stacks, loosen policies or rerun failures until lucky.
|
|
Older separately unrerun full-pipeline setup limitations remain distinct.
|