Skip to content

feat: bring up ASL-generated functional model for gfrun - #183

Draft
zhoubot wants to merge 58 commits into
mainfrom
codex/functional-model-g1-step
Draft

feat: bring up ASL-generated functional model for gfrun#183
zhoubot wants to merge 58 commits into
mainfrom
codex/functional-model-g1-step

Conversation

@zhoubot

@zhoubot zhoubot commented Aug 29, 2026

Copy link
Copy Markdown
Contributor

Scope

Single PTO-SPEC draft PR for the ASL-generated functional-model producer and checked corpus consumed by gfrun. Keep this PR draft and do not merge until the architecture/toolchain decisions and owner-review gates below are closed.

Implemented

  • Strict ASLRef warning rejection; current ASL checks produce zero warnings.
  • ASL-owned reset, PE0 initialization, 16/32/48/64 fetch/length, one-step execution, faults, transactional generated-memory commit, and generic resumable host-request state.
  • Deterministic full typed-AST inventory, pto-mir-v1, executable MIR, descriptor generation, and fail-closed canaries.
  • Installable PTOASLModel CMake package with opaque C ABI, exact descriptor hash negotiation, generated reset/step paths, C/C++ consumers, relocation tests, and sanitizer coverage.
  • Two-instance isolation strengthened to 1,000 interleaved steps; different instances run concurrently and concurrent/reentrant use of one instance returns BUSY.
  • Checked content-addressed corpus producer now binds builder/schema/release/tool hashes, 64 KiB bounds, stack contract, exact expected TPC/BPC/raw/length/sequence trace, and PTO 0.58.5 encoding identity.
  • gfrun consumer implementation is on the signed LinxCoreModel branch codex/asl-model-gfrun-bringup:
    • ASL is the only gfrun engine; --engine is removed and fails closed.
    • gfrun no longer links soft_core, isa_blockisa, or softfloat.
    • automatic symbol/link canary rejects legacy functional execution reachability.
    • independent permission-aware 64 KiB memory, PT_LOAD/BSS/stack/SP handling, exact package-root descriptor binding, complete current StepResult fields, deterministic success/failure manifests, and result export.
    • Release and ASan/UBSan scalar/block corpus CTests pass; gfsim still builds independently with legacy soft_core.

Current passing evidence

  • make pr-check: 762 tests passed, 2 expected skips on the current PTO head.
  • make repo-check: 542 encoded forms; repository closure passed.
  • make check: strict ASLRef check passed with zero warnings.
  • Fresh Release PTO package: CTest 5/5 passed.
  • Fresh ASan/UBSan PTO package: CTest 5/5 passed.
  • Fresh ASL-only gfrun Release and ASan/UBSan targeted CTest: scalar/block corpus and memory transaction tests passed.
  • The integrated ASLRef/gfrun differential gate runs the same ELF bytes and initial SP, compares every currently exported step field, and passed both cases with byte-identical result.bin.
  • Scalar stop-PC case: expected 16/16/32/48/16/32 trace and 19 00 00 00 result passed.
  • Block-control stop-PC case: expected 32/64 trace and a5 5a 00 00 result passed.

Not yet complete against the bring-up plan

  • The planned real Tile ELF (TLOAD → VEC/SFU → TSTORE) is not implemented; the current block case proves BSTART/L.BSTOP only.
  • The planned exit_group(94) ELF cannot be implemented from current accepted semantics: ADR-0111 explicitly keeps hosted request meanings/fault-vs-exit under issue [programming-model] Define hosted multi-PE startup and runtime ABI #150 and selects stop-PC for initial bring-up. No instruction currently emits a functional host request.
  • Available Linx toolchains emit PTO identity notes for 0.58.0, 0.58.1, or 0.58.3, while the model/corpus require 0.58.5. gfrun still needs the final .note.pto.isa parser, but enabling it now would correctly reject every available corpus ELF.
  • ASLRef and gfrun now share a trace schema for the two stop-PC cases; a separate standalone-library corpus producer and the real Tile/host cases remain missing from the planned three-way differential.
  • Snapshot/restore, memory/Tile summary hashes, full generic runtime construct coverage, callback transaction NDF acceptance, and first-instruction model-lock/ELF-note closure remain open.
  • Seven new architecture Reader Guides and zh-CN projections remain pending owner review; exact release verification stops at that governance gate.
  • G7 superproject pins/model lock cannot be finalized before the producer and consumer commits are reviewed and landed. No LinxCoreModel or LinxISA PR has been opened, preserving the requested single visible PR.

Decisions needed before continuing the blocked lanes

  1. Keep ADR-0111's stop-PC initial scope and revise the plan's third ELF to an injected generic host-request handshake, or open/accept a new NDF/ADR defining the exact guest instruction and ABI for minimal exit_group(94).
  2. Permit a separate Linx LLVM predecessor branch/PR that implements the exact PTO 0.58.5 encoding identity, or explicitly change the delivery contract. Merely relabeling an older toolchain note is not acceptable evidence.

After those decisions, continue with the real Tile/host ELF, ASLRef differential, ELF-note enforcement, exact-head release gate, and final superproject lock. Do not merge this PR yet.

@zhoubot zhoubot changed the title feat: add ASL functional-model step boundary feat: bring up ASL-generated functional model for gfrun Aug 29, 2026
@zhoubot
zhoubot changed the base branch from codex/aslref-warning-cleanup to main August 29, 2026 09:08
zhoubot added 30 commits August 29, 2026 21:41
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