Module examples 

Example files for the Studio playground.

These are seeded into the VFS on first launch to give users something to work with immediately.

Structs

ExampleSpec

One shipped Studio example: where it seeds in the VFS, its mode, its source text (the live const), and the outcome it is locked to.

Enums

Expected

The documented intended outcome an example is locked to. The test harness dispatches on this to the same pipeline the Studio uses for that mode.

Mode

Which Studio surface an example belongs to.

Constants

ALL_CODE_EXAMPLES

The 36 Code-mode examples. Output needles are provisional until the audit run confirms the real interpreter output.

ALL_HARDWARE_SPECS

The 18 Hardware-mode examples, sourced from the four hardware slices. The deliberately-unsafe demos (bad-arbiter, traffic-crash, queue-jam, register-alloc-spill) are locked to their intended failure/refutation.

ALL_LOGIC_EXAMPLES

The 11 Logic-mode examples.

ALL_MATH_EXAMPLES

The 24 Math-mode examples.

CODE_CRDT_COUNTERS

CODE_CRDT_TALLY

CODE_FIBONACCI

CODE_HELLO

HARDWARE_EXAMPLES

Seed only the advanced code examples (for existing installations). Always overwrites to ensure latest syntax is used. Hardware-mode examples: (filename, English spec). Each is a single English hardware specification that the Studio synthesizes to SystemVerilog Assertions and then certifies (in-browser, no Z3) against the spec. Pure spec sentences — the loader feeds the whole file to the synthesizer. The hardware_examples integration test verifies every one of these synthesizes, round-trips as certified-equivalent, and has a reachable trigger.

LOGIC_BARBER

LOGIC_LEIBNIZ

LOGIC_QUANTIFIERS

LOGIC_SIMPLE

MATH_AUTO

MATH_BOOL

MATH_GODEL_LITERATE

MATH_INCOMPLETENESS_LITERATE

MATH_NAT

MATH_PROP_LOGIC

PIGEONHOLE_EXAMPLES

Pigeonhole examples: pigeons: N → PHP(N), N pigeons into N-1 holes. Opened in Hardware mode; load_hardware_spec routes a pigeons: spec to the live solver, which animates the doomed pigeon and emits a certified symmetry-breaking refutation (Hall witness + Heule PR proof, no Z3) — the family every resolution-based solver (Kissat, CaDiCaL, Z3) needs 2^Ω(n) steps on.

REGALLOC_EXAMPLES

Register-allocation examples: a basic block’s variable live ranges + a register budget. Opened in Hardware mode; load_hardware_spec routes a registers: spec to the certified linear-scan allocator and renders the live-range timeline (coloured by register, spill clique flagged red).

RTL_EXAMPLES

RTL examples: (filename, Verilog). Synthesizable Verilog the Studio parses into a transition system and bounded-model-checks / k-induction-proves in the browser (no Z3). Verified by the hardware_examples integration test. Opened in Hardware mode (they live under /examples/hardware); load_hardware_spec routes module … endmodule content to the RTL BMC path.

Functions

seed_examples

Seed example files into the VFS if they don’t exist.