Change synthesis
Change synthesis evaluates transformations you declare, under constraints and
scenarios you declare, and retains the selected result as an ordinary
Patch Proposal. The command is bmo synthesize.
Maturity: Advanced and bounded. The command is registered on the public
CLI. It is not the default path for bmo or bmo run, and a selected
candidate is not applied, accepted, or treated as a completed parent goal.
This page does not describe general software synthesis or autonomous
decomposition.
A passing checker here is a measurement of the declared candidate. It is not a verdict grade, not mutation aftercare, and not a parent outcome. Those owners stay separate. Independent verification explains the boundary. The lifecycle, the penalty example, and the parent-check failure are on Decision-guided software synthesis.
What you supply
Section titled “What you supply”inspect, run, and the evaluation file for import-local read a JSON
specification. DecodeSpec rejects unknown fields, non-UTF-8 input, and
documents larger than 1 MiB.
The admitted request uses schema bmo-change-synthesis/v1 and policy
minimax_then_total_then_change. id and contract_ref are required.
contract_ref is provenance for the request. It does not admit a protected
workload or grant mutation authority.
| Field | Rule |
|---|---|
source_paths | Files captured for the evaluation. |
mutation_paths | Subset of source_paths. Only these paths may change. |
oracle_paths | Optional captured files outside the mutation set. Checker executables taken from the capture must live here. |
programs | Ordered operations. Allowed kinds are replace_file, replace_text, go_return_literal, go_import_add, and go_import_remove. |
candidates | Named sequences of those programs. The engine also measures an unchanged state. |
scenarios | At least one. The first scenario has no counterfactual inputs. Later scenarios may replace declared non-mutation files only. |
checks | Commands run in a fresh scenario directory. failure_loss is a penalty you declare for an observed failure. |
constraints / validators | Optional. A constraint block needs a versioned source. |
limits | Positive bounds. Source bytes stop at 16 MiB, a single file at 1 MiB, candidates at 32, one checker timeout at 120 seconds, and the run at 3600 seconds. |
The request must include one independent hard condition: a required check, a
versioned constraint source, or a blocking validator / required-coverage
validator. The text and Go AST backend reported with a run is
bmo-text-go-ast/v4. Other operation kinds are rejected as an unsupported
transformation backend.
Scenario environment values cannot replace PATH, HOME, or TMPDIR.
Commands
Section titled “Commands”bmo synthesize inspect /absolute/path/spec.jsonbmo synthesize limits --resource-profile economybmo --cwd /absolute/path/repository --data-dir /absolute/path/data \ synthesize run /absolute/path/spec.json --resource-profile economybmo --cwd /absolute/path/repository --data-dir /absolute/path/data \ synthesize compose /absolute/path/composition.jsonbmo --cwd /absolute/path/repository --data-dir /absolute/path/data \ synthesize import-local /absolute/path/evaluation.json \ --worker-dir /absolute/path/worker --producer LABEL| Command | What it does |
|---|---|
inspect | Validates the specification and prints its canonical SHA-256 digest and the parsed spec. It does not run checkers or open the proposal store. |
limits | Prints the effective synthesis resource ceilings and ablation digest. It does not read a spec, inspect a workspace, mint a grant, or run a checker. |
run | Captures declared source, runs declared checkers in scratch directories, and, when a candidate is selected, retains a Patch Proposal. --session-id attaches that proposal to an existing session. |
compose | Jointly qualifies selected files from accepted synthesis proposals. The inputs keep their own lifecycle. The combined proposal still needs its own acceptance. |
import-local | Captures an operator-selected worker directory and qualifies its bounded text changes. --worker-dir and --producer are required. The evaluation file must not contain programs or candidates. --producer is an attribution label, not an authenticated identity or a permission. --revision-of names a prior proposal to supersede only after the new qualification succeeds. |
run, compose, and import-local accept --resource-profile with
economy, balanced, or deep for that invocation. Empty means the
configured profile, which defaults to balanced.
How a candidate is chosen
Section titled “How a candidate is chosen”Hard eligibility comes first. A candidate that lacks complete hard-condition and risk evidence cannot be selected. Among eligible candidates, the order is observed worst-case loss, total loss, number of changed paths, then changed content bytes. The engine records which eligible states dominate others.
One eligible state becomes candidate_ready. The unchanged state, when it
wins, is reported as no_change and does not become a proposal. Distinct
states with equal coordinates stay unresolved: disposition
bounded_residual, reason equal measured risk and cost for distinct resultant states. No eligible candidate uses disposition bounded_residual
and reason no candidate has complete hard-condition and risk evidence.
Unknown or incomplete qualification is not promoted to an observed failure. The report keeps behavior outside the declared checks unknown.
Decision-guided selection
Section titled “Decision-guided selection”This ranking is decision-guided software synthesis in a narrow sense: you
declare failure_loss on each check, and the engine ranks eligible
candidates by the penalties those checks actually observed. A required check
must pass before a candidate is eligible. An optional check contributes its
declared penalty only when the failure is observed. A start failure, timeout,
cancellation, or a checker that changes captured inputs is unknown evidence.
Unknown evidence disqualifies the candidate. It is not stored as an ordinary
failure and it does not receive a penalty.
The comparison stays inside the candidates and scenarios in the specification. The command does not search an open program space or infer a repair you did not declare. The SIGNIN-204 recording on the proof gallery is a separate historical fixture. It is not this selection policy, and it is not evidence of general software synthesis.
ready_for_human is the status of the retained proposal. Workspace files are
still unchanged. The proposal is not accepted, not applied, and not a
verified parent result. The change becomes executable when you accept the
proposal and apply succeeds.
What a selection retains
Section titled “What a selection retains”Only candidate_ready creates a Patch Proposal. That proposal is
ready_for_human with validation status candidate_ready. Its summary says
that parent verification remains required. The proposal store keeps the spec,
the report, and the unified diff as artifacts, plus the spec, source, and
candidate digests on the selection event.
The operator then uses the ordinary proposal commands:
bmo --cwd /absolute/path/repository --data-dir /absolute/path/data \ workstream proposals accept PROPOSAL_IDbmo --cwd /absolute/path/repository --data-dir /absolute/path/data \ workstream proposals apply PROPOSAL_IDAccept records approval. Apply is the mutation. Apply checks the live
workspace against the measured preimage and checks the retained spec, report,
diff, and path set against each other. A digest mismatch, a changed retained
candidate, or a different path set refuses the apply. Applying a subset of
the measured paths, or combining this proposal with another, requires a new
joint qualification through compose.
import-local does not change primary workspace files. A held import returns
a command error and keeps the captured proposal for inspection.
Who finishes the task
Section titled “Who finishes the task”Apply writes the measured files, then mutation aftercare ingests the reserved effect into the session change contract. A successful ingest can still leave review obligations pending. Those obligations record that the path changed. They do not verify the parent goal.
Parent completion has a different owner from selection and from apply:
- On an ordinary session, parent validation obligations that were already on
the change contract stay pending. Inspect them with
/contract-obligations. Apply does not run them./contract-rerun, or thecontract_reruntool, asks the session change contract to run pending validation commands. Until that run, verification is pending and the task stays unresolved. A failed command marks that obligation failed. The task stays unresolved, and BMO does not undo the applied files or relabel the proposal. A later rerun does not invent a new attempt for an obligation that already failed. - On a provisioned controller, the owner is
bmo protected-admission decide-coordinator-outcome. Missing, failed, or unverifiable evidence is stored as a bounded residual and the command returns non-zero. The objective is not accepted while any residual remains. See Parent outcome. bmo synthesizedoes not call that decision. Signedprotected-admission run-synthesiscan retain repair evidence and still leaves parent completion to the obligation owner. A historical verification receipt on that path does not close the obligation. Failed or unknown verifier evidence leaves the applied repair actionable.
Independent verification separates these records from verdict grades, Quality Gate verdicts, work convergence, and auto-checkpoint.
Configuration
Section titled “Configuration”Resource ceilings are the only synthesis settings on this command. They are
documented with the other resource profiles in
Configuration.
options.resource_profiles.profile selects the envelope.
options.synthesis_resources overrides individual maxima. Zero inherits the
selected profile. It does not mean unlimited.
The App refuses an oversized request before it creates a run directory or starts a checker. A ceiling does not grant source capture, funding, mutation, or publication authority. Changing configuration does not rewrite a request that was already prepared under an earlier envelope.
Failure behavior
Section titled “Failure behavior”| Outcome | What you see |
|---|---|
| Invalid specification | The command returns the validation error. inspect and run do not execute checkers. |
| Resource ceiling refusal before a report exists | run prints synthesis refused: and a non-zero status. |
| Checker or preparation failure after a report file exists | JSON is still printed. The command returns synthesis retained at <report path>: and a non-zero status. The retained report disposition is bounded_residual. |
| No eligible candidate, or a tie | JSON disposition bounded_residual. run exits 0 because no execution error occurred. No proposal is created. |
unchanged wins | Disposition no_change. No proposal is created. |
compose conflict before a report exists | composition refused:. |
compose failure after a report exists | composition retained at <report path>:. |
Held import-local | local worker import <disposition>: and a non-zero status. |
Canceled or conflicting preparation still attempts to write report.json
under the run directory in the data directory’s change-synthesis folder.
Signed contracts are a different entry
Section titled “Signed contracts are a different entry”bmo protected-admission run-synthesis drives an already admitted root whose
signed desired-state contract may include synthesis_profile. That profile
is optional, grant-hashed metadata. An absent profile does not acquire
synthesis custody. automatic and native_repair_route (proposal_only or
apply) are signed declarations. A route declaration does not itself grant
mutation or start a native run.
The command contract for that path is in
CLI commands. It is
not a synonym for bmo synthesize run. Successful repair evidence on that
path still leaves parent completion to the task obligation owner.
Evidence and limitations
Section titled “Evidence and limitations”The behavior above is the command and App contract in
internal/cmd/synthesize.go, internal/app/change_synthesis.go,
internal/changesynthesis/spec.go, and internal/changesynthesis/run.go.
The bounded proposal lifecycle retains ready_for_human, refuses application
before acceptance, and permits a later check to fail without changing the
applied proposal’s validation status. That later check is outside
bmo synthesize. A parent validation stays pending through apply, then fails
or is satisfied only when the change-contract validation owner runs it.
The exact fixtures and their evidence limits are in the
maintainer evidence mapping.
Limits that follow from that contract:
- The synthesis diagram is a conceptual map. This command does not execute that map.
- Selection never grants live write authority.
- Declared checks do not establish properties they do not measure.
- Equal measured coordinates do not receive a semantic tie-break.
- A retained proposal is review material. Parent acceptance has its own command and its own evidence.
- Portable lowering, fidelity oracles, and joint checkers on signed managed
contracts are qualification machinery for that admitted path. They are not
implied by a successful
bmo synthesize run.