Define bounded mixed source CLI validation contract

This commit is contained in:
2026-09-24 21:47:40 -07:00
parent d4d50f061b
commit f810fb40eb
3 changed files with 333 additions and 0 deletions
@@ -0,0 +1,121 @@
# Mixed source8 command-line checking
Selected next outcome in the already-owned textual-language scope: an engineer
can run `arcadia check-mixed ROOT [--json]` on an explicit entry file and receive
located results for its complete included mixed model, without changing files.
Baseline source is public-read checkpoint bab6f96a. This contract is local-only
while Gitea writes/publication remain unavailable. The published preview is frozen.
## User-visible behavior
Keep existing check/lint/stabilize/rename behavior and the ordinary library
`prepare` contract. Add one explicit check-mixed spelling, rejecting --write,
unknown/repeated options and invalid argument counts. Route it separately from
editable preparation; do not construct a fake Prepared or SourceIndex. Use a
closed command-dispatch enum rather than an ambiguous combination of mode flags.
The existing Report envelope remains version1. Operation is check-mixed; success
is checked/exit0, with advisory warnings permitted. Changes is empty, written is
false, migration is null, identities_to_stabilize is zero. All locations refer to
captured original input. Missing explicit UUIDs, unsupported versions, malformed
syntax and semantic invalidity are errors, not implicit stabilization or migration.
Retain actual warning order and authored object identities from the admitted model.
Use the existing exit conventions: source/semantic rejection1, arguments2,
disk/path/journal/output failure3. Match existing treatment of loader diagnostics
and disk error variants, including its source-limit distinctions; document/test
the actual relevant precedence instead of assuming every limit uses one phase.
Human output/help must explain the explicit-ID schema8 read-only contract and
make the check result clear without implying proposed edits.
## Source discovery and ownership
Add `source_files::load_mixed_source(entry, limits)` returning an opaque
MixedSourceSnapshot with immutable bundle() and diagnostics() views. It captures
original bytes only. It confers no save authority, editable compilation, recovery
or promise of an atomic snapshot against another process. A caller must handle
discovery diagnostics before treating the bundle as complete. CLI owns this
snapshot, invokes check_mixed_bundle on its borrowed bundle only after discovery
succeeds, and copies diagnostics into the owned report before dropping the result.
Reuse the existing private disk discovery loop and path/read/physical-alias/journal
checks through a closed ordinary/mixed selector. The ordinary route remains
unchanged, including overlays, detached buffers, expectations and final compilation.
The new fresh mixed route has no overlays and skips ordinary compile_bundle.
Consume its private DiskProject storage into bundle/diagnostics and discard unused
expectations/root/reachability after the checks; avoid cloning reachable_bundle or
exporting DiskProject as mixed save authority.
Before disk reads, clamp the mixed source-byte allowance to min(caller,64MiB),
matching the parser's hard ceiling; preserve all other caller restrictions.
Keep canonical root-relative paths, UTF-8, regular-file/link rules, case and
physical-alias detection, aggregate files/bytes/edges/depth and pending journals.
Pending transactions remain an error and are never recovered implicitly.
Resolve includes with the existing resolver. Parse each successfully loaded path
once in existing deterministic traversal order; count repeated authored edges.
Complete semantic checking still detects cycles and cross-file errors.
Inspect includes by the real shared mixed Parser::unit grammar, including typed
declarations, explicit IDs and long-form refusals. Centralize the minimal parser
setup/operation needed by discovery and complete parsing; preserve the latter's
grammar, producer hooks, policy, retained witnesses and stack behavior. No regex
scanner, second grammar or complete-checker call on partial bundles is permitted.
Return no partial include list after a unit syntax failure.
## Bounded discovery phase
Choose one shared discovery Budget and ModelCounts for the entire discovery pass,
derived by the existing mixed source profile. Enable existing text and entry
producer checks once with zero initial reservation. Byte/token/reference/numeric
work and syntax/model counts accumulate across files; do not restart allowances
per file. Charge each inspected file before lexing/parsing and keep the existing
prospective syntax/value/owner producer checks. Tokens keep their existing
pre-scan bound; disk/path/traversal tables retain their separate filesystem limits.
Do not allocate edit positions or a resolved/indexed model merely for discovery.
Completed unit syntax is dropped after moving its include information. Its
remaining producer charges deliberately remain reserved until this phase ends:
these counters are a conservative cumulative admission bound, not a claim of
exact live storage or a verifier-owned carry. Ordinary in-parser temporary and
UUID/key releases remain unchanged. No unit-drop refund mechanism or new generic
allocation framework is needed. Shared grammar and once-per-path order consume
the same syntax/work events as full parsing, with fewer later projections; tests
must discriminate cumulative accounting from accidental per-file resets.
A syntax/budget failure is terminal for mixed parsing: record its original located
diagnostic, do not reuse a poisoned span-only Budget for another file, and do not
invoke final model checking on incomplete discovery. Still perform required final
filesystem and journal checks. Ordinary aggregation remains unchanged.
After successful discovery, drop the discovery budget/scratch and run the existing
complete checker with a fresh profile and the original caller policy. These are
two explicitly bounded passes, not a claim of one shared whole-command numeric
allowance or all-heap accounting. Discovery grants no semantic admission witness.
## Acceptance
- Real executable and library cases load mixed OA/SA multi-file fixtures with
cross-file/scoped typed references and nested ordinary records. Independently
construct complete expected models for those same bytes; check actual complete
JSON/human diagnostics and status rather than inventing a model field in Report.
- Prove exact source/directory preservation on success, warning and refusal,
including Unicode/CRLF and comment/string text resembling includes or aliases.
Exercise missing UUID classes and wrong-kind/unresolved typed references.
- Test missing/cyclic includes, root/path escape, case and physical aliases,
invalid UTF-8/nonregular files, pending journal, and selected exact file/byte/
depth/edge boundaries. Platform-specific checks are claimed only when run.
- Observe the actual shared discovery constructor/counters: multi-file cumulative
work, retained conservative reservations after dropping a unit, zero temporary
balance after successful units, exact caller/profile capture and first-error
location with an unparsed later sibling. Use real small boundary controls with
positive cases; test-only tightening must not become public policy.
- All old core and relevant filesystem/source/stack tests remain passing. Run
existing ordinary CLI tests plus new mixed CLI tests, actual CLI commands,
strict core/CLI Clippy, doctests and formatting disposition. Bind gates to a
reviewed clean source commit and preserve initial failures without weakening
model, bytes, locations or resource expectations.
Independent source/runtime review follows implementation. Parent owns integration,
compiler execution and acceptance. Core discovery/parser and CLI/report/tests/docs
may be delegated with disjoint files and the interfaces above. Linux remains
user-deferred; no GUI/editor/save/history or release integration is implied.
@@ -0,0 +1,48 @@
# Read-only mixed CLI: independent critique
Research only against `bab6f96a5b05b37f2b5d67a430aed0f67d783e73`; no builds, application execution, production edits or remote actions. Reviewed implementation map SHA256 `cb611919a1d6b6463f5e7054922d40457734305656e0dfff9dd4a1388a2c4ed7`. References below are relative to that source. This selects a bounded next outcome, not acceptance of an implementation.
## Recommendation
Implement explicit `arcadia check-mixed ROOT [--json]`: discover actual included files safely, then invoke the existing complete borrowed checker on captured original bytes. Require schema8 and explicit UUIDs, including ordinary declarations in this command. Return diagnostics through the existing report envelope, with no changes, migration, stabilization or write. This delivers useful command-line validation for the textual-model/linting goal in `PROJECT_GOAL.md:64–69,96`, while leaving editable model adoption separate.
`check --mixed` is also coherent, but offers no semantic advantage and requires more option-combination rules. Choose one spelling. Automatic replacement of `check` is unsafe: existing ordinary drafts intentionally accept omitted IDs and older versions. Schema8 alone cannot select between those policies. A manifest of every file is a simpler parser-free discovery interface, but transfers routine include enumeration to users and is not an equivalent root-file workflow. Full compile/index adoption is substantially larger and unnecessary here.
## Simpler correct discovery policy
Prefer **one shared discovery Budget and ModelCounts, with conservative completed-unit reservations retained until discovery ends**. This is simpler than the map's proposed exact release/reconciliation seam. Do not describe its counters as exact live storage, an admitted syntax witness, or carry into the final verifier. Ordinary and public in-memory checker accounting must remain unchanged.
The source supports this narrower policy:
- `analysis_source/mixed.rs:390–422` performs lexing and the shared `Parser::unit` using one Budget/ModelCounts. `lex.rs:15–68` charges bytes, scanner events including trivia, and scanner temporary string work. State shares model counts and typed numeric parsing rather than creating a fresh per-file allowance.
- Full parsing retains each completed unit, tokens and lexical owners, and additionally constructs positions (`mixed.rs:425–511`). Dropping the discovery unit does not itself decrement Budget. Leaving its final charges reserved therefore remains an upper bound on live producer-domain storage; it does not create dangling ownership or an authority witness. Keep normal existing temporary/UUID/provisional-key releases within the parser unchanged.
- For the same successfully parsed files and depth-first order, discovery uses the same unit grammar, U/token/reference/numeric events and transient string decoding as full parsing. Omitting position construction removes nonnegative metadata/text charges. Initial or incremental discovery file-slot reservations must be no greater than the full parser's F file slots, and must not charge already-visited paths again. Under these conditions, retaining completed-unit charges causes **no additional producer-cap refusal relative to the corresponding successful full syntax parse**, which retains those units anyway. This conditional argument does not promise identical failure precedence for invalid input or disk discovery.
- Both existing walkers push includes in reverse for source-order DFS (`source_files.rs:511–517`, `source_project/traversal.rs:179–183`). Preserve that order and once-per-path inspection. Repeated authored edges still count; repeated targets do not get another syntax budget.
Name the phases explicitly: one bounded discovery syntax pass, followed by one independently bounded complete verification pass. Derive both profiles from the same original caller policy; do not expose arbitrary production profiles. In particular, numeric work is capped per named pass, not falsely advertised as one 50,000,000-unit command-wide allowance. Discovery Budget, parser state and all ordinary/typed/token owners must be dropped before full verification starts. Only loader-owned sources, bounded include/path bookkeeping and diagnostics survive. Do not retain an unnecessary parsed model or clone a complete syntax witness.
This reasoning covers the existing logical producer domains, not all Rust allocations, path bookkeeping, model heap, allocator capacity or RSS. Resolved include targets/locations belong to the existing bounded loader domain; do not call their transfer a producer-ledger reconciliation. Discovery never invokes the resolver or its exact syntax-inventory check. No new refund mechanism is needed merely to make already-freed units disappear from a conservative reservation.
An alternative fresh unit budget with explicit remaining aggregate work caps could also be correct, but requires transferring numeric/event usage and separating remaining work from per-unit storage limits. That is more machinery than retaining reservations. Fresh unrestricted per-file budgets are rejected: they silently multiply numeric and other work ceilings by file count.
**Concrete failure obligation:** existing discovery continues after `inspect_includes` failures (`source_files.rs:519–521`), whereas `Budget::active` (`budget.rs:228`) returns a latched Error containing a Span but no filename. Reusing that failed budget for a sibling would risk reporting the old span against the sibling. Select terminal mixed syntax/work failure: keep its first located diagnostic and perform no further unit parses using that budget. Still perform the selected final filesystem/journal checks. Preserve ordinary-path aggregation unchanged. Specify first-failure behavior rather than attempting to claim diagnostic identity with complete in-memory validation.
## Disk ownership and safety
Reuse the existing logical-path, root-containment, regular-file, bounded-read, case/physical-alias and journal checks (`source_files.rs:111–325,536–549`). Before any read, enforce aggregate effective source bytes `min(caller.model.max_source_bytes, 64 MiB)`; checking only the caller's possibly unlimited ceiling and rejecting later in the parser is insufficient. Pass the original ProjectLimits to final verification, without silently widening or replacing them.
For a fresh load, consume the discovered DiskProject into an opaque read-only `{ bundle, diagnostics }` after final checks, dropping expectations/root/reachability. Every stored source was discovered from the entry; no overlay/detached-input preservation is needed. Avoid `reachable_bundle()` (`source_files.rs:59–72`), which clones all source strings. The existing temporary raw expectation bytes and UTF-8 strings are two bounded copies, not one accounted allocation; document reuse honestly. A smaller fresh-only storage owner may be a later optimization, not a prerequisite for this milestone.
Keep reserved journal names, pending-save refusal and no implicit recovery. Existing path checks do not establish an atomic multi-file snapshot or defeat every concurrent replacement race (`source_files.rs:177`); promise validation of captured bytes and no writes by this command. Do not broaden platform claims beyond actual tests. Fail discovery before invoking the complete checker on missing/invalid buffers.
Route this command before ordinary CLI `prepare` (`oa-cli/src/lib.rs:213–310`), which calls ordinary lint/ID analysis/compilation even for Check. An Arguments command branch is sufficient; do not add a fake SourceIndex, editable Prepared value, save conversion or mixed write option.
## Falsifiable acceptance
1. Real executable OA/SA multi-file fixtures: typed/scoped cross-file references, ordinary nesting, escaped includes, comments containing `include`, Unicode and mixed CRLF. Compare complete diagnostics/report bytes and independently authored complete models for the same captured literals. Hash files and directory entries before/after; reject `--write` and unknown options.
2. Discovery-budget tests: two files each individually below a tightened private numeric/event cap but jointly over it; repeated target inspected once; repeated edges counted; one shared ModelCounts limit across files; exact cap/cap-minus-one boundaries. Test-only profile tightening must not become caller-controlled public authority. Compare discovery producer reservations with the full parser at equivalent successful prefixes/fixtures, including quoted provisional releases and omitted projection charges.
3. Failure attribution: first file triggers a latched budget refusal while a sibling remains queued; assert the original file/span once, no sibling reinterpretation and no final checker invocation. Include missing IDs in project, ordinary declaration, typed definition and parameter, plus unresolved/wrong-kind references reaching final verification.
4. Existing filesystem invariants: bounded aggregate reads even with unlimited caller bytes; include depth/edges/files, invalid UTF-8, nonregular files, escapes/reserved names, case/physical aliases, cycles and pending journals. Preserve ordinary loader/CLI results. Pin mixed diagnostic precedence where discovery differs; platform-specific link/FIFO cases remain conditional.
5. Verify actual normal-library/CLI boundaries and relevant finite stack controls after helper extraction. No universal headroom or full authoring claim follows from these checks.
No design blocker remains if the contract adopts the conservative reservation meaning, terminal failure rule, effective pre-read byte cap, and separate fresh final verifier above. The implementation must demonstrate those conditions; this report does not waive existing parser limits or substitute discovery success for complete semantic admission.
@@ -0,0 +1,164 @@
# Mixed CLI read-only check: implementation map
Design only against public-read branch bab6f96a (parent reports accepted gates).
No source edits, compiler or remote actions. Paths/lines refer to this source.
## Recommended user outcome
Add explicit `arcadia check-mixed ROOT [--json]`, requiring the public checker's
schema8 and explicit UUIDs. Preserve check/lint/stabilize/rename-alias behavior.
Use the existing report envelope with operation check-mixed, status checked or
invalid, no changes, written=false, migration=null and identities_to_stabilize=0.
The operation validates captured original bytes; it does not stabilize, export,
format, index or save. Help must state this distinction and reject --write.
The command choice and discovery architecture are separate decisions. Merely
adding a command enum variant does not make the existing loader support typed
syntax. A real parser-consistent discovery seam is the prerequisite below.
## Current blockers and reusable code
- oa-cli/src/lib.rs:213 prepare loads source_files::load_project, then ordinary
lint/analyze/compile (234–310). Operation::Check still returns Prepared holding
CompiledSourceProject and a disk snapshot; it is not a read-only mixed route.
- main.rs:76 dispatches all accepted arguments through prepare and optional write.
Add a separate report-returning mixed-check branch before that branch. Do not
forge Prepared or an empty SourceIndex. An explicit Arguments command enum can
separate read-check from existing editable Operation, or use a distinct
check_mixed flag/variant handled before prepare; avoid illegal write combinations.
- source_files.rs:329 load_project creates a DiskProject then discover_missing.
Discovery's DFS reads bounded bytes and tracks originals/expectations (389–494),
but495 calls ordinary inspect_includes and529 runs ordinary compile_bundle.
- source_project.rs:207–268 inspect_includes validates paths and calls ordinary
language::parse_unit, so it rejects valid short typed declarations. Filtering
that diagnostic cannot reveal the missing include graph safely.
- mixed.rs:390–422 already lexes and invokes the shared Parser::unit with actual
mixed State and explicit IDs, producing ordinary.includes plus typed syntax.
This exact unit grammar can inspect includes without resolving global references.
Extract/reuse this narrow unit operation instead of a regex, guessed brace
scanner, second quote decoder or calling the complete checker on partial bundles.
- source_files.rs:104–216 root_entry/check_logical/disk_path/read_bounded already
enforce root containment, canonical logical names, reserved journal namespace,
link/regular-file restrictions and bounded reads.240 check_snapshot and293
check_physical_aliases preserve aggregate and physical-alias checks. Reuse these
functions in one core discovery engine; do not replicate their security logic in CLI.
## Minimal safe ownership shape
Introduce a named read-only discovery entry in source_files, with a small private
closed selector OrdinaryEditable / MixedRead for shared discovery dispatch.
Existing public discover_missing/load_project select OrdinaryEditable and retain
all current completion/lint behavior. MixedRead selects mixed include inspection
and skips ordinary compile/stabilization; it still performs all disk/path/journal
checks. No generic caller-provided parser/loader callbacks or new public framework.
Prefer an opaque owning `MixedSourceSnapshot` exposing only bundle() and
load_diagnostics(), or a narrowly scoped `load_mixed_source` result owning those
values. Do not advertise it as a save snapshot or provide conversion into editable
CompiledSourceProject. Internally reusing DiskProject's captured bytes is possible,
but returning DiskProject publicly would unnecessarily expose save/discovery
operations and expectations. Keep original raw-byte expectations private if reused.
This design adds a small wrapper, not a clone of every buffer for an extra model.
CLI owns the snapshot, borrows its complete reachable SourceBundle while calling
language::check_mixed_bundle, maps warnings/errors into the existing Report, then
drops CheckedMixed before dropping source. Report owns mapped diagnostic strings;
no borrowed checker escapes and no self-referential source/result struct is needed.
Report has no Project field: complete model evidence comes from independent core
and CLI-library tests of those same literals, not an invented JSON assertion.
## Discovery parser work and limits: resolve before implementing
Discovery is an extra syntax pass; final borrowed checker remains the sole complete
semantic admission. Its existing budgets must be fresh for that full pass; do not
subtract discovery work from final counts or represent a successful partial scan
as an admitted model. Re-reading/reparsing captured strings is explicit bounded work,
not a claim that the checker itself reparses or that disk is reread between phases.
The mixed unit helper needs a genuine Budget and ModelCounts. A naïve new budget
per file silently multiplies allowed discovery numeric/token/reference work by the
file count; a single shared budget with all retained-text totals left charged after
units are dropped misrepresents live storage. Therefore contract must choose a
small explicit **discovery-phase work policy** and lifetime:
- Recommended: one shared discovery work budget across all captured file parses,
cumulative bytes/tokens/references/numeric/syntax-event work, with per-unit syntax
owners dropped after copying only include locations. Reuse Parser::unit and its
resource checks. Name and check temporary per-unit metadata/text ownership before
growth if selecting producer mode; reconcile/release it on unit destruction.
This is a real small producer-lifetime seam to specify, not existing free behavior.
- Simpler alternative: per-unit bounded inspection with a documented aggregate
upper bound of max_files times its cap. It is finite but can be far larger than
the selected checker work profile; do not choose it silently or describe it as
inheriting one whole-project numeric budget. Parent may reject that cost policy.
- Do not retain all parsed witnesses then clone/reparse the complete bundle merely
to avoid accounting a dropped unit. That grows live state and complicates source
lifetimes for no consumer benefit. Do not stream-load into a borrowed BTreeMap
while previously parsed units retain references into it; ordinary Rust borrowing
disallows this without additional ownership infrastructure, which is unnecessary.
The implementation contract should pin the selected discovery bound/diagnostic
order and helper's drop/refund rules before source edits. This is the main remaining
bounded design question, not an argument for full editable-source adoption.
## Filesystem and diagnostic contract
Preserve existing root/file checks, UTF-8 rejection, aggregate byte/file/edge/depth
limits, case/physical alias refusals and pending-journal detection. Root depth0;
include paths resolved by existing resolve_include; count repeated authored edges.
Final complete check still rejects cycles/semantic failures using its exact original
coordinates. Discovery diagnostics prevent invoking checker with missing/invalid
buffers. Return exit3 for disk/path/pending-journal failures under existing CLI
mapping; exit1 for source/semantic rejection,0 for valid with advisory warnings,
2 for invalid arguments. Pin mixed loader's diagnostic precedence in tests rather
than assuming it equals in-memory checker's earlier/later limit branch.
Do not suppress pending_save simply because operation is read-only: existing CLI
refuses it, and the captured files may represent interrupted save state. No journal
recovery is implicit. Neither old nor new read path promises atomic multi-file
snapshot/CAS against concurrent external replacement (source_files.rs:177 comment).
Promise unchanged bytes by this command and validation of captured bytes, not
that the disk still equals that snapshot after a concurrent editor writes.
## Compared/rejected options
- Automatically replace ordinary check with mixed: breaks existing omitted-ID and
migration behavior. Schema8 alone does not distinguish ordinary drafts from the
stricter explicit-ID mixed contract. Avoid heuristic detection/fallback on errors.
- `check --mixed`: coherent alternative explicit spelling, but adds an option whose
invalid combinations must be excluded for mutations. Dedicated check-mixed makes
the limited outcome easier to explain; select one spelling, not both initially.
- Explicit all-files CLI manifest/bundle: can reuse checker immediately, but forces
users to enumerate includes and introduces another input/argument format. It is
useful only if a real pipeline already supplies bundles; not the recommended
ordinary filesystem workflow and not a substitute for safe include loading.
- Full compile_bundle adoption: requires typed stabilization/index/update/formatter
and application consumers; none is necessary for this read-only outcome.
## Finite acceptance and scoped files
Core changes: source_files shared discovery selector + read-only snapshot;
language mixed unit inspection helper and narrow reexport for core-only use;
source_project include-location conversion reuse where appropriate. CLI lib
arguments/report path + main dispatch, docs/source-cli.md/help, focused tests.
No changes to updater/save/formatter or public CheckedMixed authority.
Test actual executable on independently authored OA/SA three-file fixtures with
cross-file typed/scoped references and ordinary nesting. Exact complete JSON
warning/error reports, raw original byte hashes/directory listing unchanged after
each command, including CRLF/Unicode and comments mentioning include/aliases.
Core tests compare independently authored full models for those same bytes.
Exercise missing/cyclic include, invalid path/root escape, case/physical aliases,
nonregular/invalid-UTF8 file, pending journal and exact aggregate/depth/edge limits.
Only claim platform-specific link/FIFO tests where cfg permits; Linux remains
user-deferred. Exercise missing IDs in all four classes and typed unresolved/wrong
kind errors. Verify --write rejection and all existing ordinary CLI commands remain
unchanged. No fake success for an empty include graph or wrong command dispatch.
Add unit-hook counter/lifetime evidence for the chosen discovery work policy and
repeat relevant existing filesystem/stack regressions after shared-loop factoring.
Parent decisions needed: command spelling; explicit discovery work/storage policy
above; whether reuse of private DiskProject storage under opaque wrapper is worth
its duplicated captured bytes versus a smaller read-only buffer owner. No source
or compiler work is authorized by this proposal.