Module debug 

The bytecode debugger bridge — drives the LOGOS VM one op at a time for the Studio debug drawer, with breakpoints, step-over / step-out, and time-travel (step backwards through executed ops). Single-task, bytecode tier (tier: None) so granularity is exactly one op and behaviour is identical to a normal run.

ZERO production cost: nothing here is on the execution path. The stepping rides the VM’s STEPPED = true monomorphization (the default run_until_block is byte-for-byte the old hot loop), and this whole module dead-strips from any binary that never constructs a Debugger.

Time-travel falls out of the architecture for free: the debugger owns the CompiledProgram and rebuilds a fresh VM each step from a saved state snapshot, so it keeps the full snapshot history — stepping back is just dropping the last snapshot.

Structs

AssertionResult

The result of asserting a predicate at the cursor — the dual lens the debugger is built for: what is true now (concrete, from live values) and what is proven for every run (from the Oracle’s static facts, kernel-style interval entailment, no Z3). now is None when a term has no live integer value; the verdict is Unknown when a term has no proven range.

CausalNode

A node in a causal provenance tree — the exact op that produced a value, and (recursively) the ops that produced its inputs. Because execution is deterministic and fully recorded, this lineage is exact, not heuristic: the answer to “why is this value here?” with no guessing.

DebugFrame

One call frame’s registers. function is None for Main; base is the frame’s start address in the linear register file (its stack base), for the Stack view.

DebugReg

One register in a DebugFrame. name is the source variable when known (filled by the compiler’s debug-info pass; None ⇒ show R{index}).

DebugSnapshot

A complete picture of the paused VM for the debug drawer (serde for the UI).

Debugger

A self-contained stepping debugger over one compiled program.

HeapObject

One heap object for the Heap view: a list / map / set / struct / text reachable from a variable or global. referenced_by lists every root that points at it, so shared (more than one) makes aliasing visible — the thing assembly debuggers can’t show because they only have raw bytes, not typed objects.

ProvenFacts

A variable’s program-wide proven facts (from the Oracle’s static abstract interpretation): a finite integer range, non-negativity, a concrete scalar type. Every field is a sound guarantee that holds on every run — the static companion to VarInsight’s observed-this-run facts.

ProvenInsight

One variable’s proven invariants, pre-rendered for the UI (mirrors VarInsight).

TimelinePoint

One sample on a VarTrace: the variable’s display value at a single step, and whether it just changed (the waveform “edge”).

VarInsight

One variable’s observed invariants — facts that held over the recorded run (constant, monotonic, range, distinct count). Dynamic likely-invariants, labelled as observed (not proven), the empirical companion to the Oracle’s static facts.

VarTimeline

A logic-analyzer view of the run: every Main-frame variable’s value across the recorded history, with a playhead at the time-travel cursor. Deterministic replay makes this exact — it is the program’s entire observable past, not a sample.

VarTrace

One variable’s value over the whole recorded execution — a trace on the VarTimeline oscilloscope. points[i] is the value at explored step timeline.start + i.

Enums

ProofVerdict

The verdict of a live proof at a breakpoint — whether a predicate is statically guaranteed across every run (ProvenTrue), statically refuted (ProvenFalse), or undecided from the proven facts (Unknown, where only the concrete check speaks).