Pin independent emission byte and storage oracles
This commit is contained in:
@@ -0,0 +1,133 @@
|
||||
# Proposed independent emission-transition oracle
|
||||
|
||||
2026-09-25. **Design proposal and source-derived expectations, not runtime results or accepted output.** Source: `fa7a980418ef99d772e67c66c28dfa7b5181f875`. Reviewed initial `EMISSION-TRANSITION-PROPOSAL.md` SHA256 `c0734464991ab841ae59d6c3c26a5095b3c0908ce35656158db92476d76682de`; parent subsequently selected changed-source legacy-only guard admission. No application parser, emitter, Cargo or executable was run. UTF-8 lengths below are literal byte arithmetic, not values obtained from implementation output.
|
||||
|
||||
Use A for the admitted authored source ledger, L for the plan's ledger **already including R+M**, and O for newly owned output. Emission must reserve L+O, not L+(R+M)+O. All examples below start through the legacy source path, so no external carried baseline is concealed in A.
|
||||
|
||||
## Minimal exact predecessor and emission caps
|
||||
|
||||
E is the existing `project::tests::single("")` literal, entry/key `main.arcadia` (12 UTF-8 bytes each):
|
||||
|
||||
```text
|
||||
arcadia 8;\nproject p "Project" id "00000000-0000-0000-0000-000000000001" {\n\n}\n
|
||||
```
|
||||
|
||||
This notation represents actual LF bytes. Original source length78, syntax U1/M11, retained syntax text8; no expressions, references, lower occurrences or warnings. These grammar/accounting terms also appear in the independent carried-phase oracle. Desired changes only the project alias from `p` to `next`. Exactly one physical token changes: canonical file0, range19..20. Independently authored complete expected source is:
|
||||
|
||||
```text
|
||||
arcadia 8;\nproject next "Project" id "00000000-0000-0000-0000-000000000001" {\n\n}\n
|
||||
```
|
||||
|
||||
Expected source length81. The extra entry-path string is separate from the equal-spelled file key. Thus O=(1,0,81+12+12)=(1,0,105).
|
||||
|
||||
| E phase | Retained entries/text after phase | Maximum entries/text within phase |
|
||||
| --- | --- | --- |
|
||||
| Resolve | 12 / 8 | 16 / 10 |
|
||||
| Typed index (one global project name, no typed sites) | 13 / 9 | 14 / 9 |
|
||||
| Ordinary index (one project header) | A=14 / 9 | 15 / 9 |
|
||||
| Rename E0, Q1, R1, M1 | L=16 / 9 | 16 / 9 |
|
||||
| Output reservation | L+O=17 / 114 | 17 / 114 |
|
||||
| Pending after old source/maps drop | O=1 / 105 | — |
|
||||
|
||||
All occurrence counts are zero. Phase maxima are coordinatewise logical maxima, not allocator/RSS measurements. The complete real path must fit at **entries17 / bytes114**. Entries16 with bytes114, or bytes113 with entries17, clears all predecessors and independently refuses the upfront emission reservation. Source-byte work78, planned output81 and changed-name-byte check4 all fit either byte cap. No live Budget mutation is needed to manufacture these pairs.
|
||||
|
||||
Source derivation: `mixed/project/accounting.rs:233–352` charges U+M and syntax text; `mixed/project.rs:273–314` project catalog adds four temporary entries and two alias bytes, later released. `index.rs:288–298` retains one name entry/byte and `:684–709` temporarily reserves the one global lookup. `ordinary_index.rs:98–108,123–153,251–263` retains the single ordinary header while releasing one reverse-global scratch entry. `rename.rs:14–28,30–91,106–120` gives E0 and max(R+Q,R+M)=2; no new copied text is retained by the plan.
|
||||
|
||||
H is the exact three-file Unicode/CRLF chain from `CARRIED-PHASE-ORACLE.md`: main101B includes part25B, which includes last6B (`//é\r\n`); entry `main.arcadia`; all three keys total36B, entry12B. Only change project p→next, again main range19..20; canonical file order last/main/part makes that file1. Main becomes104B; part and last remain byte-exact. Original U3/M19 and syntax text32 give:
|
||||
|
||||
| H quantity | Entries | Occurrences | Text |
|
||||
| --- | ---: | ---: | ---: |
|
||||
| Resolved retained | 22 | 0 | 32 |
|
||||
| Authored A (one name plus project header) | 24 | 0 | 33 |
|
||||
| Planned L, R1/M1 | 26 | 0 | 33 |
|
||||
| Output O, S135 + keys36 + entry12 | 3 | 0 | 183 |
|
||||
| Emission overlap L+O | 29 | 0 | 216 |
|
||||
|
||||
Resolver maximum26entries/34text; typed-index maximum24entries/33text; ordinary-index maximum25entries/33text; planning maximum26entries/33text. Thus **29 / 216** fits the entire path and **28 / 216**, **29 / 215** independently fail only at emission overlap. This distinguishes accounting for all untouched files and copied path/entry strings from source-size-only checks.
|
||||
|
||||
## Unchanged branch and guard boundary
|
||||
|
||||
E no-op fits the original pipeline at entries16/bytes78; H at entries26/bytes132. An unnecessary output copy would exceed those byte ceilings (E A.text+102=111; H A.text+180=213). A successful unchanged branch at these actual inherited caps therefore discriminates against reserving/copying identical output. It must return the original authored owner with unchanged ledger, Usage/numeric work, warnings, Project, maps and exact original bundle borrow. Signed-zero-equivalent target intent is also unchanged bytes; no new semantic rewrite is authorized.
|
||||
|
||||
Freshness is checked even on unchanged intent: mutate an untouched comment byte, entry, key or file set in an independent current snapshot and require refusal before branch return. An independently allocated but equal complete current bundle is acceptable; emission authority still belongs to the retained original, not that comparison input.
|
||||
|
||||
**Required selected edge test:** produce an authored source via carried parsing, both borrowed-zero Some guard and actual retained nonzero guard, then plan a changed alias. Changed emission must refuse before O reservation for either Some guard. No-op must preserve and return that original guarded owner. Dropping a borrowing guard does not drop its external RetainedSnapshot; carrying only O after such a changed source would hide still-live counted ownership. The narrow legacy-None restriction avoids that false transition without inventing an emitter/verification ownership architecture. A zero numeric C is not sufficient to bypass the selected guard restriction.
|
||||
|
||||
## Independent four-file mixed swap bytes
|
||||
|
||||
This proposed fixture combines a typed/ordinary global swap with cross-family references, a leading multibyte character, CRLF, comments containing alias spellings and an untouched included file. Every line below ends CRLF, including the last line of each file. UUID strings are literal. Entry is `main.arcadia`; canonical order is a/b/main/untouched.
|
||||
|
||||
Original `a.arcadia`:
|
||||
|
||||
```text
|
||||
calculation f "F" id "00000000-0000-0000-0000-000000000010" { result Number; body 1; }
|
||||
```
|
||||
|
||||
Original `b.arcadia`:
|
||||
|
||||
```text
|
||||
// f and w are comments
|
||||
oa_activity w "Work" id "00000000-0000-0000-0000-000000000002" {}
|
||||
```
|
||||
|
||||
Original `main.arcadia`:
|
||||
|
||||
```text
|
||||
// 雨
|
||||
arcadia 8;
|
||||
project p "Project" id "00000000-0000-0000-0000-000000000001" {
|
||||
include "a.arcadia"; include "b.arcadia"; include "untouched.arcadia";
|
||||
oa_property v "Value" id "00000000-0000-0000-0000-000000000003" { subject @w; type Number; base @f(); }
|
||||
}
|
||||
```
|
||||
|
||||
Original and expected `untouched.arcadia`:
|
||||
|
||||
```text
|
||||
// 雪 untouched f w
|
||||
```
|
||||
|
||||
Desired changes exactly calculation10 alias f→w and activity2 alias w→f; every other Project field remains original. Independently authored expected `a.arcadia`:
|
||||
|
||||
```text
|
||||
calculation w "F" id "00000000-0000-0000-0000-000000000010" { result Number; body 1; }
|
||||
```
|
||||
|
||||
Expected `b.arcadia`:
|
||||
|
||||
```text
|
||||
// f and w are comments
|
||||
oa_activity f "Work" id "00000000-0000-0000-0000-000000000002" {}
|
||||
```
|
||||
|
||||
Expected `main.arcadia`:
|
||||
|
||||
```text
|
||||
// 雨
|
||||
arcadia 8;
|
||||
project p "Project" id "00000000-0000-0000-0000-000000000001" {
|
||||
include "a.arcadia"; include "b.arcadia"; include "untouched.arcadia";
|
||||
oa_property v "Value" id "00000000-0000-0000-0000-000000000003" { subject @f; type Number; base @w(); }
|
||||
}
|
||||
```
|
||||
|
||||
Exact original-coordinate edit oracle:
|
||||
|
||||
| Canonical file | Range | Old | New | Target |
|
||||
| --- | --- | --- | --- | --- |
|
||||
| 0, a.arcadia | 12..13 | f | w | calculation10 |
|
||||
| 1, b.arcadia | 37..38 | w | f | activity2 |
|
||||
| 2, main.arcadia | 232..233 | w | f | activity2 |
|
||||
| 2, main.arcadia | 254..255 | f | w | calculation10 |
|
||||
|
||||
File byte lengths are88,92,265,22, unchanged by the swap; S467, key bytes47, entry12. Therefore **O=(4,0,526)**, R2/M4. The original raw-expression count E is2 (calculation literal and property call). Preserve this scalar in pending, but do not call it an already-proven bound for future equality over arbitrary reparsed output; that successor must establish the compared side/shape bound explicitly. The cap proof for this richer fixture is intentionally not invented: use generous inherited limits and the independent E/H cap pairs above. Fixture syntax/admission still requires a real gate; these bytes do not report an unrun parser success.
|
||||
|
||||
This exact output catches sequential spelling substitution (f→w followed by w→f), alias replacement in comments/display names, loss of markers, accidental newline conversion and omission of untouched content. Add the existing independently authored rich OA/SA full maps for scoped parameter swaps/reordered labels and the category fixture for comment-separated references/historical UUID preservation. Do not generate expected output by running the implementation's sizing/emission helper or copying its returned map.
|
||||
|
||||
## Outcome shape and remaining evaluator requirements
|
||||
|
||||
The proposed owning enum is understandable but contains the large unchanged authored owner; smaller pending payload does not make that union small. Box/Rc/Arc would introduce allocation and accounting concerns rather than demonstrate a free repair. Source-only analysis cannot guarantee debug-frame behavior, particularly after the prior inline-policy regression.
|
||||
|
||||
Parent selected **two consuming, branch-checked methods**: `into_unchanged(self,current) -> Result<AuthoredMixedProject<'s>,Failure>` and `emit_changed_unverified(self,current) -> Result<PendingRename<'t>,Failure>`. Existing `changed_names().is_empty()` supports caller selection; both methods independently validate freshness and enforce the selected branch. Wrong-branch use refuses with no partial output. This avoids a new large owning enum, generic callbacks, extra owner allocation and lint suppression; pending has no original-source lifetime and unchanged has no desired lifetime. Tradeoff: two explicit private entry points. Scoped callbacks were considered as an alternative if one dispatch method were essential, but add generic callback layering. The selected split still requires stack verification and does not warrant weakening the old 128 KiB tests.
|
||||
|
||||
Before implementation acceptance require: complete expected maps, exact source/key/entry count and O retention; E/H predecessor-clearing caps; stale/no-op and Some-guard controls; immutable desired/old bundles; policy equality across all captured fields; no parse/Exact work during emission; no pending partial result on checked failure; and an observable source/map drop before pending escapes. A helper returning Pending from a scope holding the original bundle should prove pending does not borrow old source after the changed transition. After extracting unchanged, desired need not remain borrowed. Keep all legacy stack controls unchanged and add success/no-op/refusal/drop coverage for the chosen new outcome shape. No production pending extraction/adoption, parser entry, final whole-model equality or accepted-output claim is part of this oracle.
|
||||
Reference in New Issue
Block a user