feat: add ASLRef-backed PTO reference model

.github/workflows/ci.yml

@@ -0,0 +1,17 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+    branches: [main]
+
+permissions:
+  contents: read
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Configure and test
+        run: make check

CMakeLists.txt

@@ -0,0 +1,62 @@
+cmake_minimum_required(VERSION 3.20)
+project(PTOASLModel VERSION 0.1.0 LANGUAGES C CXX)
+
+include(CMakePackageConfigHelpers)
+include(GNUInstallDirs)
+
+option(PTO_ASL_MODEL_BUILD_TESTS "Build PTO ASL model tests" ON)
+
+add_library(pto_asl_model STATIC src/client.cpp)
+add_library(PTOASLModel::pto_asl_model ALIAS pto_asl_model)
+target_compile_features(pto_asl_model PUBLIC cxx_std_20)
+target_compile_options(pto_asl_model PRIVATE -Wall -Wextra -Werror)
+target_include_directories(pto_asl_model
+    PUBLIC
+        $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
+        $<INSTALL_INTERFACE:${CMAKE_INSTALL_INCLUDEDIR}>
+)
+
+add_executable(pto-model-run tools/pto-model-run.cpp)
+target_link_libraries(pto-model-run PRIVATE pto_asl_model)
+target_compile_options(pto-model-run PRIVATE -Wall -Wextra -Werror)
+
+if(PTO_ASL_MODEL_BUILD_TESTS)
+    enable_testing()
+    add_executable(pto_asl_model_abi_c_test tests/abi_c.c)
+    target_link_libraries(pto_asl_model_abi_c_test PRIVATE pto_asl_model)
+    add_executable(pto_asl_model_abi_cpp_test tests/abi_cpp.cpp)
+    target_link_libraries(pto_asl_model_abi_cpp_test PRIVATE pto_asl_model)
+    add_executable(pto_asl_model_client_test tests/client_test.cpp)
+    target_link_libraries(pto_asl_model_client_test PRIVATE pto_asl_model)
+    foreach(target
+            pto_asl_model_abi_c_test
+            pto_asl_model_abi_cpp_test
+            pto_asl_model_client_test)
+        target_compile_options(${target} PRIVATE -Wall -Wextra -Werror)
+    endforeach()
+    add_test(NAME pto_asl_model_abi_c COMMAND pto_asl_model_abi_c_test)
+    add_test(NAME pto_asl_model_abi_cpp COMMAND pto_asl_model_abi_cpp_test)
+    add_test(NAME pto_asl_model_client COMMAND pto_asl_model_client_test)
+endif()
+
+install(TARGETS pto_asl_model EXPORT PTOASLModelTargets
+    ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
+install(TARGETS pto-model-run RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR})
+install(DIRECTORY include/ DESTINATION ${CMAKE_INSTALL_INCLUDEDIR})
+install(EXPORT PTOASLModelTargets
+    FILE PTOASLModelTargets.cmake
+    NAMESPACE PTOASLModel::
+    DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/PTOASLModel)
+
+configure_package_config_file(
+    cmake/PTOASLModelConfig.cmake.in
+    ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfig.cmake
+    INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/PTOASLModel)
+write_basic_package_version_file(
+    ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfigVersion.cmake
+    VERSION ${PROJECT_VERSION}
+    COMPATIBILITY SameMajorVersion)
+install(FILES
+    ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfig.cmake
+    ${CMAKE_CURRENT_BINARY_DIR}/PTOASLModelConfigVersion.cmake
+    DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/PTOASLModel)

Makefile

@@ -0,0 +1,14 @@
+PYTHON ?= python3
+BUILD_DIR ?= build
+
+.PHONY: test check
+
+test:
+	PYTHONPATH=src $(PYTHON) -m unittest discover -s tests -p 'test_*.py'
+	cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release
+	cmake --build $(BUILD_DIR) -j 8
+	ctest --test-dir $(BUILD_DIR) --output-on-failure
+
+check: test
+	$(PYTHON) -m py_compile src/pto_asl_model/*.py scripts/pto-asl-run
+	git diff --check

README.md

@@ -10,3 +10,71 @@ model lifecycle, hosted execution, transport, ABI, ELF loading, and validation.
 
 Development changes land through pull requests. The initial ASLRef backend is
 tracked by the repository issue list.
+
+## Reference runner
+
+The first closure runs consecutive PTO instructions inside one ASLRef process.
+It accepts a checked static ELF whose load segments fit the explicit hosted
+memory bound, plus an assembled PTO ASL file:
+
+```bash
+scripts/pto-asl-run \
+  --asl-spec /path/to/pto-spec/build/pto-spec.asl \
+  --aslref /path/to/aslref \
+  --elf program.elf \
+  --stop-pc 0x114 \
+  --stop-after-hits 2 \
+  --start-pc 0x120 \
+  --return-pc 0x114 \
+  --max-steps 6 \
+  --result-address 0x200 \
+  --result-size 4 \
+  --memory-bytes 0x20000 \
+  --tile-elements 1 \
+  --runtime-typecheck minimal \
+  --memory-backend host-sparse \
+  --result-out result.bin \
+  --manifest-out run.json \
+  --lock pto-lock.json
+```
+
+Run repository checks with `make check`.
+
+## Performance status
+
+The one-shot process backend uses a fresh-process reset specialization. The
+pinned ASLRef initializes fresh global storage to zero, so the runner removes
+only the redundant byte-by-byte memory-clear loop while retaining every
+register, queue, Tile, bundle, fault, ACR, and system-state reset. The
+specialization matches the exact PTO reset loop once and fails closed if that
+source shape changes.
+
+Minimal-typecheck runs now default to the model-owned `host-sparse` backend.
+It links a small executable against the exact pinned ASLRef `asllib` and binds
+only `ReadPhysicalMemoryByte` and `WritePhysicalMemoryByte` to an O(1) sparse
+host byte map. Translation, permission, ordering, preflight, faults, decode,
+and instruction semantics remain in PTO ASL. The executable is content-addressed
+by the ASLRef commit, `asllib` hash, model source hash, and OCaml version.
+
+On the measured Darwin host, `scalar.abs_i32_thr` fell from 2415.72 seconds
+with the ASL reference array to 424.93 seconds with host memory, a 5.68x
+improvement, while preserving final TPC and the complete 8 KiB result SHA-256.
+The earlier fresh-process reset specialization remains active; on a 128 KiB
+TLOAD carrier it reduced 600.6 seconds to 61.0 seconds with the same result.
+Use `--memory-backend reference-array` for explicit parity checks.
+
+The remaining process path is still parse/startup dominated for short cases.
+A native persistent-worker prototype reaches sub-millisecond warm decode/step
+latency after initialization, while a full reusable-state reset takes 544–582
+seconds.
+
+The next accelerated backend keeps a pristine initialized worker and forks
+one copy-on-write child per case. This reuses the parsed/typechecked model while
+preserving case isolation. Worker-pool concurrency must be bounded by memory;
+the measured initialized worker peaks near 498 MiB RSS. The one-shot
+host-memory backend remains the default until that snapshot backend passes its
+promotion gates.
+
+The reset contract is in [`docs/model-ndf-v1.md`](docs/model-ndf-v1.md). The
+snapshot lifecycle, identity, transport, and promotion gates are in
+[`docs/worker-snapshot-design.md`](docs/worker-snapshot-design.md).

cmake/PTOASLModelConfig.cmake.in

@@ -0,0 +1,3 @@
+@PACKAGE_INIT@
+
+include("${CMAKE_CURRENT_LIST_DIR}/PTOASLModelTargets.cmake")

docs/aslref-patch-audit.md

@@ -0,0 +1,18 @@
+# ASLRef patch audit
+
+The reference runner consumes ASLRef commit
+`0b6e09066d4186c8a26e02e3bb884bd664d5eb34`, exactly matching the PTO-SPEC
+`.aslref-version` at the model lock's PTO commit.
+
+The initial implementation applies no patch to ASLRef:
+
+- parser semantic patches: 0;
+- typechecker semantic patches: 0;
+- interpreter semantic patches: 0;
+- standard-library semantic patches: 0.
+
+Consecutive PTO instructions execute through a generated ASL harness in one
+ASLRef process. The harness calls only the PTO-owned
+`ExecuteNextPTOInstruction` action and uses reference-profile initialization and
+observation functions. ELF parsing, memory initialization, stop policy, and
+manifest formatting remain outside ASLRef.

docs/model-ndf-v1.md

@@ -0,0 +1,99 @@
+# PTO ASL model NDF v1
+
+This repository consumes PTO architecture from an exact PTO-SPEC ASL revision.
+It does not own instruction semantics.
+
+## Model architecture
+
+- `PTO-MODEL-INSTANCE-001`: one model instance carries one isolated projection
+  of PTO architectural state and model lifecycle state.
+- `PTO-MODEL-ASLREF-001`: the reference backend executes the pinned ASLRef
+  interpreter without parser, typechecker, or interpreter semantic patches.
+- `PTO-MODEL-STEP-001`: one step invokes the PTO-owned next-instruction action;
+  model observations cannot refine its architectural meaning.
+
+## Hosted runner ABI
+
+- `PTO-MODEL-ELF-001`: the initial runner accepts little-endian static ELF64
+  `ET_EXEC` images with bounded, non-overlapping `PT_LOAD` segments and explicit
+  stop-PC/result policy. The caller selects a bounded hosted-memory profile;
+  its memory and Tile capacities are model bounds, not architectural capacity
+  claims.
+  The stop policy may select a later occurrence of the same PC, so a return
+  label embedded in an entry bundle is not mistaken for program completion.
+  A direct-boot profile may start at a verified executable symbol and seed the
+  captured return state plus architectural GPR R10 (`ra`) with the verified
+  return PC, bypassing platform service-request startup glue. The paired state
+  is model ABI: compiler-generated epilogues may select `ra`, while PTO return
+  bundle state independently carries the captured target.
+- `PTO-MODEL-MANIFEST-001`: each run emits a deterministic JSON manifest bound
+  to the exact PTO tree, ASLRef pin, ELF hash, entry, stop policy, result bytes,
+  and final TPC.
+- `PTO-MODEL-C-ABI-001`: C and C++ consumers invoke the hosted reference runner
+  through a versioned standard-layout configuration without observing worker
+  transport details.
+- `PTO-MODEL-HOST-MEMORY-001`: a model-owned executable MAY bind PTO's
+  `ReadPhysicalMemoryByte` and `WritePhysicalMemoryByte` profile hooks to O(1)
+  host storage. It MUST NOT replace ASL-owned translation, access permission,
+  preflight, ordering, fault, decode, or instruction semantics.
+- `PTO-MODEL-HOST-MEMORY-IDENTITY-001`: the host-memory executable MUST link
+  the exact pinned ASLRef `asllib` and MUST be content-addressed by the ASLRef
+  commit, `asllib` hash, model source hash, and OCaml version. Every run
+  manifest MUST record that identity and the selected memory backend.
+
+## Implementation boundary
+
+The implementation assembles a run-specific ASL harness and executes it once
+with the pinned ASLRef interpreter. Consecutive instructions execute inside
+that single process. Minimal-typecheck runs default to the model-owned
+host-memory executable; strict or explicit `reference-array` runs use the
+stock pinned `aslref` binary. ELF parsing, memory initialization, stop policy,
+backend selection, and manifest generation are model implementation behavior.
+
+The transport may later move to a persistent library backend without changing
+PTO architecture or the hosted manifest contract.
+
+## Performance and worker lifecycle
+
+- `PTO-MODEL-FRESH-RESET-001`: the one-shot process backend MAY remove the
+  byte-by-byte `_Memory` clear from `ResetProfileState()` only when the pinned
+  ASLRef process is newly created, its global storage is initially zero, and
+  the process executes exactly one ELF. Every other architectural and model
+  state reset MUST remain present.
+- `PTO-MODEL-FRESH-RESET-DRIFT-001`: the specialization MUST match the exact
+  PTO-owned memory-reset loop once and MUST fail closed if the owner changes.
+  A persistent or reused worker MUST NOT select this policy.
+- `PTO-MODEL-FRESH-RESET-PARITY-001`: promotion requires the same ELF, PTO
+  tree, ASLRef pin, terminal PC, result bytes, and failure class under the full
+  and fresh-process reset policies. The run manifest MUST record the selected
+  reset policy.
+- `PTO-MODEL-WORKER-SNAPSHOT-001`: an accelerated backend may parse and
+  initialize the pinned ASL model once, then fork a copy-on-write child for one
+  case. The pristine parent MUST NOT execute case commands or return into ASL
+  mutable execution after the snapshot point.
+- `PTO-MODEL-CASE-ISOLATION-001`: one case child owns all architectural and
+  hosted state changes for that run and exits after reporting its terminal
+  result. A later case MUST begin from the pristine parent snapshot, not from a
+  full in-model reset of the preceding case.
+- `PTO-MODEL-WORKER-POOL-001`: pool size is a model resource policy. It MUST be
+  bounded independently of GTest concurrency and reported with peak RSS and
+  cold-ready, case-run, and recycle timings.
+- `PTO-MODEL-DARWIN-STACK-001`: a native Darwin ASLRef worker MUST be linked
+  with an explicit main-thread stack large enough for the pinned model. The
+  measured minimum working configuration uses a 512 MiB `LC_MAIN` stack; shell
+  `ulimit` alone is insufficient.
+
+On the measured host, the original process-per-case path took 526–600 seconds.
+Fresh-process reset reduced one 128 KiB TLOAD carrier from 600.6 seconds to
+61.0 seconds while preserving its terminal PC and result SHA-256. A persistent
+prototype takes about 510 seconds to become ready, then decodes and steps in
+less than one millisecond, with roughly 498 MiB peak RSS. Full reusable-state
+reset takes 544–582 seconds, so reset-per-case reuse remains rejected; the
+snapshot child lifecycle above is the selected direction beyond the one-shot
+optimization.
+
+For a compiler-generated scalar throughput ELF, replacing ASL list-backed
+physical memory with the host sparse map reduced 2415.72 seconds to 424.93
+seconds (5.68x) with identical final TPC and complete 8 KiB result SHA-256.
+This optimization is orthogonal to snapshot reuse: it removes linear physical
+memory indexing, while snapshot reuse removes repeated parse/startup cost.

docs/worker-snapshot-design.md

@@ -0,0 +1,92 @@
+# Snapshot worker design
+
+This document defines the selected accelerated lifecycle for the PTO ASL
+functional model. It is a model implementation contract, not PTO architecture.
+
+## Why snapshot workers
+
+The original process backend was cold-start dominated. On the measured Darwin
+host, one specialized run took 526–600 seconds. The fresh-process reset policy
+now removes the redundant memory sweep and reduced one 128 KiB TLOAD carrier
+from 600.6 seconds to 61.0 seconds without changing its terminal PC or result
+SHA-256. A native persistent
+prototype takes 510.271 seconds to become ready, after which decode and step
+commands take 0.284–0.983 milliseconds. Re-running `ResetProfileState()` takes
+544.350–582.447 seconds, so reset-per-case reuse is slower than the current
+backend and is rejected.
+
+The one-shot host-memory backend also removes ASL list-backed physical-memory
+indexing. On `scalar.abs_i32_thr` it reduced 2415.72 seconds to 424.93 seconds
+with identical final TPC and 8 KiB result SHA-256. It remains one process per
+case, so the snapshot design below still targets repeated parse/startup cost.
+
+The initialized worker peaks near 498 MiB RSS. Pool concurrency therefore must
+be explicit and memory-bounded.
+
+## Selected lifecycle
+
+The worker is an asl-model-owned executable linked against the exact pinned
+ASLRef `asllib`; it does not patch the ASLRef parser, typechecker, interpreter,
+or standard library.
+
+```text
+parse and typecheck the specialized PTO specification
+  -> initialize the interpreter environment
+  -> enter the static worker ASL wrapper
+  -> ResetProfileState() exactly once
+  -> enter HostReadCommand()
+       pristine parent: accept request, fork, wait/reap; never return to ASL
+       case child: receive one case, execute one ELF, report, then _exit
+```
+
+The fork gate belongs in a small C stub called by the model-owned host
+primitive. Keeping the parent inside that stub avoids allocating protocol
+objects in the parent OCaml heap and minimizes copy-on-write dirtiness.
+
+## Isolation and identity
+
+Each case child owns all architectural and hosted mutations for exactly one
+run. A child is never reset and reused. A failed, timed-out, or crashed child is
+discarded; the next case forks from the unchanged parent snapshot.
+
+Workers are keyed by all state that can change behavior:
+
+- PTO tree and ASLRef commit;
+- worker executable and protocol version;
+- exact `memory_bytes` and `tile_elements` bounds;
+- runtime typecheck mode and static wrapper version.
+
+Profiles must not be coalesced into a larger bound because bounds affect
+observable access and fault behavior.
+
+## Transport
+
+The shared daemon uses framed Unix-domain `SOCK_STREAM` connections. The
+Python runner retains current ELF, sidecar, symbol, hash, and segment
+validation, opens the verified ELF once, and passes its read-only descriptor
+with `SCM_RIGHTS`. The pristine parent reads only a fixed fork header; the case
+child reads variable payload and ELF segments with `pread`.
+
+The request contains start, return, stop, stack, step, result, profile, segment,
+and ELF-hash data. The child initializes memory through PTO-owned ASL accessors,
+sets both captured return state and R10, then executes only
+`ExecuteNextPTOInstruction()` until the stop policy terminates.
+
+## Platform requirements
+
+Darwin workers must be linked with a 512 MiB `LC_MAIN` stack
+(`-Wl,-stack_size,0x20000000`). Raising shell stack limits alone is not
+sufficient. Linux launchers must set the corresponding stack resource limit.
+
+## Promotion gates
+
+The process backend remains the default until the snapshot backend proves:
+
+1. one cold parent reaches the post-reset fork gate;
+2. good–failing–good cases demonstrate pristine isolation;
+3. one ELF matches the process backend and independent golden byte-for-byte;
+4. eight same-profile children run concurrently without cross-talk;
+5. the 124 scalar GTests pass with cold, fork, case, recycle, and memory data;
+6. every exact profile required by the 341-case corpus passes;
+7. crash, timeout, busy, stale-socket, and parent-restart paths pass;
+8. two consecutive complete green runs are reproducible.