TI-BASIC dynamic tracing

TI-BASIC coverage combines exhaustive local models, natural calculator traces, and provenance-labeled probes. The models classify bounded decisions. Natural traces establish program reachability. Probes distinguish remaining outcomes without presenting prepared state as a natural language path. None of these layers is whole-interpreter coverage.

Evidence layers

tools/ti84re/tibasic/analyze_coverage.py refuses a ROM whose SHA-256 differs from the pinned OS 2.55MP image, then verifies short byte signatures at every modeled decision family. [confirmed]

Exhaustive finite models

The checked report exhausts 591,360 states and 45 semantic outcomes:

The block model uses token equivalence classes because the ROM performs the same comparisons for every non-control byte. It still enumerates all 65,536 values of the 16-bit DE depth, including the zero and increment-wrap boundaries. This is exhaustive over the stated local transition, not a depth limit of 255.

Z3 minimizes one representative per semantic outcome after exhaustive enumeration establishes the partition. Z3 is not being presented as a proof of the entire Z80 routine or of arbitrary token streams.

Coverage by provenance

The report declares 26 branch sites and both outcomes at each site. Natural programs reach 38 of those 52 outcomes. Public-bcall probes add the four page-33 bounds outcomes. Internal-entry probes add the remaining 10 outcomes. The union reaches 52 of 52, but only the first number describes natural TI-BASIC reachability. [confirmed]

flowchart LR
    N["Natural TI-BASIC<br/>38 / 52 outcomes"] --> U["Declared outcome union<br/>52 / 52"]
    B["Public bcall probes<br/>4 additional outcomes"] --> U
    I["Internal-entry probes<br/>10 additional outcomes"] --> U
    F["Eight finite models<br/>591,360 states"] --> R["Compact report"]
    U --> R
    R --> Z["Exact Z3 set cover<br/>15 outcome traces"]

The per-provenance counts in the JSON are 38, 8, and 18 because wrappers share ordinary grammar outcomes. Those counts overlap. The additional-outcome counts in the diagram describe what each probe layer contributes after the preceding layer. No successor at a declared branch is unclassified. [confirmed]

That 52-outcome matrix is a regression test for eight local models. It is not the interpreter denominator. The broader CFG audit seeds all valid destinations from grammar_handler_table (38:4000) and the 13-entry ctrlflow_handler_table (33:4381), then follows direct control flow through five bounded components. [confirmed]

Expanded CFG saturation

The expanded graph contains 8,490 reachable instructions and 1,351 conditional branches. Its 2,702 possible outcomes produce this trace breakdown:

Natural factorial and dfs traces identify the page-38 loop path: For( reaches parse_for_production (38:41E5), End reaches parse_end_ops_record (38:4200), and the loop continuations are for_first_update (38:5836) and for_steady_update (38:587D). They do not enter the page-33 probe dispatcher. [confirmed]

flowchart LR
    T["81 parser handlers<br/>plus subsystem entries"] --> G["8,490-instruction<br/>direct CFG"]
    G --> B["2,702 outcomes"]
    N["Natural programs"] --> O["898 observed"]
    P["ABI and entry probes"] --> A["924 observed total"]
    O --> A
    B --> A
    B --> U["1,778 unobserved"]

The exact outcome cover retains 30 of 33 traces. hello, callstop, and the natural syntax-error trace remain useful semantic examples, but they do not add a branch outcome to the larger graph. The report therefore separates the minimum outcome corpus from the selective documentation corpus. [confirmed]

Natural programs

Seven successful fixtures cover distinct interpreter behaviors:

missingend and terminalif add natural end-of-input structural boundaries. They exercise carry returns that closed blocks do not reach, then finish through page-38 cleanup and display Done; they do not raise an OS error. The report marks both traces with termination: completed. [confirmed]

The syntax and divide-by-zero fixtures provide baseline unwind witnesses. syntaxerr executes Disp 1+ and reaches the syntax entry at 00:2700. divzero executes Disp 1/0 and reaches _ErrDivBy0 at 00:26EC. The expanded numeric corpus raises the natural local-matrix result from 34 to 38 outcomes. The 15-trace outcome minimum omits the error fixtures because other traces cover those local branches; the semantic corpus retains their distinct causes. [confirmed]

Twelve selected numeric-error fixtures also retain the path before the shared error shim. The reducer restarts a candidate slice whenever it sees the guard’s first instruction. It accepts the slice only when the remaining guard and shim addresses occur in order and the shim leaves the expected error code in A. This prevents an unrelated earlier call to _FPDiv, _FPMult, or the zero checker from being attached to a later error. [confirmed]

All 12 paths come from stored TI-BASIC programs. They cover all six numeric error codes, 12 causes, and 11 distinct direct caller sites. [confirmed]

The report separately inventories 114 whole-ROM direct-reference candidates: 9 overflow, 2 divide-by-zero, 3 singular-matrix, 91 domain, 6 increment, and 3 non-real. Linear disassembly can decode data as instructions, so each candidate still needs CFG or dynamic reachability evidence. Indirect transfers and helpers that load A before entering 00:270A remain outside that inventory. [confirmed]

Probe outcomes

Three public-bcall probes call grf_435f = 5140h with an input below the table, inside the table, and at its upper boundary. They cover both outcomes at 33:436D and 33:4372. These are public ABI executions, not stored-program loop transitions. [confirmed]

Eight internal-entry probes cover four command-finalization classes and four grammar states. They map the required ROM page, enter the selected routine from RAM, and let the exact ROM execute the branch. cmdbad combines the safe implicit-end case with the invalid class, which removes one redundant trace. These probes establish branch behavior only; they do not establish a natural caller or a supported interface. [confirmed]

Across all 33 traces, the saturation report records 132,634,495 instructions. The raw files total about 6.08 GiB. Only SHA-256 digests, counts, outcomes, provenance, and the 47 KB report are checked in. Exact outcome-only set cover retains 30 traces. The three omitted traces remain useful semantic examples. [confirmed]

Reproduce the report

Generate the source/token/link fixtures first:

python3 -m ti84re.tibasic.samples --write-dir tools/tibasic-samples

The TilEm binary must support loading command-line .8xp files before the macro starts. Run the natural cases while retaining their temporary traces:

TILEM=/path/to/patched/tilem2
python3 -m ti84re.tibasic.smoke \
  --tilem "$TILEM" --rom tools/rom.bin \
  --out-dir /tmp/tibasic-coverage --keep-trace \
  --case hello --case factorial --case data \
  --case dfs --case callabi --case callstop \
  --case branchmatrix --case missingend --case terminalif \
  --case syntaxerr --case divzero \
  --case overflow --case muloverflow --case lndomain --case increment \
  --case asindomain --case acosdomain --case sqrtnonreal --case singular \
  --case lateincrement --case negfactdomain --case ncrdomain

Run the probe cases in the same output directory:

python3 -m ti84re.tibasic.smoke \
  --tilem "$TILEM" --rom tools/rom.bin \
  --out-dir /tmp/tibasic-coverage --keep-trace \
  --case cflowlow --case cflowhigh --case cflowvalid \
  --case cmdclose --case cmdopen --case cmdunit --case cmdbad \
  --case gramlow --case gramhigh --case gramflag --case gramnonzero

The natural branch matrix uses a RAM marker instead of an image crop. The probe cases use resolved trace anchors. Existing user-facing samples retain LCD oracles where the displayed result is part of the behavior.

Build the compact report through the Nix shell so z80dasm and Z3 are pinned. The checked command passes all 33 LABEL=PATH pairs; the complete ordered label list is the dynamic.traces array in tools/oracles/tibasic/tibasic-coverage.json.

set --
for label in \
  hello factorial data dfs callabi callstop \
  branchmatrix missingend terminalif syntaxerr divzero \
  overflow muloverflow lndomain increment \
  asindomain acosdomain sqrtnonreal singular \
  lateincrement negfactdomain ncrdomain \
  cflowlow cflowhigh cflowvalid \
  cmdclose cmdopen cmdunit cmdbad \
  gramlow gramhigh gramflag gramnonzero
do
  set -- "$@" --trace "$label=/tmp/tibasic-coverage/$label.trace"
done
nix develop -c python3 -m ti84re.tibasic.analyze_coverage "$@" \
  --output tools/oracles/tibasic/tibasic-coverage.json

Export exact instruction boundaries from the rebuilt Ghidra database, then reuse the same trace arguments for the expanded report:

ghidra-analyzeHeadless "$PWD" ti84 \
  -process ti84_page00.bin -noanalysis -readOnly \
  -scriptPath "$PWD/tools/ghidra" \
  -postScript ExportTiBasicInstructionStarts.java \
  /tmp/tibasic-instruction-starts.tsv

nix develop -c python3 -m ti84re.tibasic.analyze_saturation \
  --instruction-list /tmp/tibasic-instruction-starts.tsv \
  "$@" --output tools/oracles/tibasic/tibasic-saturation.json

Capture and reduce the selected numeric-error paths separately. This keeps their semantic provenance without adding redundant traces to the branch-only minimum corpus:

python3 -m ti84re.tibasic.smoke \
  --tilem "$TILEM" --rom tools/rom.bin \
  --out-dir /tmp/tibasic-numeric-errors --keep-trace \
  --case divzero --case overflow --case muloverflow \
  --case lndomain --case increment --case asindomain \
  --case acosdomain --case sqrtnonreal --case singular \
  --case lateincrement --case negfactdomain --case ncrdomain

nix develop -c env PYTHONPATH=tools \
  python3 -m ti84re.tibasic.analyze_numeric_errors \
  --trace divzero=/tmp/tibasic-numeric-errors/divzero.trace \
  --trace overflow=/tmp/tibasic-numeric-errors/overflow.trace \
  --trace muloverflow=/tmp/tibasic-numeric-errors/muloverflow.trace \
  --trace lndomain=/tmp/tibasic-numeric-errors/lndomain.trace \
  --trace increment=/tmp/tibasic-numeric-errors/increment.trace \
  --trace asindomain=/tmp/tibasic-numeric-errors/asindomain.trace \
  --trace acosdomain=/tmp/tibasic-numeric-errors/acosdomain.trace \
  --trace sqrtnonreal=/tmp/tibasic-numeric-errors/sqrtnonreal.trace \
  --trace singular=/tmp/tibasic-numeric-errors/singular.trace \
  --trace lateincrement=/tmp/tibasic-numeric-errors/lateincrement.trace \
  --trace negfactdomain=/tmp/tibasic-numeric-errors/negfactdomain.trace \
  --trace ncrdomain=/tmp/tibasic-numeric-errors/ncrdomain.trace \
  --output tools/oracles/tibasic/tibasic-numeric-errors.json

Delete the temporary traces after regeneration. They are reproducible evidence, not source assets.

Reading gaps honestly

Full coverage of the small matrix means both outcomes at 26 selected sites. The expanded report gives the more useful denominator: 924 of 2,702 outcomes across five declared components, with 898 reached naturally. Neither number means whole-interpreter coverage.

The graph expands all four declared computed jumps over their valid domains: 14 literal parser continuations at 38:4390, 27 nonzero destinations from the 49-class table used by 38:7244, five literal command targets at 02:5675, and 13 bounds-checked rows at 33:4380. This does not establish behavior for a corrupted class, stack, or pointer outside those domains. Other open dimensions include arbitrary token-stream length, every nested error context, full OPS/FPS record layout, arbitrary VAT and list shapes, floating-point path classes, and display or graph subsystem continuations.

The next useful coverage expansion starts with the unresolved caller census:

1. reject linear-disassembly candidates that are data or unreachable code;
2. backward-slice one remaining executable caller to its input predicate;
3. construct the smallest natural program and a RAM or value oracle;
4. retain its trace only when it adds a guard path or CFG outcome; and
5. update the relevant interpreter model with the established transition.

Lower-level trace formats and memory-write decoding are documented in tools/notes/dynamic-tracing.md.