Explore choices with constraints

Leave a musical choice open and ask Volta to find a value that meets the constraints you write.

Every checker is a solver run backwards. Where Refinements rejects a value that breaks a T | pred refinement, a hole (?name) asks the compiler to propose values (scalars) or patterns that satisfy it. The predicate is the author's taste, made checkable; the solver enumerates the satisfying region. A solved hole, once pinned, is literal source like anything hand-written — delete the solver and every pinned song still compiles identically.

Studio's Propose/Reroll controls run the same Rust search on a background worker in desktop and browser builds. Browser requests use the existing compiler Worker; no server or native-only library is needed. Editing source or imports invalidates a pending page, and old candidates are cleared before replacement search. Candidates retain their seed, scores and audition notes; pinning still writes ordinary editable source.

1. Surface#

A hole is ?ident — named, always (? alone is a lex error; the name keys the seed, the pin, and the diagnostics). It is an ordinary expression that takes the type of its position:

-- a scalar hole inside a field expression
cutoff = const 500Hz + ?depth            -- | 800Hz <= x <= 4000Hz

-- a whole binding as a pattern goal
bassPat : Pattern Pitch
  | inScale key and density 0.4 and offGrid kickPat
  = ?bass

The conjunction operator is and (the shipped refinement conjunction; the design doc's & is aspirational and does not lex). A duplicate hole name in one module is a compile error.

Unsolved-hole semantics (the live-coding invariant). An open hole never stops the audio or fails the build: a scalar hole lowers to a neutral Const 0, a pattern hole to silence, each with a warn-level Hole diagnostic listing its goals. In a refined field the neutral default is still checked against the refinement, so an open scalar hole there can also carry a Refinement error-level diagnostic naming the default (cutoff = const 500Hz + ?depth under 800Hz <= x reports the computed 500); the module still lowers and plays. Under @strict "on"|"module" an open hole fails the compile — strict means "pin a satisfying value" — via the same enforce_strict dial refinements use.

2. Stage 2/3 — scalar inversion#

For a scalar hole inside a refined patch field, the compiler linearises the field root's interval endpoints as an affine function of the hole value d (lo = lo_c + lo_k·d, hi = hi_c + hi_k·d — the forward interval engine run symbolically), translates each obligation conjunct into a bound on d, and intersects them into the satisfying interval.

• Endpoint targeting. A plain x <= B bounds the field's hi; x >= A its lo. peak x / floor x name the endpoints explicitly (Interval::hi / lo), so a point-target ("the filter opens to ~4k") is expressible alongside range-containment. peak/floor are refinement-only selectors — they strip to their argument for type-checking.
• Pin policy. A two-sided interval pins to its midpoint — log-midpoint for Hz (Hz interpolates in log space). A one-sided / relation interval pins to a margin inside the finite bound (⅔ from the open end), never the degenerate boundary — Explore choices with constraints §4's witness-as-fix (Stage 3).
• Not invertible. A non-monotone step (a multiplier interval spanning zero, a hole under a denominator, an opaque node kind) marks the goal advisory: the card offers a free scrub instead of a bounded one.

An unpublished base still solves. A hole's owner is the top-level binding whose declaration holds it. When that binding is only consumed as an operand (bass2 = bass with {…}, morph bass other t, a knob-sugar lift) the publish rule (Voice signal flow § "An operand is not an instrument") drops it from module.synths, but annotate_holes still solves against the dropped graph, so the card reads the same interval as when bass is played. A hole inlined into several synths is joined to the copy lowered into its owner.

The workbench renders a hole card: the satisfying interval, the goals, and a scrub knob bounded to the interval; pinning splices the literal (3354Hz) at the hole's span.

3. Stage 4 — the pattern predicate vocabulary (forward)#

Checkable refinements over hand-written patterns (a pattern flattens to a finite event vector, so every predicate is decidable at compile time). Each is a warn-with-witness on violation and the same function the search scores with.

Numeric-target tolerance: ±0.1 on fractions (density, syncopation), exact on counts (onsets). Diagnostic kind PatternRefinement.

The vocabulary continues in Interweaving melodies: melodic-shape rules (stepwise, leapRecovery, singlePeak, noRepeats, outlines, beginOn/endOn), relational rules against a sibling voice (intervalsWith, consonantOn, noParallels, contrary, noCross, maxSpread, …), the soft-goal prefer marker, and the species N cantus bundles. All ride this same obligation/verdict machinery.

4. Stage 5 — pattern holes: the seeded search#

For a pattern hole, solve_hole(src, sources, hole, seed, budget) (a wasm entry beside compile, and a Rust API) runs a seeded generate-and-test:

1. Generate. A small inventory — euclidean skeletons, random subsets, rwalk over scale degrees, and mutation of the nearest sibling pattern — each a pure function of (seed, index) (splitmix64, the repo's deterministic substrate).
2. Score. The Stage-4 predicates: hard predicates filter (a candidate breaking inScale is discarded), numeric targets rank by distance.
3. Return top-5 as Candidate { sourceText, scores, rank, generator, seed }, sorted (rank, sourceText) for a stable page.

Determinism is a hard guarantee. The search seed is hash(module seed, hole name, reroll); same (source, hole, seed, budget) ⇒ byte-identical candidates (pinned in compiler/tests/constraint_holes.rs). The reroll counter is workbench state — bump for a new page. Candidate cards render the mini-notation, audition it through the existing preview seam (previewSnippet — the candidate plays through a generic saw voice, the cheapest honest audition), and offer pin / reroll. Pinning splices the mini-notation (a minimal private emitter, solve/mini_print.rs — flat tokens, [..] subdivision, =vel; the general serializer lives on another branch) as a !"…" literal, optionally with a -- solved: seed N, generator provenance comment.

The CLI surface#

volta <song.volta> runs the same search for every OPEN pattern hole after lowering and prints the top-k proposals under the hole's warning, in the form a pin splices:

proposals for `?bass` (line 44, col 5):
  [1] !"~ c4 a3 ~ ~ f#3 ~ g3"
  [2] !"~ c4 e4 ~ ~ ~ ~ f#4"
  …
  pin one with: volta pin <file.volta> bass [1..5]

volta pin <file.volta> <hole> [index] (1-based, default 1) splices proposal index in place and writes the file back — byte-identical to the workbench's holes::pin_candidate, provenance comment included, so a CLI pin and a workbench pin of the same page are the same edit. --json carries the same page on holes[].candidates (absent when empty, so pre-existing IR round-trips unchanged). lower() itself never runs the search: it is a separate budgeted pass, so a module with no open pattern hole pays nothing. Determinism is the search's own contract (seed 0 is the first page), so the terminal and the panel cannot disagree. See production-gaps.md §31 AD2.

4a. The workbench surface#

The hole-cards panel is part of the Rust workbench: it mounts in the macro strip (ui/src/app/macrostrip.rs::macro_strip) and auto-appears whenever the compiled ModuleInfo carries open holes. Desktop and browser run the same crate, so there is one surface, not two. Because the compiler is a direct volta-ui dependency (feature intel), there is no seam translation — volta_compiler::solve::{solve_hole, format_pin} and Module.holes are called in-process. (The TypeScript hole-cards.ts panel was deleted with the TypeScript workbench on 2026-08-09; see git history.)

• Data layer — ui/src/holes.rs holds the card view-models (ScalarCard / PatternCard), clamp_scrub, a pure format_pin (a unit test pins byte-parity with the compiler's), and the span-verified pin_literal / pin_scalar / pin_candidate (-- solved: seed N, <gen> provenance). ui/src/moduleinfo.rs parses Module.holes into HoleInfo / HoleSolutionInfo.
• Scalar card — goals + satisfying interval + a slider bounded to the interval (log-scaled for Hz), and a pin chip → the editor's span-verified, undoable editor.splice → recompile. Scrub is display-only until pinned: a scalar hole lowers to a Const, not a live macro, so there is no zero-recompile preview seam. This is a recorded scope cut.
• Pattern card — propose / reroll build a solver::Query (ui/src/solver.rs) and poll the bridge's solve_poll; the native bridge runs the search on its bounded background solver::Worker with the cached import sources, never in the UI frame. Then come the top candidates, each with an audition ▶ and a pin (mini-notation + seed provenance, applied via the editor's undoable whole-buffer edit so the trailing comment splices too).
• Audition — the engine has no snippet-preview module, so a candidate auditions as a stepped sequence of one-shot preview_triggers (engine/src/preview.rs, UiCommand::Audition) over two cycles on a real synth from the module; the bridge flattens the candidate's mini-notation into the audition events. Determinism is passed through untouched (reroll = seed+1).

Tests: ui/src/holes.rs unit tests (view-models + format_pin parity + the span-verified pins), ui/tests/constraint_holes.rs (kittest: the cards appear, a scalar pin splices the buffer, propose populates candidates, a pattern pin splices the mini-notation + provenance). Screenshot fixture: examples/songs/constraintholes-open.volta (the shipped song with ?depth + ?bass reopened — the pattern binding left unreferenced to sidestep the play-a-pattern-hole lowering gap). Design: Explore choices with constraints "Native port plan".

5. The pin contract#

Pinning is the only mutation a hole makes, and it is a pure text splice:

• Span-verified. Before replacing, the workbench (ui/src/holes.rs) asserts the hole's span reads exactly ?name; a stale span (edited buffer) is refused, never clobbered — recompile first.
• A pinned hole is just source. The literal (a number + unit for a scalar, a !"…" for a pattern) is indistinguishable from hand-written code. Playback, export, import, and the native engine never learn the solver existed.
• Invariant 1 (no drift). The search scores with the same membership functions the forward checker uses, so a pinned candidate always re-passes the Stage-4 checker.

6. Where it lives#

7. Not yet#

• Stage 6 — harmony holes: SHIPPED via Interweaving melodies §8 — the roman functional-harmony walk generates progressions (pins are numeral text, mode-derived qualities), and the CSP generator handles counterpoint-shaped goals (Interweaving melodies §6). The per-note voicing CSP shipped alongside it as the voiceLines n combinator (Stage 6b). See Interweaving melodies.
• Coupled holes (?a + ?b <= bound): pin one, solve the other. Needs a linear/SMT backend for scalars (Explore choices with constraints §9); the pattern case (joint multi-voice solve) is staged in Interweaving melodies §10.
• Rendered-property + mix-level goals, and a user-defined generator — harvested to Ideas when a song demands them.