Yichus

Guide

Explorer

Explorer queries over typed Matchless IR

Explorer statically analyzes compiled Bosatsu. Bosatsu checks recursion for termination; external implementations and the host IO runtime remain trust boundaries. Explorer walks typed Matchless IR (the compiled form) and exposes bindings, IO sites, dependencies, reads, and argument influence as a queryable graph. It does not execute the target program or infer facts from source text.

Code & run Run the two order functions

Yichus is the analysis and tooling layer built on top of Bosatsu. Explorer is its main investigation surface. Start in the browser playground, use the same tools from the CLI, or write a Bosatsu program that does the investigation for you. The setup guide covers the local build, and the Explorer reference defines the command and result vocabulary used here.

1

Literal-root and return-data signals distinguish two dataflows

A well-typed output can still come from a constant rather than a state read. Explorer reports that structural difference without assigning a product-level judgment: one binding has a return-data path from a read, while the other has a literal-root and no upstream read.

State read with return-data provenance

counter: IO[State[Int]] = state(0)

def read_counter() -> IO[Int]:
  c <- counter.flat_map()
  read(c)

current: IO[Int] = read_counter()

This card is an explanation of the return-data signal, not a captured Explorer payload.

return-data: the compiled model contains a potential data path from a state read to the output.

Constant with literal-root provenance

fabricatedTotal = 42

response = fabricatedTotal

This card is an explanation of the literal-root signal, not a captured Explorer payload.

literal-root: the output comes entirely from hardcoded constants.

Both bindings produce a value, but only the left example is structurally connected to a state read. The overview command below returns the relevant per-binding signals; use the traces in the next section when you need the full upstream path. 

yichus explore --overview Demo/ExplorerPlayground/SuspiciousFabrication --overlay signals \
  demos/explorer-playground/suspicious-fabrication.bosatsu
Or open the playground, pick the constant-derived sample backed by suspicious-fabrication.bosatsu, and click Analyze.

Continue to the trace section for the dependency edges behind those summary signals.

2

Trace upstream dependencies from an output binding

A trace follows upstream dependencies from an output binding through typed IR nodes. Each node reports its role, signal tags, reads, and argument influence. Compare the two commands below, then use the trace-flow reference when you need exact influence-label semantics.

Trace with a state-read dependency

yichus explore \
  --trace Demo/ExplorerPlayground/TrustworthyCounter/current \
  demos/explorer-playground/trustworthy-counter.bosatsu

current traces back through read → counter → state(0). This is a static dependency path involving a state read, not a recording of values observed during execution.

Trace with only a constant dependency

yichus explore \
  --trace Demo/ExplorerPlayground/SuspiciousFabrication/response \
  demos/explorer-playground/suspicious-fabrication.bosatsu

response ends at the fabricatedTotal constant binding shown above. Inspect the trace for its literal origin and the absence of a state-read dependency; the graph describes compiled structure, not an execution.

Each binding in the trace carries four pieces of structural evidence:

Role
What the binding does: terminal-io (observable output), state-init (creates a state cell), intermediate-io (reads and feeds downstream), or pure (no IO).
Signal tags
Structural flags: dead-input (a read that never reaches the output), guard-only-arg (argument used only as a branch selector), literal-root (output from constants only).
Read provenance
For each state read: does it reach the output as return-data, only as a guard-only branch condition, or is it detached entirely?
Argument influence
For each function argument: does it flow through as data, or is it only used as a guard?
In the playground, click any binding in the graph to see its trace. In the CLI, add --trace-flow instead of --trace to get a flat edge list you can pipe into jq.

Use a query program when the same structural check must run across many bindings or targets.

3

Compile a structural check as a Bosatsu query

Interactive tools support exploration. A query program makes a known structural policy repeatable over the complete ProgramData value.

Query contract. Explorer compiles a Bosatsu function from ProgramData to ClassifyResult. The function can filter bindings, inspect structural facts, and return a label plus evidence. Explorer supplies facts; the query author defines the policy.

Query that classifies upstream derivation

package MyCheck

from Yichus/Explorer/Query import (
  ClassifyResult, ProgramData,
  classify_result, has_any_io,
  terminal_io_without_deps,
  bindings_with_signal,
)

def classify(data: ProgramData) -> ClassifyResult:
  match has_any_io(data):
    case False:
      classify_result("pure-computation",
        ["pure computation, no IO"])
    case True:
      no_deps = terminal_io_without_deps(data)
      match no_deps:
        case [_, *_]:
          classify_result("no-upstream-derivation",
            ["output has no upstream derivation"])
        case []:
          dead = bindings_with_signal(data, "dead-input")
          match dead:
            case [_, *_]:
              classify_result("dead-input-detected",
                ["reads that never reach the output"])
            case []:
              classify_result("upstream-derivation-present",
                ["real upstream derivation"])

This program checks three things: is there IO? Does any output lack upstream dependencies? Are there dead inputs? It runs against the full binding graph and returns a structured answer.

Run the query against two targets

yichus explore --query my-check.bosatsu \
  demos/explorer-playground/suspicious-fabrication.bosatsu

# classification: "no-upstream-derivation"
# evidence: ["output has no upstream derivation"]
yichus explore --query my-check.bosatsu \
  demos/explorer-playground/trustworthy-counter.bosatsu

# classification: "upstream-derivation-present"
# evidence: ["real upstream derivation"]

BindingEntry fields available to a query

Each BindingEntry in the program data carries:

  • Role, signal tags, dependency count, literal count
  • reads: List[ReadEntry], per-read provenance with influence kind
  • arguments: List[ArgEntry], per-argument data flow info
  • dependencies: List[DependencyEdge], edges to other bindings this one depends on, with targetBindingId and edgeKind
  • hasBranchEquivalence, the analyzer’s compiled branch-equivalence flag

The simple program above uses summary checks. When you need more precision, inspect individual reads, arguments, or follow the dependency graph: 

# Does any read actually reach the output as data?
has_return_data_read(entry)

# Follow dependency edges to another binding
deps = get_dependencies(entry)
any_dep(deps, dep -> str_eq(get_dep_target(dep), "MyPkg/counter"))

# Find a binding by id and inspect it
match find_binding(data, "MyPkg/counter"):
  case Some(dep_entry): has_return_data_read(dep_entry)
  case None: False

Graph traversal: follow dependencies transitively

Because each binding carries its dependency edges, you can write programs that walk the graph instead of only inspecting individual nodes. This query checks whether every terminal-io output has a transitive path back to a real state read: 

def step_one(data: ProgramData, work: List[String], visited: List[String])
    -> (List[String], List[String], Bool):
  match work:
    case []: ([], visited, False)
    case [id, *rest]:
      # ... check if id has a return-data read, or expand its deps
      match find_binding(data, id):
        case Some(entry):
          match has_return_data_read(entry):
            case True: ([], visited, True)  # found real data!
            case False:
              # Add dependency targets to work list
              new_work = get_dependencies(entry).foldl_List(rest, ...)
              (new_work, [id, *visited], False)

def traverse(data, work, visited, fuel):
  recur fuel:
    case []: False
    case [_, *remaining]:
      (next, vis, found) = step_one(data, work, visited)
      match found:
        case True: True
        case False: traverse(data, next, vis, remaining)

The recur fuel: pattern consumes a fuel list, so the compiler can check that this recursion terminates while allowing multi-hop traversal. Open the full working eval/queries/graph-traversal.bosatsu query.

Explorer reports facts; the query defines policy. Explorer gives you structural observations: signal tags, read provenance, argument influence. What those facts mean for your product is your decision, expressed as a Bosatsu program. The program above uses objective property labels; you can write a different one that checks different things, uses different thresholds, or maps the same properties to product-specific conclusions. Reference queries ship in eval/queries/. Read them, modify them, or write your own from scratch.
Reuse boundary. A saved query applies the same explicit classification logic to each target. MCP is the tool protocol the CLI, browser, and Node engines speak. The MCP operation names include explorer_overview, explorer_trace, and explorer_connections; a query replaces a fixed manual sequence with one explicit program without claiming a universal call count. Review the shipped query directory for complete programs and use the query reference for the input fields and invocation forms.
The entry point defaults to classify but you can use any name with --entry-point check_permissions on the CLI or the entryPoint parameter in MCP. In the playground, paste the query source, select a target, and run it.
Permission example: the generic query above checks derivation structure, but it will not automatically catch a permission gate bypass. For the fictional permission leak demo, run eval/queries/perm-gate-check.bosatsu against demos/explorer-playground/permission-leak-demo.bosatsu. That query is anchored to this demo's secret_cell and can_see_secret bindings, walks the dependency graph, and checks that secret-returning exports still flow through the gate. To reuse it on another program, update the gate_binding and secret_binding constants at the top of the query.

The command table below maps other graph questions to their Explorer operations.

4

Explorer operations and their graph questions

Explorer has eight tools. Each answers a different question about the program graph.

When you want to… Use CLI
Get a high-level picture overview --overview
Navigate the binding graph explore --path --depth
See what feeds or depends on a binding connections --connections
Find bindings matching a pattern search --search
Understand how two bindings relate path --path-from <from> --path-to <to>
See the full upstream tree with provenance trace --trace
Get raw edges for scripting trace_flow --trace-flow
Automate the entire investigation query --query

Browser, CLI, and MCP surfaces

All eight tools are available from three surfaces. The browser playground compiles Bosatsu in the browser and renders the graph visually. The CLI (yichus explore) produces JSON you can pipe to jq or scripts, which suits automation. The MCP server (yichus mcp my-program.bosatsu) exposes all eight tools over the MCP protocol so agents can call the corresponding ExplorerWorkspace operation contracts. See the reference for each surface's invocation and output shape.

Overview, trace, and query sequence

# 1. Start with the big picture
yichus explore --overview Demo/ExplorerPlayground/MixedTrust \
  demos/explorer-playground/mixed-trust.bosatsu

# 2. Spot something suspicious — drill in
yichus explore --trace Demo/.../MixedTrust/reviewSummary \
  demos/explorer-playground/mixed-trust.bosatsu

# 3. Compare with a trustworthy binding
yichus explore --trace Demo/.../MixedTrust/readScore \
  demos/explorer-playground/mixed-trust.bosatsu

# 4. Automate the check for next time
yichus explore --query my-check.bosatsu \
  demos/explorer-playground/mixed-trust.bosatsu

This example starts broad, inspects two bindings, then saves a repeatable query. Each operation is available in the playground, CLI, and MCP surface. Use the operation reference for flags and result shapes.

5

Run the six Explorer sample programs

Choose a surface based on the task. Browser: Open the playground, pick the state-read counter sample, click Analyze, then switch to the constant-derived sample and compare. CLI: Run the two commands below, then drill with --trace into the binding that catches your eye. Query: Copy the program from the query section, save it as my-check.bosatsu, and run it with --query against any Bosatsu file. 

yichus explore --overview Demo/ExplorerPlayground/TrustworthyCounter \
  demos/explorer-playground/trustworthy-counter.bosatsu

yichus explore --overview Demo/ExplorerPlayground/SuspiciousFabrication --overlay signals \
  demos/explorer-playground/suspicious-fabrication.bosatsu

Six samples live in demos/explorer-playground/. Each demonstrates a different pattern. The filenames below are literal repository identifiers retained for copyable commands; words inside a filename are not Explorer verdicts.

FileWhat it demonstrates
trustworthy-counter.bosatsu State reads whose values reach the output
suspicious-fabrication.bosatsu IO is declared while the output remains constant-derived
dead-inputs.bosatsu A state read that never reaches the output, a dead input
mixed-trust.bosatsu A state-read path alongside a constant summary binding
pure-computation.bosatsu No IO sites, only pure arithmetic
permission-leak-demo.bosatsu A secret reaches the export without flowing through the permission gate
Worked comparison: Load Mixed Trust. Compare readScore and reviewSummary in the overview, then trace both. The first has a read dependency; the second is constant-derived. Return to the trace field definitions if an influence label is unclear.

Where this fits

What this is about: Fact Tooling

Do it

Measure it