Skip to content

Modularize Scheme event AOT, parse TLA+ sets, and optimize parser core - #13

Draft
GTrunSec wants to merge 596 commits into
mainfrom
codex/final-event-offset-aot
Draft

GTrunSec wants to merge 596 commits into
mainfrom
codex/final-event-offset-aot

Conversation

@GTrunSec

@GTrunSec GTrunSec commented Sep 26, 2026 •

Copy link
Copy Markdown
Contributor

Scope

  • Keep the generic Scheme event fold as the parser authority, with separate execution, typed IR lowering, and public facade modules.
  • Add POO-admitted source-delimited, first-split, and balanced-reference policies that lower through the existing Rowan event AOT IR; Org-specific grammar remains in Orgize.
  • Incorporate TLA+ set union/intersection grammar and tests from PR Parse TLA+ set union and intersection operators #19 as an identical patch.
  • Keep the newer Rust Rowan graph index and explicit AOT module origin changes on this same branch.
  • Move the language-support implementation to the top-level package and pin the reverted poo-flow-core@e85fd45303b208b23e5957fd316e7004994109a4 revision.
  • Add Scheme LR construction candidates, a canonical LR reference, contextual scanner ranking, and mode-certified incremental checkpoint reuse across deterministic and selective-GLR prefixes.
  • Drive fresh Scheme LR parsing in one continuous scanner/LR loop, with the existing checkpoint path for incremental captures and observed phases. Regression tests compare fresh and checkpointed artifacts for arithmetic, GQL, HL7, and rejected input.
  • Fuse semantic operand mapping and recognition concatenation with Gerbil v0.19 foldl, and skip unused state-stack prefixes during LR reductions.
  • Add explicit lalr-then-follow construction: keep LALR for conflict-free grammars, use follow-partition LR(1) only after unresolved LALR cells, preserve genuine conflict rejection and the selective-GLR route. The default remains LALR.
  • Keep the concurrently added POO-native graph query context for language packs on this PR branch.
  • Include the follow-up Rowan graph index nearest-ancestor projection.

Complete pinned TLA+ corpus closure

  • Rebased this existing PR onto main c6ecb40dbc6816510b6ad68d3dc68429b89c9531, including main's strict final-token offset validation.
  • Close all 195 remaining SANY-positive root syntax rejections in one slice: 424/424 accepted, zero invalid artifacts and zero source roundtrip failures, retaining all 229 previous successes.
  • Immutable corpus: tlaplus/Examples@ceeaa904140e3e03781cb2a79cd6c6d8b8b08e10; the Scheme runner verifies the clean checkout and exactly 424 tracked TLA+ files.
  • Cover nested/concatenated modules, original document text, higher-order and symbolic formals/operators, LAMBDA, labels, selectors, LET, ASSUME/PROVE and hierarchical proof step spellings. Pure CST validation rejects bad proof levels, missing QED and inadmissible subproofs.
  • Correct inclusive marker columns, retain reductions under ineligible layout markers, and guard precedence-suppressed reductions on outdent. Invalidate old compiler cache receipts for the new action semantics.
  • Keep the parser and comparison in Scheme; Java is used only for the pinned official SANY v1.7.4 oracle (tla2tools.jar SHA-256 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88).
  • Require corpus and structural comparison in Linux CI. Noninteractive Scheme watchdogs fail after five seconds of silent output; actual module admission, artifact validation, LR work and completed benchmark batches report progress.

Local verification at 9d148da (implementation) / 567daf9 (test ownership)

  • Keep the closure regression module in the executable test owner, excluded from the production library catalog.
  • Fresh isolated Gerbil v0.19 build passed.
  • Complete native regression: 54 modules / 274 cases, MODULE-OK, HARNESS-OK, final OK, with the five-second watchdog active.
  • Pinned Examples corpus: 424/424 accepted, valid and byte-exact roundtrip.
  • Structural oracle gate: 72 expression trees, 10 genuine root syntax rejection fixtures, 2 controls excluding import/semantic oracle failures; all passed.
  • POO Flow corpus: 28/28 accepted, valid and roundtripped through both the published layout entry and the candidate.
  • Rust workspace: 74 passed / 2 ignored. Generated arithmetic Scheme LR and HCL Scheme step checks passed. Compiler artifact cache and closure regressions passed after the cache version change.
  • Silent-child negative control fails at five seconds; git diff --check passed.
  • CI test preloading explicitly exposes the project source path (fbaf317) so source-only fixture imports are admitted before gxtest initializes.
  • Run every native test module in a separate process (3654201), keeping the 1 GB heap fence, five-second silence rejection and existing performance thresholds. This prevents all source expansion contexts from accumulating in one heap.
  • Use gxtest assertion verbosity (ca86a02) to expose actual progress inside exhaustive LR recognition equivalence sweeps; the five-second silence gate remains unchanged.
  • Incrementally admit compiled macro phase bindings (7c15333) so cold macOS imports expose real library progress before gxtest imports a source module. Focused ANTLR, LR equivalence and GQL/Rust generation tests passed with the five-second watchdog.
  • Exact-head remote CI at 7c1533356585154c8b5d340f64ffefb289d18907: Rust/Rowan, Ubuntu native Gerbil and macOS native Gerbil all SUCCESS. Run 37039132506.
  • Both remote native suites completed all 54 test modules. Ubuntu also passed all 72 SANY expression trees, 10 syntax negatives, 2 oracle exclusion controls and the complete clean 424-file corpus with zero invalid artifacts or roundtrip failures.
  • Final remote head matches the clean local worktree, and current main c6ecb40dbc6816510b6ad68d3dc68429b89c9531 is an ancestor.

Evidence boundary

The 424-file syntax receipt closes this immutable corpus. The 72-tree projection is a bounded structural gate, not complete SANY semantic equivalence, full proof hierarchy equivalence, every precedence interval or PlusCal translation. TLC qualification remains a separate gate. Orgize PR #18 remains a downstream consumer and should pin an exact reviewed parser head.

Scheme engine and common language library boundary

  • Move POO Loader declarations to language-support/entry; engine entry owns only descriptor dispatch and generic policy execution.
  • Make corpus, scanner and build services explicit through language-support/development, with direct caller migration.
  • Keep GQL production parser.ss independent of corpus; parser-test.ss owns the corpus and development entry over the exact production descriptor.
  • Supply GQL lexical rules and exact ANTLR terminal bindings from grammar.ss, preserving lexical order and removing name-based GQL assumptions from the common adapter.
  • Synchronize modular English design/paper rationale in docs/research/scheme-engine-library-boundary.org, including Scheme examples and falsifiable limits.
  • Repair prior CI harness failures: install GNU timeout on macOS and run the renamed executable research control explicitly, retaining the native no-cases guard.

Evidence

  • Unified local gate: 435 cases/checks, 18 bounded child processes, all exit 0.
  • Exact old/new GQL Grammar IR and Parser IR equality; 1176 Bound IR identities/references and pinned source coordinates match. Author-origin coordinates and resulting complete Bound IR identity digests remain distinct.
  • Native adapter compilation succeeds under the unchanged 240-second total / 5-second idle watchdog after removing local Nix/macOS C compiler mixing. Earlier cold-cache and idle failures are retained in the design receipt.
  • No parser speedup or complete GQL/ANTLR semantic equivalence is claimed. Full exact-head matrix CI is tracked separately.

Complete language interface alignment

Revision 71efb9f migrates all eight shipped packages and ten public entries to:

  • grammar.ss: language declarations, lexical/policy data and pinned source metadata.
  • parser.ss: production LanguageLoader. only; no corpus/build/scanner/test services.
  • parser-test.ss: corpus, optional LanguageDevelopmentLoader. and independent conformance tests.

All 53 accepted/rejected corpus members have production/development dispatch controls for exact descriptor identity, status, complete events and roundtrip. Existing language-specific tests are retained; source workers, HCL generated-backend profiles and build strategies now belong to the development interface. Test and benchmark consumers import the relocated data explicitly.

The extended topology guard rejects development imports and declarations in production interfaces. A new separate all-ten-entry benchmark reports raw samples and nearest-rank P50/P95 with workload identity; the historical four-language measured gate is preserved. English design documentation records ownership and executable scientific questions.

Verification boundaries: Scheme readers confirmed unchanged grammar declarations and relocated corpus bytes; source-overlay boundary controls passed all 53 dispatch comparisons. Affected Rust all-target/all-feature Clippy passed. Interrupted/cold local native attempts and nonzero child exits remain failures, even after success markers. Exact-head Linux/macOS native execution is being qualified by this revision's CI; no complete native or latency improvement claim is inferred from local build output.

All-language qualification follow-up

Previous alignment head: bbbe76a058786f125d6c382a69d9138476c7f064.

  • All eight language packages / ten production entries use the three-interface ownership contract. All 53 corpus entries are preserved; production entries have no development services.
  • Native build failures at 0a78ea9 and 712c65f remain retained evidence. The first combined build stopped during GQL Scheme-to-C translation; after separate translation, both platforms stopped when their largest C frontend jobs began together.
  • The conformance build retains Gerbil's public-API-generated bootstrap, reuses SDK objects and uses Gambit's documented ordered incremental bases. The real work queue starts large jobs early and reserves a worker for short independent units. No synthetic heartbeats, timeout changes, parser algorithm changes or weakened semantic assertions.
  • Local cold project-object rebuild: exit 0 in 64.06 seconds under unchanged 240-second completion / five-second output-idle limits. It retained existing Scheme-to-C outputs and SDK objects; this is not a fresh toolchain/source build claim.
  • All 26 local conformance child processes then exited 0 under unchanged ten-second limits. This includes all eight language suites, all three TLA+ entries, the 53-member production/development comparison, DSL/POO/source-origin controls and the ten-entry benchmark smoke.
  • Each of ten independently selected native benchmark workloads completed twenty samples and a matching descriptor receipt under its ten-second process fence: 200 raw samples, ten complete receipts. The failed combined twenty-sample attempt timed out after 182 samples and nine receipts; it is not a complete result. Measurements are warm corpus-batch parsing/roundtrip, not total process latency or a speedup claim.
  • The complete existing call/array author package now uses supported strings, unambiguous names and implicit node-body sequences. Its independently written eleven-case native suite and 85 inline-control checks exited 0. No new DSL constructor or grammar interpreter was introduced.
  • The English author-interface study distinguishes completed file alignment from remaining public API design: generated IR/parser exports, backend binding imports and lexical catalog duplication still require a coherent design review.
  • CI for bbbe76a: Linux/macOS native jobs failed; Rust passed. These failures are retained. Local receipts did not establish remote qualification.

Checked source author frontend — 2026-10-07

Preceding frontend implementation head: 2a55f99feeb81a822b4c4aefb1d4723d6e806d83.

  • Bash now declares identity, one syntax block and one rules block directly in deflanguage, with native defgrammar-syntax vocabulary. No additional required SourceGrammar model was added.
  • The common shell source library derives scanner states, delimiter widths, capture/result programs, command continuations and internal POO strategy assembly. Bash authors no longer maintain scanner transitions, command VM opcodes or duplicate command schemas.
  • Removed the legacy deflanguage-source author declaration and raw profile/strategy exports from the public source facade. Migrated parser receipt and internal test callers directly; no compatibility alias or runnable legacy grammar remains.
  • The topology contract rejects backend profile declarations in author grammars. New negative controls reject duplicate blocks/rules, backend recipe constructors, unresolved references, non-consuming repetition and unterminated command-list calls. Existing independent Bash semantic assertions are preserved.
  • First native initialization failed under the unchanged ten-second child fence. POO slot names shadowed outer lexical values; distinct lexical initializer names fixed recursive reads. The failed attempt remains evidence.
  • Final incremental native translation/link completed with actual exit zero; the final native link took 15.66 seconds under the unchanged 240-second completion/five-second output-idle fences.
  • Final complete local closure: all 26 children exited zero under unchanged ten-second fences. This covers all eight language suites, topology, Loader/source services, native POO/composition/provenance controls and the ten-entry one-sample benchmark smoke. Bash reported 31 passing cases, including the two new author-contract cases.
  • English research and author documentation record the implementation, the Scheme witness answering both design questions, paper transfer limits and removal of legacy examples. Internal profile documentation is identified as compiler/executor contracts.

Remaining boundaries: source plans remain distinct from CFG/LR GrammarIR; macro blame currently covers the rule block; dispatch inference is scoped to the closed shell adapter. General ambiguity analysis, precise expansion provenance, complete module relocation, clean build/downstream installation and performance gains are not claimed. Exact-head GitHub CI for this new commit is pending and is separate from local qualification.

Parser metadata values and optional native POO — 2026-10-07

  • All eight language packages / ten production entries now author release language, version and contract in parser.ss; grammar.ss exports unbound syntax products. Upstream source pins remain grammar inputs.
  • Metadata accepts a distinct symbol-keyed association-list value or a native POO object. Ordinary authors need no .o or prototype declaration. Native inheritance/override is optional. Engine admission binds effective identity once, snapshots identity strings and derives digest fields while retaining either representation.
  • Focused tests compare value and inherited-object identity/digests/events/roundtrip, retain real overrides, and reject missing fields, duplicate keys and invalid values. Production/development identity and corpus checks remain independent.
  • A narrow Scheme grammar frontend avoids unrelated source adapter imports. Internal Bash product inspection is a test-only fixture derived from the compiled DSL. Command/Source generation removed an unused test-suite import.

Local qualification and limits

  • Final native link: actual exit zero, 32.18 seconds under the unchanged 240-second build / five-second output-idle fences. The preceding complete recompile/link took 218.41 seconds with actual exit zero.
  • Final complete closure: all 26 children actually exited zero under unchanged ten-second fences, including all eight languages, ten entries, value/POO contracts, services, native POO/composition/provenance controls and benchmark smoke. This one-sample smoke is not a performance comparison.
  • Binding-name generation: 135 traces, exit zero. Command/Source generation: 54 controls, 9.01 seconds, exit zero. Downstream Rust execution is not established by those generators.
  • Retained failures: stale native entry/strategy consumers crashed until recompiled; intermediate native build/link attempts exceeded output-idle bounds; generator/fixture imports and fixture process exit exceeded child bounds. The expression fixture now uses the existing disposable child exit helper only after all 85 assertions and output flush; failing assertions still abort.
  • At preceding head 2a55f99, Rust/Rowan CI passed; both native CI jobs exceeded the 240-second conformance compilation fence. The new head's clean CI remains a separate gate. No timeout was widened.

Command entry contract migration (1500e75)

  • Separate assignment-tail and pipeline-head capabilities from private rule IDs in Scheme admission, execution, and generated Rust execution.
  • Infer ordinary command selectors from token structure; preserve direct-expression and author-macro invocation source blame.
  • Qualify complete event parity under private-rule renaming and fail closed on invalid entry contracts.
  • Local results: all 26 bounded DSL/research children exited 0; Bash 46 cases; Rust library 127 tests; 54 Scheme-generated Command/Source controls. Child limits remain 10 seconds.
  • Compile the existing native research child exit binding before research execution in CI.
  • Remaining architecture gates: shared contextual Parser IR, complete macro lineage, context-aware recovery, and cross-edit incremental reuse. This change does not claim those gates or a latency improvement.
  • Exact-head CI is queued for 1500e75.

Single source compilation and native descriptor ownership (1d2e677)

  • Compile source providers once, returning the identity recipe and executable engine from the same admitted plans.
  • Fix the builtin FFI facade to import release-bound descriptors from parser.ss. Add publication coverage to the existing entry-boundary suite.
  • Separate Rust command product types from execution and remove the test glob import reported by exact-head CI.
  • Local qualification: all 26 bounded research/conformance children exited 0; Rust library 127 tests passed. The broader native ABI suite and ASP Rust quality gate are not locally qualified; cold dependency loading/build receipts failed existing deadlines.
  • Design direction: Rust consumes Scheme-owned AST/CST through the C ABI; Rowan APIs are not required by the primary client. Mandatory Rowan dependency separation and independent native AST access remain implementation work.
  • Exact-head CI is running for 1d2e677.

@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Sep 26, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-09-26T05:00:54.459175Z 2adf0e3 PR opened
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@GTrunSec GTrunSec changed the title Allow saved source offsets in event-fold final tokens Modularize Scheme event AOT and parse TLA+ set operators Sep 28, 2026
@GTrunSec GTrunSec changed the title Modularize Scheme event AOT and parse TLA+ set operators Modularize Scheme event AOT, parse TLA+ sets, and optimize parser core Sep 29, 2026
@GTrunSec
GTrunSec force-pushed the codex/final-event-offset-aot branch from 85f62fe to 9d148da Compare October 2, 2026 16:31
Use Gerbil final record contracts for private LR, recognition, event and
machine metadata while retaining checked accesses and existing protocols.

Add complete-artifact matched request workloads and native Scheme admission
of repeated CPU benefit, tails, SDK control and independent image identity.
Bind the separate CPU-improvement requirement into locked uv/native Ascent
review, with mutation controls and official compiler/research documentation.

Keep CI, runtime budgets, allocation admission and public DSL unchanged.
Preserve source-bound Lean, Quint and real AOT controls, rejected scan trials and explicit open throughput gate. No full performance matrix or SMP acceptance is claimed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant