Configuration options


SymCC is configured at two different stages:

1. At compile time, you decide which features to enable, which mainly affects
   compilation time and the set of dependencies. This is done via arguments to
   CMake.

2. When you run programs that have been compiled with SymCC, the environment
   variables control various aspects of the execution and analysis.

We list all available options for each stage in turn.


                              Compile-time options


Each of these is passed to CMake with "-D" when configuring the build:

- QSYM_BACKEND=ON/OFF (default OFF): Compile either the QSYM backend or our
  simple Z3 wrapper (see docs/Backends.txt for details). Note that binaries
  produced by the SymCC compiler are backend-agnostic; you can use
  LD_LIBRARY_PATH to switch between backends per execution.

- TARGET_32BIT=ON/OFF (default OFF): Enable support for 32-bit compilation on
  64-bit hosts. This will essentially make the compiler switch "-m32" work as
  expected; see docs/32-bit.txt for details.

- LLVM_DIR/LLVM_32BIT_DIR (default empty): Hints for the build system to find
  LLVM if it's in a non-standard location.

- Z3_DIR/Z3_32BIT_DIR (default empty): Hints for the build system to find Z3 if
  it's in a non-standard location.

- Z3_TRUST_SYSTEM_VERSION (default OFF): Trust that the system provides a
  suitable version of Z3 if the corresponding CMake module can't be found. Use
  this with Linux distributions that don't package the CMake module but still
  ship an otherwise usable development setup (e.g., Fedora before F33). Note
  that we can't check the Z3 version for compatibility in this case, so prepare
  for compiler errors if the system-wide installation of Z3 is too old.


                                Run-time options


"Run time" refers to the time when you run programs compiled with SymCC, not
when you run SymCC itself. In other words, these are settings that you can
change on every execution of an instrumented program. They are specified via
environment variables.

- SYMCC_NO_SYMBOLIC_INPUT=0/1 (default 0): When set to 1, input is never marked
  as symbolic; in other words, instrumented programs will run just like their
  uninstrumented counterparts.

- SYMCC_OUTPUT_DIR (default "/tmp/output"): This is the directory where SymCC
  will store new inputs (QSYM backend only). If you prefer to handle them
  programmatically, make your program call symcc_set_test_case_handler; the
  handler will be called instead of the default handler each time the backend
  generates a new input.

- SYMCC_INPUT_FILE (default empty): When empty, SymCC treats data read from
  standard input as symbolic; when set to a file name, any data read from that
  file is considered symbolic. Ignored if SYMCC_NO_SYMBOLIC_INPUT is set to 1.

- SYMCC_MEMORY_INPUT=0/1 (default 0): When set to 1, expect the program under
  test to communicate symbolic inputs with one or more calls to
  symcc_make_symbolic. Can't be combined with SYMCC_INPUT_FILE. Ignored if
  SYMCC_NO_SYMBOLIC_INPUT is set to 1.

- SYMCC_LOG_FILE (default empty): When set to a file name, SymCC creates the
  file (or overwrites any existing file!) and uses it to log backend activity
  including solver output (simple backend only).

- SYMCC_ENABLE_LINEARIZATION=0/1 (default 0): Enable QSYM's basic-block pruning,
  a call-stack-aware strategy to reduce solver queries when executing code
  repeatedly (QSYM backend only). See the QSYM paper for details; highly
  recommended for fuzzing and enabled automatically by the fuzzing helper.

- SYMCC_FOCUS_BYTES=LO-HI (default empty): Restrict QSYM input symbolization to
  one inclusive byte range for one worker execution. This is used for coarse
  work splitting and remains disabled for exact prefix-target replay.

- SYMCC_FOCUS_SET=<path> and SYMCC_FOCUS_MARGIN=N (default 2): Restrict QSYM
  input symbolization to a sparse offset set plus a small byte-neighborhood.
  The file contains one offset per line. Bytes beyond the largest known offset
  remain symbolic to avoid losing unexplored suffix-dependent paths.

- SYMCC_COMPACT_FOCUS_SET=0/1 (default 1 in the MPI helper): Enable
  Gordian-style compact input linearization in the coordinator. Recent AFL hint
  offsets and Cottontail comparison-taint dependency offsets are written to a
  bounded `.compact_focus_set` file and dispatched as SYMCC_FOCUS_SET for
  ordinary non-targeted work. Targeted prefix replay and explicit focus
  partitions do not use the compact set.

- SYMCC_AFL_COVERAGE_MAP (default empty): When set to the file name of an
  AFL-style coverage map, load the map before executing the target program and
  use it to skip solver queries for paths that have already been covered (QSYM
  backend only). The map is updated in place, so beware of races when running
  multiple instances of SymCC! The fuzzing helper uses this to remember the
  state of exploration across multiple executions of the target program.
  Warning: This setting has a misleading name - while the format of the map
  follows (classic) AFL, the variable isn't meant to point at a map file that
  AFL uses too!

- SYMCC_TELEMETRY_OUT (default empty, QSYM backend): Atomically write a
  versioned JSON summary for one concolic execution. Schema 3 contains an
  ordered path fingerprint, branch/dependency counts, prefix-sensitive branch
  trace, solver outcomes and timings, generated-input counts, and optional data
  coverage features. It also reports bounded implicit-flow targets, Backsolver
  attempts, and successful adapted models. The MPI helper enables this
  automatically for adaptive scheduling and persists the resulting scheduling
  signal in the prefix DAG. Static-data fields are
  `static_data_regions`, `static_data_objects`, `static_data_segments`,
  `static_data_accesses`, `data_switches`, `data_switch_probes`, and
  `static_data_features`. Each static feature row is
  `[object_id, byte_offset, matched_bits, maximum_bits, kind]`, where kind 0 is
  a simple load, kind 1 is a predicate/load-based comparison, and kind 2 is a
  byte-region comparison.

- SYMCC_DATA_COVERAGE=0/1 (default 0 in the runtime, enabled by the MPI hybrid
  helper when adaptive scheduling is enabled): Enable structured Data Coverage
  for immediate integer comparisons, bounded switch neighbors, simple loads
  from static storage, load-derived predicates, and byte-region comparisons.
  Trivial branch outcomes remain represented by ordinary code coverage instead
  of being duplicated. Equality progress is the number of equal bits; ordered
  comparisons use the number of equal leading bits. Switch instrumentation
  sorts cases once and probes only the adjacent cases (or range endpoint).

  Constant globals compiled by SymCC are registered with deterministic
  module/global IDs. At startup the QSYM runtime also registers readable,
  non-writable ELF PT_LOAD segments from already loaded modules, so an
  instrumented caller can cover read-only tables in an uninstrumented DSO.
  Runtime addresses are normalized to ASLR-independent
  `(object_id, byte_offset, effective_width_bits)` feature keys. Fine-grained
  LLVM objects take precedence over their containing ELF segment.

  The adaptive coordinator stores comparison and static-data winners in the
  `data_coverage` section of its versioned scheduler state. This is an
  independent, collision-free novelty set; it is not overlaid on the AFL edge
  bitmap. A seed replaces another feature winner only after strictly improving
  matched bits. `data_corpus_refinements` is incremented only when both inputs
  have the same nonzero path fingerprint, a conservative proxy for equal code
  coverage. Replacement is logical scheduling dominance: AFL-owned queue files
  are not deleted, and a seed that remains best for another feature keeps its
  priority.

- SYMCC_DATA_CMP_BYTES=N (default 64, maximum 4096): Maximum bytes recorded for
  libc constant-data comparisons and region features. The runtime wrappers emit
  region progress for memcmp/bcmp and bounded strcmp/strncmp comparisons, then
  retain the existing symbolic-vs-concrete byte hints. A late, uninstrumented
  module loaded with dlopen after runtime initialization is not part of the ELF
  fallback registry unless its relevant objects are explicitly registered.

- SYMCC_CMP_TAINT=0/1 (default 1 when SYMCC_TELEMETRY_OUT is set): Emit
  Cottontail-style comparison-taint summaries in telemetry. Each bounded entry
  records a branch site, prefix-sensitive branch id, dependent input-byte count,
  min/max dependent byte offsets, taken outcome, and whether the branch was
  solver-interesting. The adaptive scheduler converts these summaries into a
  locality signal for structure-aware seed ranking and exports them to agentic
  planning hooks. Setting this option to 0 disables the JSON field without
  affecting ordinary solving.

- SYMCC_ECT=0/1 (default 1 in the adaptive coordinator): Maintain an
  engine-neutral expressive coverage tree from prefix-sensitive branch traces,
  comparison dependencies, compiler structural metadata, data progress, solver
  outcomes, and concrete coverage reward. Observed and open outcomes are
  separate nodes; source/function/context fields come from SYMCC_TASK_GRAPH.
  Constraint shapes intentionally omit absolute byte offsets so structurally
  equivalent parser states can share duplicate and rarity statistics.

- SYMCC_ECT_NODES=N (default 16384), SYMCC_ECT_TRACE=N (default 512), and
  SYMCC_ECT_CONTEXT=N (default 8): Bound retained ECT nodes, consumed trace
  length per execution, and function-context depth. Repeated site/outcome
  shapes are compressed into loop counters, and inactive low-quality nodes are
  pruned before active open/timeout nodes.

- SYMCC_ECT_OUT=PATH (default empty): Atomically export the persisted scheduler
  ECT as versioned JSON for offline analysis or an external planner. ECT
  priority is used internally even when no export path is configured.

- SYMCC_POLY_CACHE=PATH/0 (default off in the runtime, enabled by the adaptive
  MPI hybrid helper as "$AFL_OUT/<symcc-name>/.poly_cache"): Enable Pangolin-
  style context reuse in the QSYM backend. Each interesting branch stores a
  prefix-sensitive cache entry containing the SAT/UNSAT/timeout result, the
  changed bytes from the Z3 model, a byte-interval polyhedral box for a bounded
  subset of dependent input bytes, and normalized linear path constraints when
  QSYM can extract them. Later executions with the same
  prefix/expression/dependency key can replay the model, skip known UNSAT work,
  and generate extra samples from the saved constraint context before falling
  back to ordinary Z3 solving.

- SYMCC_POLY_CROSS_PREFIX=0/1 (default 0 in the standalone runtime; enabled
  by the adaptive MPI sampling profile): On an exact-key SAT miss, scan a
  bounded set of cache entries and classify their normalized
  linear abstractions as equivalent, cached-subset, current-subset, or
  compatible. This relation only ranks candidates. Every foreign model and
  every derived polyhedral sample is re-evaluated against the complete current
  prefix and desired target before it is written. UNSAT entries are never
  reused across prefixes.

- SYMCC_POLY_PROJECTED_REUSE=0/1 (default 1 when cross-prefix reuse is
  enabled): Permit foreign SAT entries with different variable sets or input
  lengths to be related over shared byte offsets. Missing byte variables are
  eliminated per linear row using their `[0,255]` interval, producing a
  conservative projected proposal domain. Cross-size entries must pass this
  projection path. Every projected model/sample is still evaluated against the
  complete current prefix and target; UNSAT entries are never projected.

- SYMCC_POLY_EXACT_PROJECTION=0/1 (default 1 when cross-prefix reuse is
  enabled): Refine projected relation classification with bounded exact
  integer formulas. Cached and current non-shared bytes are existentially
  quantified over `[0,255]`; Z3 checks both implications and their
  intersection. The interval projection remains the sampling envelope and
  every candidate still receives complete current-expression validation.
  Timeout or unknown falls back to interval classification.

- SYMCC_POLY_EXACT_PROJECTION_VARS=N (default 2, maximum 6): Maximum total
  number of existentially eliminated cached/current byte variables.

- SYMCC_POLY_EXACT_PROJECTION_ROWS=N (default 32, maximum 128): Maximum total
  number of cached/current linear rows admitted to exact relation checks.

- SYMCC_POLY_EXACT_PROJECTION_TIMEOUT=N (default 10, maximum 1000):
  Millisecond timeout for each implication or intersection check.

- SYMCC_POLY_EXACT_PROJECTION_PROBES=N (default 8, maximum 64): Maximum
  exact projected cache relations attempted for one branch.

- SYMCC_POLY_FIELD_RENAMING=0/1 (default 1 when cross-prefix reuse is
  enabled): Search for a bounded structure-preserving bijection or exact-proof
  injection between cached and current linear byte variables when their input
  offsets, widths, or total input sizes differ. A matched mapping rewrites the
  cached model, byte box, and full constraint matrix. Multi-byte endian changes
  are supported when their byte coefficients form a provable permutation.
  Wider/narrower variable-count mappings additionally require exact existential
  integer projection; interval-only relations cannot authorize width changes.
  This is SAT-candidate retrieval only; every renamed candidate is checked
  against the complete current prefix and target, and UNSAT is never renamed.

- SYMCC_POLY_RENAME_VARS=N (default 6, maximum 8): Maximum number of nonzero
  variables on either side of a field-renaming search.

- SYMCC_POLY_RENAME_ATTEMPTS=N (default 128, maximum 4096): Maximum number of
  complete variable mappings checked for one cached/current relation.

- SYMCC_POLY_RENAME_EXACT_PROBES=N (default 8, maximum 32): Maximum exact
  integer projection checks used while searching an injective width-changing
  field mapping. Widening and narrowing mappings are rejected when this proof
  budget is exhausted; they never fall back to interval-only acceptance.

- SYMCC_POLY_CROSS_PREFIX_PROBES=N (default 32, maximum 256): Maximum number
  of relation-ranked foreign SAT models evaluated for one branch. Telemetry
  reports `poly_cross_prefix_probes`, `poly_cross_prefix_relations`,
  `poly_cross_prefix_hits`, `poly_cross_prefix_validation_failures`,
  `poly_projection_attempts`, `poly_projection_relations`,
  `poly_projection_hits`, `poly_exact_projection_attempts`,
  `poly_exact_projection_relations`, `poly_exact_projection_unknown`,
  `poly_exact_projection_hits`, `poly_renaming_attempts`,
  `poly_renaming_relations`, `poly_renaming_hits`,
  `poly_sample_validations`, and
  `poly_sample_validation_failures`.

- SYMCC_PREFIX_CONTEXT_CACHE=0/1 (default follows SYMCC_POLY_CACHE): Cache the
  translated Z3 assertion vector for prefix dependency forests. This keeps
  repeated branch, address, and solve-all queries from rebuilding the same Z3
  context when Pangolin-style reuse is enabled.

- SYMCC_POLY_RANGE_BYTES=N (default 4, 0 disables box extraction): Maximum
  number of dependent input bytes for which the QSYM backend computes min/max
  feasible byte intervals when SYMCC_POLY_CACHE is enabled.

- SYMCC_POLY_LINEAR_BYTES=N (default 4, maximum 6): Maximum number of symbolic
  input bytes that the QSYM backend linearizes into one unsigned integer for
  cached path constraints. Linearized add/sub/neg and multiplication by small
  constants are stored with the poly cache and used to keep generated samples
  inside the cached context.

- SYMCC_POLY_SAMPLES=N (default 2, maximum 16): Number of deterministic samples
  to generate from a cached or freshly computed polyhedral byte box.

- SYMCC_POLY_TEMPLATE_BYTES=N (default SYMCC_POLY_RANGE_BYTES, maximum 16) and
  SYMCC_POLY_TEMPLATE_PAIRS=N (default 16, maximum 128): Add Pangolin-style
  linear template bounds to SAT cache entries. The runtime computes exact
  feasible min/max bounds under the current strict Z3 context for selected
  bytes, pairwise sums, pairwise differences, and already extracted linear
  path expressions. The serialized format remains the existing linear
  constraint column, so older cache entries are still readable.

- SYMCC_POLY_WALK=john|dikin|coordinate (default john when linear constraints
  are available): Choose the cache sampler. John and Dikin modes construct the
  complete dense `A x <= b` system from byte boxes and cached linear
  inequalities, factor the full slack-scaled barrier Hessian, and draw
  correlated directions through its Cholesky factor. John mode additionally
  performs fixed-point Lewis/leverage weighting over all facets. Every rounded
  byte assignment is checked against the exact integer inequalities; singular
  and boundary cases fall back to integer hit-and-run and coordinate sampling.

- SYMCC_POLY_DENSE_DIM=N (default 16, maximum 64),
  SYMCC_POLY_JOHN_STEPS=N (default 4, maximum 16), and
  SYMCC_POLY_WALK_STEPS=N (default max(12, 3 * dimension), maximum 256): Bound
  dense polytope dimension, John/Lewis reweighting iterations, and transitions
  per sample. Offsets outside the dense cap remain fixed in each inequality, so
  the projected polytope stays consistent with the concrete model.

- SYMCC_UNSAT_CORE_CACHE=0/1 (default 0): Enable an exact-subset UNSAT reuse
  cache in the QSYM backend. The runtime asks Z3 for tracked UNSAT cores,
  minimizes small cores under a bounded timeout, and stores both exact and
  structural fingerprints. Later same-shaped contexts can reuse the core even
  when symbolic input indices have been renamed. Linear constraint
  contradictions are also pruned early when the poly cache has collected
  normalized path constraints.

- SYMCC_UNSAT_CORE_MINIMIZE_MAX (default 16, maximum 128) and
  SYMCC_UNSAT_CORE_MINIMIZE_TIMEOUT (default 50 ms, maximum 1000 ms): Bound
  UNSAT-core reduction probes before caching.

- SYMCC_EMIT_HINTS=0/1 (default 0 in the runtime, enabled by the fuzzing
  helper): Emit changed-byte sidecars for generated inputs. Values 0, false,
  off, and no disable the option.

- SYMCC_STRING_HINT_DIR / SYMCC_HINT_DIR (default empty): Export concrete string
  and byte-sequence tokens observed by memcmp/bcmp/strcmp/strncmp wrappers when
  one side is symbolic and the other is concrete. The adaptive hybrid helper
  can feed these tokens to AFL++ extras/mutators.

- SYMCC_STRING_HINT_MIN / SYMCC_STRING_HINT_MAX (defaults 2 / 256, maximum
  4096): Minimum and maximum concrete token sizes emitted by the string hint
  channel.

- SYMCC_STRING_CONSTRAINT_OUT=PATH (default empty): Append versioned
  `symcc-string-constraint-v1` JSONL records for memcmp/strcmp/strncmp wrappers
  when exactly one side is concrete and the symbolic side consists of direct
  input-byte expressions. Each record contains the operation, site id, concrete
  token, NUL-termination flag, and exact input-offset patches. This is a
  SymCC-str-inspired string/BV bridge: it creates verifiable candidates without
  replacing the existing bit-vector path constraints.

  The same stream may contain `symcc-string-operation-v1` observations from
  bounded strlen/strchr/strstr/atoi wrappers. These rows bind a contiguous direct
  input-byte span through its first NUL, the symbolic operand role, constant
  operand, and observed length/index. They are translated to alternative
  length/indexof predicates in `symcc-string-query-v2`; they are observations,
  not direct patches. Incomplete, non-contiguous, embedded-NUL, over-budget, or
  multi-symbolic observations fail closed.

  The atoi model is deliberately restricted to a non-empty, unsigned ASCII
  decimal string of at most 10 digits whose value fits `int`. It emits a
  decimal-regex plus `str.to_int` alternative and an exact 32-bit BV
  multiply-by-10 fold. Whitespace, sign, locale, base prefixes, trailing
  characters, and overflow retain concrete libc semantics and emit no
  conversion artifact.

  The strtol model is separately restricted to `endptr == NULL`, concrete
  base 10, an optional single `-`, one or more ASCII digits, first-NUL
  termination, and a value fitting the target `long` width. The artifact binds
  `integer_bits`; both atoi and strtol queries assert their exact C type range
  before asking for a different value. Non-null endptr, `+`, whitespace,
  suffixes, base 0/non-10, locale, or ERANGE paths emit no strtol artifact.

- SYMCC_STRING_CONSTRAINT_MAX_BYTES=N (default 256, maximum 4096): Maximum
  concrete token bytes inspected for one string-constraint record. `strcmp`
  records include a NUL patch when the bounded concrete token terminates within
  the limit. It also bounds operation spans; the strstr BV contains summary has
  an additional 16384 byte-comparison product bound.

- SYMCC_STRING_CONSTRAINT_MAX_RECORDS=N (default 4096, maximum 1048576):
  Per-process cap on emitted string-constraint records.

- SYMCC_STRING_CONSTRAINTS=PATH (default empty in the AFL++ mutator): JSONL
  string-constraint artifact consumed by `util.afl_symcc_hint_mutator`. If this
  is unset, the mutator falls back to `SYMCC_STRING_CONSTRAINT_OUT`. The mutator
  applies the recorded offset patches as a separate `symcc_string` mutation
  stage before ordinary havoc fallback.

- SYMCC_STRING_SOLVER_ENABLE=0/1 (default 1 in the MPI helper): Capture a
  per-run hidden string-constraint artifact, translate eligible complete
  memcmp/strcmp/strncmp records into backend-neutral string queries, and write
  materialized `string-solver-*` candidates into the worker output directory.
  These candidates enter the existing AFL showmap and worker coverage triage;
  they are not admitted directly. `symcc-string-query-v2` declares both an SMT
  String and one 8-bit BV per covered input offset, links characters, length,
  and the first NUL exactly, and permits bounded BV byte predicates alongside
  String predicates. Version-1 queries are accepted and normalized to v2.
  A concrete evaluator rechecks both views before a solver candidate is used.

- SYMCC_STRING_SOLVER=COMMAND (default auto-discovered `symcc-query-solver`):
  Solver helper used by `util.string_constraints.SymccJsonStringBackend` and
  `util/symcc_string_solver.py`. The helper is invoked as
  `COMMAND --generic query.smt2 TIMEOUT_MS` and returns the existing JSON model
  protocol. If no helper is available, the MPI helper still applies exact
  offset patches and records the missing backend in metrics.

- SYMCC_STRING_SOLVER_PORTFOLIO=JSON_OR_PATH (default empty): Override the
  single backend with 1..8 bounded entries and optional `parallelism`.
  `kind=symcc-json` commands use the existing
  `COMMAND --generic QUERY TIMEOUT_MS` protocol. `kind=smtlib` commands receive
  an SMT-LIB file by replacing `{query}` (or appending the path) and may replace
  `{timeout_ms}`; the adapter appends `check-sat` and `get-value` for every
  linked 8-bit input symbol. Commands are argument arrays or shell-split strings
  and are never evaluated by a shell.

  Example:
    {"parallelism":2,"backends":[
      {"kind":"symcc-json","name":"z3","command":["symcc-query-solver"]},
      {"kind":"smtlib","name":"cvc5-adapter",
       "command":["cvc5","--lang","smt2","--produce-models","{query}"]}]}

  Optional validation-first online selection:
    {"parallelism":2,
     "selection":{"state_path":"/shared/string-backend-policy.json",
                  "max_backends":1,"warmup":1,"explore_every":16,
                  "context_limit":128,"exploration":0.35},
     "backends":[...]}

  `selection` is opt-in; without it every configured backend still runs.
  `max_backends` bounds calls per query. The policy groups queries by operation
  family, total-capacity bucket, variable count, and presence of linked BV
  constraints. It combines concrete-verified SAT yield, elapsed solver cost,
  global priors, context-local observations, cold-start trials, and periodic
  exploration. UNSAT is only a zero-reward observation and never a proof.
  `state_path` uses atomic replacement plus an advisory file lock so local
  MPI workers can share restart-stable evidence; omit it for process-local
  learning. Backend names must be unique.

  Backend calls run concurrently. Every SAT assignment is rechecked by the
  concrete dual-view evaluator; invalid SAT is rejected, duplicate valid models
  are classified separately, and distinct valid models may all enter the
  candidate budget. SAT/UNSAT disagreement is telemetry only: no portfolio
  UNSAT prunes execution or enters an UNSAT cache. Metrics include backend runs,
  SAT/UNSAT/unknown/error, rejected/duplicate models, and disagreements.

  Before enabling a new SMT-LIB backend, run:
    python3 util/string_backend_conformance.py \
      --backend STRING_PORTFOLIO_JSON_OR_PATH --timeout-ms 5000

  The executable gate submits six portable dual-view probes: binary bytes,
  contains plus a BV predicate, negative indexof, atoi, signed strtol10, and
  unsigned strtoul10.
  Every reported SAT assignment must pass the independent concrete evaluator.
  The command emits `symcc-string-backend-conformance-v1` JSON evidence and
  exits nonzero on an empty result, non-SAT result, incomplete model, or semantic
  mismatch. `--solver COMMAND` checks one symcc-query-solver-compatible backend.
  Conformance always bypasses learned selection and executes every backend.

  Worker metrics additionally record selected/skipped backend calls, policy
  updates, forced explorations, and the current number of bounded contexts.

- SYMCC_STRING_SOLVER_QUERY_LIMIT=N (default 4 in the MPI helper, maximum
  256): Maximum number of string-constraint records scanned for one worker
  execution. This bounds the number of string-theory solver calls on targets
  that emit many libc comparison artifacts.

- SYMCC_STRING_SOLVER_CANDIDATES=N (default 8 in the MPI helper, maximum 256):
  Maximum number of string-derived candidates written for one worker execution.

- SYMCC_STRING_SOLVER_TIMEOUT_MS=N (default 250 in the MPI helper, maximum
  60000): Per-query timeout for the string-theory backend. Offline use through
  `util/symcc_string_solver.py` defaults to 1000 ms.

- SYMCC_FAST_SOLVE=0/1 (default 0, QSYM backend): Try the bounded Fuzzy-Sat
  fast path for simple byte and concatenated integer comparisons before Z3.
  Every successful assignment is checked against the concrete expression
  before it is emitted.

- SYMCC_MULTI_SOLVE=0/1/2 (default 0, QSYM backend): Generate related branch
  models as a group. Level 1 recognizes consecutive-byte comparison patterns;
  level 2 additionally enables experimental switch-case and structure-field
  grouping. The adaptive coordinator normally selects this through a tailored
  executor profile.

- SYMCC_EXPR_CACHE_SIZE=N (default 65536, QSYM backend): Maximum entries in the
  expression hash-cons cache. The cache is synchronized and eviction-safe;
  setting a smaller value trades repeated construction for memory.

- SYMCC_DENSITY_OUT=PATH (default empty, QSYM backend): Run the target as a
  dependency-density profiler and write `input_offset branch_count` rows for
  interesting symbolic branches. MPI density balancing and TACE consume
  bounded variants of this profile.


                 Under-constrained execution options


- SYMCC_UCSAN_CONFIG=<path> (compile-time): Enable UCSan-style
  compilation-based under-constrained execution. The compiler renames any
  existing main, creates a self-contained main harness for the configured
  entry function, materializes entry arguments from structured roots, and
  instruments scoped pointer operations with pseudo-pointer shadow metadata.
  The accepted YAML subset is:

      entry: callee
      scope:
        - helper
      external: pure
      externals:
        api_name: arbitrary
      wrappers:
        api_name: wrapper_name

  `external` may be `pure`, `arbitrary`, or `passthrough`. Pure externals
  return structured root values. Arbitrary externals additionally invalidate
  pointer arguments passed to the stub. Wrappers replace the target call with a
  user-provided function of the same LLVM call type.

- SYMCC_UCSAN_ENTRY=<function> (compile-time): Enable the same mode without a
  config file and use this function as the under-constrained entry. This also
  adds the function to the instrumentation scope.

- SYMCC_UCSAN_SCOPE=<function[,function...]> (compile-time): Comma-separated
  additional functions whose pointer operations and call shadow channels should
  be instrumented.

- SYMCC_UCSAN_EXTERNAL=pure|arbitrary|passthrough (compile-time): Default
  external-call policy when no per-function policy or wrapper is configured.
  Native allocation, memory, process-exit, LLVM intrinsic, and SymCC runtime
  calls are passed through by default.

- SYMCC_UCSAN_INPUT=<path> (run time, default SYMCC_INPUT_FILE when unset):
  Structured seed read by the generated harness. Use util/ucsan_seed.py to
  create or inspect seeds. Root ids are entry argument indices. Pointer-object
  paths use `ROOT[/POINTER_FIELD_OFFSET...][@LOWER]`, where LOWER is the
  object's logical lower bound relative to the pseudo pointer. For example,
  `--root 0=0100000000000000 --object 0@-8=...` seeds argument 0 as pseudo
  pointer value 1 and gives its pointee object bytes starting at logical
  offset -8. `--alias PATH[@LOWER]=OBJECT_ID` maps additional paths to an
  existing object. Reusing an object id expresses pointer aliasing/shared
  subobjects; mapping a nested path back to an ancestor's id expresses a cycle.

- SYMCC_UCSAN_DUMP=<path> (run time): Dump the roots and JIT-provisioned
  objects observed during the execution in the same structured seed format.

- SYMCC_UCSAN_SYMBOLIZE=0/1 (default 1): Mark structured root and object bytes
  symbolic at their original seed-file offsets. Set to 0 for concrete
  reproducibility tests.

- SYMCC_UCSAN_MAX_OBJECT=N (default 1048576): Maximum JIT-provisioned object
  size in bytes. Container-of style negative offsets and upper-bound growth are
  allowed as long as the resulting allocation remains under this cap.


                         Hybrid coordinator options


- SYMCC_ADAPTIVE_SCHEDULER=0/1 (default 1): Enable contextual LinUCB seed
  scheduling, the cost-aware solver-strategy portfolio, and bounded path
  replay in mpi_fuzzing_helper.py. Set to 0 for a legacy-policy ablation.

- SYMCC_SELF_CONFIG=0/1 (default 1 with the adaptive scheduler): Enable
  ParaSuit-style online parameter discovery and posterior sampling. The
  coordinator loads `util/self_config_schema.json`, applies its conditional
  parameter DAG, and attributes reward/cost only to parameters actually sampled
  by the assignment token. State is atomically persisted at
  `$AFL_OUT/<symcc-name>/.self_config_state.json`.

- SYMCC_SELF_CONFIG_SCHEMA=<json-or-path> (default
  `util/self_config_schema.json`): Override the versioned
  `symcc-self-config-parameter-schema-v1` registry. Each parameter declares
  `values`, optional numeric `min`/`max`, and optional `active_when` parent
  values. Unknown-parent and cyclic condition nodes are rejected. The normalized
  registry can be inspected with
  `python3 util/self_config.py --print-schema`.

- SYMCC_SELF_CONFIG_SPACE=<json-or-path>: Add or override bounded candidate
  values in the discovered parameter schema. Existing runtime profiles are
  merged as observations, and productive numeric values may expand by one
  bounded half/double step after sufficient evidence.

- SYMCC_SELF_CONFIG_PARAMETERS=N (default 4, maximum 16): Maximum number of
  active parameters sampled in one assignment after condition-graph filtering.

- SYMCC_SELF_CONFIG_SEED=N (default unset): Deterministic RNG seed for
  reproducible parameter-policy runs.

- SYMCC_SELF_CONFIG_PRIOR=<state-json> (default unset): Import global
  parameter/value posteriors from another campaign as a decaying, read-only
  prior. Imported pulls never enter the target campaign's observation counts,
  context posteriors, interactions, or saved local statistics.

  Target-local posteriors are conditioned on bounded program phase
  (`cold/warm/mature`), targeted/non-targeted work, structural-task presence,
  and input-size bucket. Worker rank is deliberately excluded so changing MPI
  parallelism does not fragment learned contexts. Pairwise interaction
  posteriors are capped at 4096 and context strata at 128.

- SYMCC_SIMIFUZZ=0/1 (default 1 with the adaptive scheduler): Enable
  seed-worker contextual scheduling. The pair context combines the ordinary
  seed vector with worker-local yield, cost, previously observed sites and
  paths, structural-region affinity, cross-learning opportunity, and overlap
  with assignments already in flight. DynamiQ structural ownership remains the
  first eligibility boundary; pair scoring chooses among eligible work.

- SYMCC_SIMIFUZZ_SLICE=SECONDS (default 30): Aggregate pair feedback over this
  interval before updating LinUCB. Slice reward combines exact globally new AFL
  bitmap features with worker-local acquisition of already globally known
  branch sites, accepted corpus entries, cost, and the ordinary scheduler
  reward.

- SYMCC_SIMIFUZZ_CANDIDATES=N (default 64, maximum 512): Maximum queued work
  items evaluated per idle worker. Bounding this window keeps pair scoring off
  the MPI master's asymptotic hot path during large queue bursts.

- SYMCC_PREFIX_DAG=0/1 (default 1): Maintain a bounded prefix execution DAG in
  the coordinator. Shared actual prefixes accumulate subtree reward, open
  opposite branches are scheduled explicitly, and SAT/UNSAT/stale target
  summaries retire completed work. Frontier selection uses a UCT-style score
  combining subtree reward, exploration pressure, ColorGo distance, data
  comparison progress, mutation rarity, and historical solver timeout/cost.

- SYMCC_PREFIX_DAG_NODES (default 4096, minimum 128): Maximum number of prefix
  DAG nodes retained in the adaptive scheduler state. When the cap is reached,
  old low-value terminal nodes are evicted first; active nodes are also bounded
  if a target exposes more open prefixes than the budget.

- SYMCC_SELECTIVE_SAMPLING=0/1 (default 1): Let the prefix DAG restrict the
  solver-strategy portfolio for explicit target jobs. Difficult, high-reward
  branches that mutation is unlikely to cover are allowed to use multi-solution
  profiles; easier branches prefer cheaper profiles.

- SYMCC_S2F_DUAL_EXECUTOR=0/1 (default 1): Use an S2F-style exact/tailored
  executor split in the adaptive scheduler. The first attempt at an explicit
  open-prefix target uses the exact Z3 profile; follow-up attempts on hard or
  low-mutation-probability branches can select high-throughput fast/multi-solve
  tailored profiles.

- SYMCC_S2F_SAMPLING_BUDGET (default 2): Maximum early targeted attempts for
  which each prefix can use the sampling executor action. The action-seed tree
  tracks exact, tailored, and sampling attempts, reward, cost, and consecutive
  failures independently; after this sampling-action budget is consumed, the
  branch falls back to exact/tailored profiles.

- SYMCC_S2F_HIGH_QUEUE_FRACTION (default 0.75): Fraction of replay capacity
  assigned to prefixes with productive action history, directed/data progress,
  or path-cover value. Remaining capacity is reserved for the exploratory low
  queue; single-slot selection visits the low queue every fourth dispatch.

- SYMCC_S2F_ACTIONS_PER_SEED (default 16): Maximum branch actions attached to
  one S2F actionseed dispatch. For a selected seed, the coordinator batches
  high-queue open branches as `solve` or `sample` actions and can mark
  lower-value same-seed branches as `skip`, matching S2F's non-sleeping
  high/low queue split without spawning one MPI job per branch.

- SYMCC_S2F_ACTIONS=<path> (worker run time): QSYM actionseed file consumed by
  one execution. Each non-comment row is `branch_id action`, where action is
  `solve`, `sample`, or `skip`. `solve` and `sample` force the branch to bypass
  normal coverage/directed pruning when its prefix is reached; `sample` uses
  the active sampling executor profile, including Pangolin poly-cache samples
  when enabled. `skip` records the branch but suppresses solving for that
  execution. The MPI helper normally writes this file per worker item.

- SYMCC_OPTIMISTIC_FIRST=0/1 (default 0, normally coordinator-managed): Use a
  SYMCTS-style mutation order for one execution. The solver first checks the
  flipped current constraint without the full path prefix; if that optimistic
  query is UNSAT/timeout, it skips the expensive strict solve, otherwise it runs
  the strict path-constrained solve and keeps optimistic fallback output only if
  strict solving fails. Adaptive MPI exposes this as a tailored profile.

- SYMCC_BACKSOLVER=0/1 (default 1): Enable bounded Backsolver-style recovery
  from implicit-flow constraints. The compiler preserves symbolic `select`
  values as ITE expressions and reconstructs ITEs for two-input PHIs or
  3--8-input PHIs in bounded acyclic conditional regions. Nested two-input
  PHIs are recursively folded into nested ITEs. Multi-arm regions use an
  explicit path worklist (at most 64 paths) to reconstruct predecessor
  relevance predicates and a reverse ITE region-state chain, so internal
  choices remain visible when an outer target is solved. PHI incoming values
  may be constants,
  previously available symbolic values, bounded side-effect-free SSA
  computations cloned from the two branch arms, or read-only load snapshots
  proven safe by MemorySSA/AliasAnalysis; ambiguous loads, calls, stores,
  divisions, loops, and non-canonical control flow remain conservative
  fallbacks. A merge-local simple load may additionally recover a two-arm
  write state when its direct MemorySSA definition is a 2--8-input MemoryPhi,
  all incoming definitions resolve to equal-width simple stores, AA proves
  each store MustAlias the load, and every other region write is proven not to
  Mod that location. Data PHIs and MemoryPhis share the same exact
  branch-region partition (at most 32 total blocks and 64 paths). Each
  MemoryPhi incoming may skip at most 8 preceding
  MemoryDefs when AA proves every skipped definition NoMod for the target
  location. The generated ITE carries `symcc.ifss_memory` metadata with stable
  load/controller/store sites; a def-chain proof additionally includes the
  true/false skip counts and nearest-first skipped sites; a multi-arm proof
  records every incoming block/store plus its path and skip counts. MayAlias,
  partial overlap, a ninth definition, volatile, atomic/fence, undef/poison,
  and unknown ModRef fall back without transformation.
  Within one accepted multi-arm data or memory partition, original LLVM
  condition values are deterministically deduplicated before any predicate is
  built. Every condition that needs symbolic synthesis owns an independent
  short-circuit computation and exit PHI; cached RegionValues deliberately do
  not own those instructions. This preserves dominance when several internal
  conditions are reused across multiple enumerated paths. Such expressions
  carry `symcc.ifss_condition` metadata with schema
  `partition-condition-cache-v1`. A condition with no admissible symbolic
  input, or any later synthesis failure, rejects and rolls back the complete
  partition. The cache is local to one merge and does not claim structural
  hash-consing across partitions.
  When the
  strict query containing the recorded path prefix fails and the target
  expression contains an ITE, QSYM enumerates near-current ITE-controller
  outcomes, tries to invert those controllers directly, and validates every
  candidate by replaying the target plus retained independent prefix
  constraints through the lightweight expression evaluator. Only after this
  verified direct path fails does it retry the target with Z3 after dropping
  prefix constraints whose dependencies overlap an ITE controller. This retry
  also runs after a strict UNSAT-core or poly-cache hit.
  Generated inputs use the `-backsolve` suffix and are concretely triaged by
  the MPI worker before entering the shared corpus.

  Tunables:
    SYMCC_BACKSOLVER_CONTROLLERS (default 8, max 12): maximum ITE controllers
      considered for one target.
    SYMCC_BACKSOLVER_CANDIDATES (default 128, max 4096): maximum direct
      controller-candidate validations per target.
    SYMCC_BACKSOLVER_ENUM_BYTES (default 2, max 8): maximum dependent bytes
      covered by the one-byte truth-table fallback.
    SYMCC_BACKSOLVER_ENUM_BUDGET (default 512, max 4096): total fallback
      enumeration budget.

  Setting this option to 0 disables the ITE-specific prefix adaptation, but it
  does not remove ITE expression propagation from compiler instrumentation.
  This implementation covers compiler-visible `select`, canonical
  two-predecessor PHIs, and branch-only single-exit multi-arm regions bounded
  to 3--8 incoming values, 12 expression levels, 32 acyclic basic blocks and
  64 paths. It also supports bounded read-only load snapshots when
  MemorySSA/AliasAnalysis prove that the region has no interfering write or
  escaping alias, plus the strict multi-arm MustAlias write-state case above.
  Multi-arm and memory synthesis require exact structural proofs, independent
  ownership for every cached symbolic condition, and atomically roll
  speculative IR back on a late rejection. It does not claim
  arbitrary IFSS region discovery, multi-location memory state, multi-exit or
  loop state, general/shared-destination switch-edge splitting, ambiguous
  memory, or
  expression substitution across non-canonical control flow.

- SYMCC_IFSS_SWITCH_STATE=0/1 (compile time, default 0): Enable F255 bounded
  switch-to-branch lowering before return-exit lowering and symbolization.
  Eligible switches have 2--8 logical case/default edges and at least two
  unique successors. Every successor must have only the switch controller as
  its unique predecessor block and all arms must either branch unconditionally
  to one exact-predecessor merge or return normally.
  Cases become a deterministic sequence of equality branches followed by the
  default edge; destination PHIs are updated to the corresponding test block.
  Existing data/MemorySSA IFSS state recovery then consumes the branch region.

  Generated comparisons and branches carry `symcc.ifss_switch` metadata with
  schema `bounded-switch-chain-v1`, original switch site, case ordinal/value,
  and arm count. The last branch also carries `symcc.ifss_switch_default`.
  External predecessors, conditional/mixed arms, a ninth logical edge,
  all-edges-to-one-destination switches, EH/address-taken blocks, and unclosed
  merges are unchanged.
  The compatibility default is linear in source case order. F256/F257 add:

    SYMCC_IFSS_SWITCH_MODE=linear|balanced|profile (default linear)
    SYMCC_IFSS_SWITCH_PROFILE=<path>
    SYMCC_IFSS_SWITCH_MANIFEST_OUT=<path>

  `balanced` sorts cases by unsigned APInt value, emits `ule` range nodes and
  exact-equality leaves, and marks them with `bounded-switch-tree-v1`.
  Every leaf miss enters default; a default destination PHI therefore receives
  one copy of its original edge value per leaf predecessor. For seven cases,
  maximum decision depth is four instead of seven, while total comparisons
  increase from seven to thirteen.

  `profile` expects ASCII-space-separated rows:

    <stable-switch-site> <unsigned-decimal-case|default> <positive-weight>

  Comments begin with `#`. A site must have exactly one row for every case and
  one `default` row. The pass computes a deterministic optimal alphabetic
  range tree over the case weights and marks its root with
  `profile-weighted-switch-v1`, including the full profile fingerprint,
  weights, and objective. Missing, unreadable, malformed, duplicate, stale, or
  incomplete input falls back to `balanced` with
  `profile-switch-fallback-v1` metadata. Since one aggregate default count
  contains no value-gap distribution, it is recorded in the proof but is not
  used to choose splits. Unknown mode text falls back to `linear`.

  If an external profile is not configured, or it contains no entry for an
  otherwise eligible site, profile mode may import a valid LLVM
  `!prof branch_weights` vector. Successor zero is default and the remaining
  weights follow source case order. The vector must contain exactly one
  positive weight per logical edge. An explicitly configured unreadable,
  malformed, duplicate, or incomplete external entry is authoritative and
  falls back to balanced instead of silently using LLVM metadata.

  `SYMCC_IFSS_SWITCH_MANIFEST_OUT` appends one
  `symcc-ifss-switch-tree-v1` JSON record per transformed switch. It records
  normalized profile provenance, fallback, objective, complete preorder tree,
  case/destination mapping, original/lowered edge multiplicity, and
  profile/tree fingerprints. Verify one or more JSONL files offline with:

    python3 util/verify_ifss_switch_manifest.py <manifest.jsonl> [...]

  The verifier recomputes saturated optimal-tree DP, every split and
  multiplicity, and both fingerprints. Remove or rotate a shared output before
  a new compilation campaign; output uses append mode.

  These modes do not redistribute an aggregate default weight into generated
  range-branch `!prof` metadata, split shared switch critical edges with
  external predecessors, compress ranges, model indirect control, or summarize
  loop switches.

  F258 accepts multiple case/default edges sharing a destination when LLVM
  PHI multiplicity is exact and all repeated incoming values from the switch
  controller are identical. Linear lowering preserves original multiplicity;
  balanced/profile lowering may increase a shared default destination's
  multiplicity because every equality leaf has a default miss edge. Root
  metadata `shared-switch-edge-split-v1` records original/lowered totals and
  per-destination multiplicities. Rewritten PHIs carry
  `shared-switch-phi-multiplicity-v1`. Shared two-endpoint data and memory
  states use the full path-partition algorithm rather than the direct
  two-branch shortcut.

- SYMCC_IFSS_EXIT_STATE=0/1 (compile time, default 0): Enable F254 bounded
  normal-return exit-state lowering before Hydra, continuation export, and
  regular symbolic instrumentation. Eligible functions have 2--8 distinct
  scalar return states controlled by one branch-only, single-entry, acyclic
  region with at most 32 non-controller blocks and 64 enumerated paths. Every
  path must end in one of the function's returns and every return must be
  reached by the region. The pass redirects those returns to a synthetic
  dispatch block with one `ifss.exit.state` PHI, allowing the existing
  multi-arm IFSS machinery to propagate a return ITE to callers.

  The state PHI and unified return carry `symcc.ifss_exit` metadata with schema
  `bounded-return-exit-state-v1`; each redirected edge carries
  `symcc.ifss_exit_arm` with its ordinal and original return site. Void,
  aggregate/vector, identical-Value, undef/poison, musttail, switch, loop,
  exception/indirect, ninth-exit, address-taken, and unclosed regions fall back
  without CFG changes. This is an opt-in compile-time transformation; runtime
  `SYMCC_BACKSOLVER` independently controls ITE-specific solving. It does not
  support arbitrary continuation identities, live-out tuples, exception
  exits, or multi-location memory state.

- SYMCC_IFSS_CONTINUATION_STATE=0/1 (compile time, default 0): Enable F260
  bounded multi-continuation exit-id/live-out tuple lowering after switch and
  return-exit lowering, but before Hydra, live-continuation export, and regular
  symbolic instrumentation.

  An eligible controller is a conditional branch whose dominated,
  branch-only, acyclic region has 2--8 distinct CFG exit edges, at least two
  continuation destinations, at most 32 region blocks, and at most 64
  enumerated paths. A boundary is a block outside the controller's dominance
  region or a block beginning with PHIs. The pass accepts at most the first
  fully proven region in each function.

  Every destination PHI becomes one tuple slot; the region normally must have
  1--8 integer, floating-point, or pointer slots. When
  SYMCC_IFSS_CONTINUATION_MEMORY=1, a zero-SSA-slot region may proceed so that
  the analysis-backed memory pass can discover memory state. Incoming edge
  multiplicity must exactly match the CFG, repeated predecessor edges must
  carry the same LLVM value, and direct undef/poison is rejected. All checks
  finish before the CFG is modified.

  Accepted exit edges enter per-edge capture blocks and a common dispatch with
  `i8 ifss.cont.exit_id` plus one PHI per live-out slot. A real conditional
  branch chain consumes the exit ID, then per-edge resume blocks return to the
  original destinations. Destination PHIs are rebuilt one logical edge at a
  time. Metadata schema `bounded-continuation-tuple-v1` records controller,
  source-terminator/successor, destination, slot, original PHI, and bounded
  region counts.

  This flag does not enable runtime Backsolver by itself. It does not summarize
  loops, split aggregates, or model exception/coroutine/indirect exits.
  MemorySSA locations require the separate flag below. Unsupported candidates
  retain their original CFG.

- SYMCC_IFSS_CONTINUATION_MEMORY=0/1 (compile time, default 0): Enable F262/F286
  MemorySSA/AA-proven scalar memory slots for regions already lowered by
  SYMCC_IFSS_CONTINUATION_STATE=1. The automatic Function pass runs immediately
  after F260 and before Hydra or symbolic instrumentation.

  A candidate is a used, simple, non-atomic/non-volatile integer,
  floating-point, or pointer load in a continuation destination. Its MemoryUse
  must be defined by the F260 dispatch MemoryPhi. Dispatch capture edges,
  destination resume predecessors, controller identity, exit count and
  destination ordinals must exactly match F260 metadata; external
  predecessors fail closed.

  For every exit that reaches the load's destination, the pass follows at most
  eight MemoryDef links from the corresponding dispatch incoming state. It may
  skip only definitions that AliasAnalysis proves NoMod for the load location.
  The chain may end in an equal-width simple MustAlias store whose instruction
  and stored value dominate the capture. F269 also permits some relevant exits
  to end exactly at Function MemorySSA LiveOnEntry when the load pointer
  dominates that capture and at least one other relevant exit has a proven
  store. F270 may additionally recurse through a non-dispatch MemoryPhi that
  dominates the downstream edge. Each such phi must have 2--4 unique incoming
  blocks; each relevant exit is bounded to four nested phis and 16 provenance
  nodes. Every edge independently applies the same eight-definition NoMod
  bound and must terminate in a store or LiveOnEntry leaf. A recursion active
  set rejects cycles. MayAlias/Mod effects, atomics, fences, a five-arm phi,
  repeated incoming blocks, direct undef/poison, an all-LiveOnEntry candidate,
  or any exceeded bound reject the whole location.

  F275 is a fallback when the equal-width v1--v3 proof fails for a 2--8-byte
  integer load. It scans at most 16 linear MemoryDef nodes and maps every
  address-order load byte to its latest overlapping simple integer store byte.
  Store and load addresses must reduce through inbounds constant offsets to the
  same pointer base; each store is 1--8 bytes and byte aligned in type width.
  Uncovered lanes may come from one path-local LiveOnEntry snapshot. Source and
  destination bit shifts follow the module DataLayout endianness, so the same
  lane proof works on little- and big-endian modules. Every relevant exit is
  rebuilt in byte-lane mode; each must contain at least one store source and
  cover every lane. A dynamic/unknown overlap, Mod/MayAlias interference,
  MemoryPhi, volatile/atomic access, undef/poison value, non-inbounds address,
  unsupported width, or exceeded definition budget rejects the whole slot.
  This is exact byte reconstruction, not symbolic alias partitioning.

  F276 adds one bounded symbolic alias partition per relevant path. The pointer
  of one simple integer store may be an LLVM `select i1` whose condition is a
  stable instruction dominating the capture. Both pointer arms must reduce to
  inbounds constant intervals: each arm either overlaps a known load lane on
  the same base or is independently AA-proven NoAlias. An overlap on exactly
  one arm becomes a guarded overlay on the older lane source; overlap on both
  arms is accepted only when both select the same store byte. The generated
  byte is `select guard, new-store-byte, previous-byte` with polarity matching
  the pointer select. At most one distinct guarded store is accepted on a
  path. Unknown alias arms, argument-only guards without stable site identity,
  a second guarded store, non-select symbolic pointers and nested MemoryPhi
  remain fail closed.

  F277 admits one canonical loop-carried byte-lane state. The reaching
  MemoryPhi must have exactly two incoming edges: one unique unconditional
  entry edge outside the header's dominance region and one unique
  unconditional latch edge dominated by the header. The header must dominate
  the capture. Entry bytes use the F275 proof. The latch scans at most 16
  MemoryDefs back to the same MemoryPhi; exact constant-offset stores replace
  covered lanes and every uncovered lane carries the corresponding byte of the
  integer cycle PHI. At least one store lane and one carry lane are required.
  Prefix and latch NoMod chains retain the eight-site bound. Conditional or
  multiple backedges, nested MemoryPhi, dynamic offsets, guarded latch stores,
  full-width no-carry updates, atomics and volatile accesses fail closed.

  F278 generalizes one store's pointer select to a complete depth-two finite
  union: two or three unique internal selects and three or four leaves. Every
  instruction guard must dominate the capture. Each leaf is independently an
  exact same-base constant interval or AA-proven NoAlias. Every load lane must
  have at least one fallback leaf and the tree must contain an overlap. Shared
  select DAGs, depth three, unknown leaves and a second partition store reject.

  F279 permits two single-level guarded stores on one path. Reverse MemorySSA
  order assigns priority zero to the newest writer and one to the older writer.
  Lowering applies older first and newest last, so simultaneous guards select
  the newest store. A third guarded writer, a mix with F277/F278, unknown
  pointer arms and cross-MemoryPhi priority remain unsupported.

  F280 extends F277 with one strict conditional backedge diamond. The latch
  MemoryPhi must have exactly one arm whose bounded MemoryDef chain reaches the
  header MemoryPhi through exact partial stores and one arm that directly
  carries that same MemoryPhi. Both arms have the same conditional branch
  predecessor, one predecessor each, and one unconditional edge to the latch.
  The i1 guard must be an instruction with stable identity and dominate the
  latch. Lowering selects the stored or carried byte with the original
  condition and polarity before endian-aware composition. Argument-only
  guards, a writer on the carry arm, unknown ModRef on the write arm,
  non-strict joins, multiple backedges, mixed v6/v9 cycles in one slot and
  nested conditional transfer reject.

  F281 accepts one canonical header MemoryPhi with exactly one external entry
  and two internal unconditional latches. Each latch independently scans a
  bounded MemoryDef chain back to the same header phi and must contain both an
  exact partial-store lane and a self-carry lane. Lowering creates a three-
  incoming integer PHI and materializes each transfer in its own latch; LLVM
  predecessor selection supplies the semantics, so no artificial latch
  priority is introduced. Three latches, a full-width transfer on either
  latch, nested/conditional latch MemoryPhi, symbolic offsets and mixed
  single-/multi-latch cycle schemas reject.

  F282 composes one newest F278 depth-two pointer-union store with at most one
  older F276 single-level guarded store on the same path. Lowering first
  reconstructs the base byte, applies the older guarded select, and then uses
  that value as every NoAlias/fallback leaf of the newer pointer tree. Thus a
  matching union leaf wins over the older writer, while a fallback leaf
  preserves `old_guard ? old_byte : base_byte`. The reverse program order, two
  older guarded writers, a second partition, or another exit in the same slot
  requiring the two-writer v8 priority schema reject the whole slot. Unknown
  leaves, symbolic offsets, MemoryPhi and volatile/atomic accesses also reject.

  F283 composes the F280 conditional transfer with the F281 two-latch header.
  The header still has exactly one external entry and two internal backedges.
  Each backedge independently proves either an unconditional partial-store/
  self-carry transfer or one strict write-versus-carry diamond; at least one
  transfer must be conditional. Lowering preserves the actual three-incoming
  PHI and emits the guarded byte update only in its owning latch, so no
  cross-latch writer priority is invented. A single dominating instruction
  guard may be shared by both latch branches, and each branch retains its own
  true/false store polarity.

  F283 rejects an argument-only guard because it has no stable instruction
  identity, two writing arms because there is no canonical carry, an unknown
  ModRef in a write chain, non-strict diamonds, a third latch, full-width
  no-carry transfers, dynamic offsets, volatile/atomic accesses and mixed
  unsupported cycle structures. It remains a bounded two-latch byte-lane
  fixed point, not general loop-memory or heap reasoning.

  F284 raises the actual header MemoryPhi bound from two to two through four
  latches. The header has one external entry and two to four dominated
  backedges; every backedge independently proves an ordinary or strict
  conditional partial-store/self-carry transfer. Lowering emits an integer PHI
  with exactly one plus the transfer count incoming values and materializes
  each update in its owning latch. The CFG predecessor, not a synthesized
  priority chain, selects the active transfer.

  Two-latch-only slots keep the canonical v10 or v12 schema. A slot uses v13
  only when at least one relevant state has three or four transfers. Once v13
  is selected, another relevant state may contain two through four transfers;
  every transfer carries an explicit conditional-presence tag, including
  all-unconditional states. Five latches, any failed transfer proof, dynamic
  offsets, nested predicates, volatile/atomic accesses and unsupported cycle
  structure retain the original load.

  F285 replaces that nested-predicate rejection only for a bounded strict tree.
  A backedge MemoryPhi may have three or four leaf incoming values controlled
  by a unique-parent full binary tree with at most three internal `br i1`
  nodes. Each leaf is independently proven as pure self-carry or same-base
  constant-offset partial-store/self-carry, and at least one leaf must write.
  The pass materializes each complete integer in its original leaf block and
  creates an actual predecessor-selected leaf PHI in the latch; it does not
  eagerly evaluate or combine the branch guards. The header may have one
  through four latches, and non-tree latches may retain ordinary or strict
  conditional transfer records.

  F285 rejects five leaves, shared/reconvergent predicate DAGs, switch nodes,
  full-width leaves without carry, dynamic offsets, unknown ModRef,
  volatile/atomic accesses and any leaf that does not trace back to the same
  header MemoryPhi. This is a three-node/four-leaf proof budget, not arbitrary
  predicate CFG or general loop-memory reasoning.

  F286 replaces F278/F282's one-partition writer-order bound with a single
  ordered representation. A linear MemorySSA path may contain at most four
  conditional writer layers: no more than two F278 depth-two pointer
  partitions and two F276 single-level guarded stores. Ordinal zero is the
  newest writer. Guard layers retain per-lane source byte and true/false
  polarity; partition layers retain the complete node/leaf tree. If a newer
  unconditional store already owns a lane, older writer layers are masked to
  fallback for that lane.

  Lowering starts from the nearest definite store or path-local initial
  snapshot and applies layers oldest first, newest last. This makes the newest
  writer the outermost actual select and preserves MemorySSA last-writer
  semantics for arbitrary interleavings within the bound. One partition
  remains v7, two guarded writers remain v8, and newest-partition/older-guard
  remains v11; only a non-legacy ordering or a second partition upgrades the
  slot to v15. A third partition or guard, fifth total layer, depth-three or
  shared select DAG, unknown alias leaf, dynamic offset, cross-MemoryPhi
  priority, volatile/atomic access, poison/undef value, aggregate or exception
  edge remains fail closed.

  Each controller carries at most four accepted memory slots. A fifth
  candidate rejects memory lowering for that controller instead of committing
  a partial tuple. Accepted slots are PHIs in the F260 dispatch. A direct store
  leaf contributes its stored operand. A LiveOnEntry leaf gets a path-local
  snapshot load immediately before its capture or MemoryPhi incoming branch;
  it executes only on a path that reaches the original destination. Nested
  provenance is materialized bottom-up as scalar PHIs in the corresponding
  MemoryPhi blocks. Exits for other destinations carry a typed zero/null that
  is never consumed there. The original destination load is retained and still
  executes, but its data uses consume the proven dispatch PHI. A may-write
  instruction before that load in the destination rejects the slot.

  Metadata schema `must-alias-continuation-memory-tuple-v1` records controller,
  slot, destination, load, exit/store and skipped NoMod site identities. This
  remains the all-store form. A mixed store/initial tuple uses
  `must-alias-or-live-on-entry-continuation-memory-tuple-v2`, records a state
  kind and canonical source for every relevant exit, and binds every snapshot
  to the same proof. A tuple containing a nested phi uses
  `bounded-acyclic-memoryphi-continuation-memory-tuple-v3`. Its canonical
  preorder records each node kind/source/NoMod chain plus every incoming block
  site and child ordinal. Manifest/replay validation checks both nested scalar
  PHIs and the dispatch PHI's actual store/snapshot/neutral incoming values.
  F275 uses `byte-lane-continuation-memory-tuple-v4`; every relevant exit
  records byte width, endianness, skipped NoMod sites and a canonical lane
  vector of `(ordinal, source kind/site, source byte, source width)`.
  Lowering explicitly extracts, zero-extends, positions and ORs every byte.
  Independent LLVM replay checks that actual instruction chain and the unique
  path-local snapshot, rather than trusting metadata alone. General symbolic
  alias partitions, aggregate/vector state, atomics, destination write-after
  entry, and cross-function memory are unsupported.
  A tuple containing an F276 guarded overlay instead uses
  `guarded-byte-lane-continuation-memory-tuple-v5`. For every guarded lane it
  additionally binds guard site, true/false polarity, store site, source byte
  and width; replay checks the actual i8 select operands and condition. This is
  a two-arm finite partition, not general points-to or symbolic-offset aliasing.
  A tuple containing an F277 cycle uses
  `cyclic-byte-lane-continuation-memory-tuple-v6`. It distinguishes linear and
  cyclic exits, binds header/entry/backedge terminator sites, entry lanes,
  prefix/latch NoMod chains and each backedge store/carry lane. Lowering creates
  a real integer PHI in the original loop header and an endian-aware latch
  transfer; replay checks those actual PHI incoming blocks and expression
  sources.
  An F278 tuple uses
  `finite-pointer-union-continuation-memory-tuple-v7`, binding the partition
  store, preorder select/guard/child topology and every leaf lane source.
  Replay recursively checks the actual nested i8 select tree. An F279 tuple
  uses `guarded-write-priority-continuation-memory-tuple-v8`; each lane records
  zero to two newest-first guarded sources with explicit priority, and replay
  peels the actual outer-to-inner select chain before checking the base byte.
  An F280 tuple uses
  `conditional-cyclic-byte-lane-continuation-memory-tuple-v9`; it adds the
  branch, write-arm, carry-arm and guard sites plus write polarity to the v6
  cycle proof. Replay checks the actual guarded i8 update against the recursive
  header PHI.
  An F281 tuple uses
  `multi-latch-cyclic-byte-lane-continuation-memory-tuple-v10`; it records two
  ordered backedge states, each with its own site, NoMod chain and store/carry
  lanes. Replay checks the actual three-input recursive PHI and both latch
  expressions.
  An F282 tuple uses
  `pointer-union-priority-continuation-memory-tuple-v11`; its base lane record
  binds the older guard/polarity/store/source byte while its partition record
  binds the newer store, preorder select tree and all leaf lane sources.
  Replay first checks the actual guarded fallback select and then recursively
  checks the outer pointer-partition expression.
  An F283 tuple uses
  `conditional-multi-latch-cyclic-byte-lane-continuation-memory-tuple-v12`;
  it retains the ordered v10 backedge records and adds a per-transfer
  conditional/unconditional tag. Conditional transfers bind their branch,
  write arm, carry arm, instruction guard and store polarity. Replay checks
  the actual three-input recursive PHI plus each ordinary or guarded latch
  expression.
  An F284 tuple uses
  `bounded-multi-latch-cyclic-byte-lane-continuation-memory-tuple-v13`.
  It carries two to four ordered transfer records with an unconditional
  presence tag and optional branch/arm/guard/polarity fields. At least one
  cyclic state in a v13 slot must have three or four transfers. Replay checks
  an actual three- through five-input recursive PHI and every latch expression.
  An F285 tuple uses
  `nested-predicate-cyclic-byte-lane-continuation-memory-tuple-v14`.
  Each transfer has an unconditional, conditional or predicate-tree kind.
  Tree records bind preorder branch/guard nodes, typed child references,
  canonical leaves, per-leaf NoMod chains and every byte source. Replay checks
  the actual latch leaf-PHI, incoming block identity and leaf expressions in
  addition to the one- through four-latch header fixed point.
  An F286 tuple uses
  `ordered-writer-graph-continuation-memory-tuple-v15`. Each relevant exit
  records its plain base lanes followed by zero to four newest-first
  `writer_layers`. Guarded layers bind the store, instruction guard, width and
  per-lane byte/polarity arrays; partition layers bind a complete canonical
  pointer tree. Compiler replay parses the actual nested select expression
  outermost-to-innermost and checks the base source last.

- SYMCC_IFSS_CONTINUATION_MANIFEST_OUT=<path> (compile time, default empty):
  Append one F263 `symcc-ifss-continuation-manifest-v1` JSON record for every
  F260 continuation whose CFG/tuple proof can be replayed at the F262 analysis
  point. The manifest works with memory lowering on or off.

  Before writing, the compiler rechecks canonical exit ordinals, unique
  original terminator/successor edges, capture/resume equality, destination
  partition, scalar slot identities and all bounded counts. For every F262
  memory slot it uniquely locates the source load and reruns the current
  MemorySSA/AA MustAlias/NoMod proof; metadata store and skipped-definition
  sites must exactly equal the recomputed chain.

  All-store records use analysis label `llvm-memoryssa-aa-revalidated-v1`;
  F269 mixed records use
  `llvm-memoryssa-aa-live-on-entry-revalidated-v2`, add a per-slot
  `state_schema` and per-exit `state_kind`, and include those identities in the
  fingerprint. F270 nested records use
  `llvm-memoryssa-aa-nested-phi-revalidated-v3` and add `root_node` plus
  `provenance_nodes`; each record is a bounded canonical tree obtained by
  unfolding the accepted acyclic MemoryPhi provenance. F275 byte records use
  `llvm-memoryssa-aa-byte-lane-revalidated-v4` and bind byte width, DataLayout
  endianness, NoMod chain and every source lane. F276 guarded records use
  `llvm-memoryssa-aa-guarded-byte-lane-revalidated-v5` and add an optional
  `guarded_source` object to canonical lanes. F277 cyclic records use
  `llvm-memoryssa-aa-cyclic-byte-lane-revalidated-v6`, add cycle topology,
  nested entry state and backedge store/carry lanes. F278 finite-union records
  use `llvm-memoryssa-aa-finite-pointer-union-revalidated-v7`; F279 priority
  records use `llvm-memoryssa-aa-guarded-write-priority-revalidated-v8`.
  F280 conditional-cycle records use
  `llvm-memoryssa-aa-conditional-cyclic-byte-lane-revalidated-v9`.
  F281 two-latch records use
  `llvm-memoryssa-aa-multi-latch-cyclic-byte-lane-revalidated-v10`.
  F282 composed pointer-writer records use
  `llvm-memoryssa-aa-pointer-union-priority-revalidated-v11`.
  F283 conditional two-latch records use
  `llvm-memoryssa-aa-conditional-multi-latch-cyclic-byte-lane-revalidated-v12`.
  F284 bounded-latch records use
  `llvm-memoryssa-aa-bounded-multi-latch-cyclic-byte-lane-revalidated-v13`.
  F285 nested-predicate records use
  `llvm-memoryssa-aa-nested-predicate-cyclic-byte-lane-revalidated-v14`.
  F286 ordered-writer records use
  `llvm-memoryssa-aa-ordered-writer-graph-revalidated-v15`.
  Scalar/exit-only records use `structural-only-v1`. Site IDs and
  `proof_fingerprint` are canonical decimal strings. Verify artifacts with:

      python3 util/verify_ifss_continuation_manifest.py <manifest.jsonl>

  The verifier independently recomputes ordinal/count bounds, edge and
  destination partitions, scalar/memory slot structure, NoMod chain bounds,
  v3 node/edge/tree bounds, v4 lane/source/endianness invariants, v5
  guard/polarity/store identities, v6 cycle topology and canonical self-carry,
  v7 finite-tree ownership/leaf coverage, v8 write priorities, v9
  strict-diamond topology/guard polarity, v10 two-latch transfer ownership,
  v11 guarded-fallback/pointer-tree writer order, v12 per-latch conditional
  topology/polarity and shared data-guard identity, v13 2--4 transfer bounds,
  tagged layout and at-least-one-expanded-state rule, v14 tree root/indegree/
  forward-child topology, 3-node/4-leaf budgets and per-leaf partial-state
  completeness, v15 layer order/kind budgets, per-lane fallback/polarity,
  finite-tree ownership and full writer sequence, and the full content
  fingerprint.
  It does not implement LLVM AliasAnalysis; F265/F274
  invoke the compiler pass in a separate LLVM process to rederive that proof
  and validate the actual recursive PHI/select expressions.
  Use a fresh path per build and archive the corresponding pre/post IR and
  compiler identity. Appends are not currently locked or atomically sealed
  across concurrent compiler processes; write per-process files and merge only
  after each verifies.

  F264 can bind this manifest to the actual input/output IR, SymCC pass binary
  and LLVM tool with a write-once atomic SHA-256 envelope:

      python3 util/seal_ifss_continuation_artifact.py seal \
        --manifest continuations.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --output continuations.seal.json

      python3 util/seal_ifss_continuation_artifact.py verify \
        --manifest continuations.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --seal continuations.seal.json

  The seal records file sizes/SHA-256, ordered proof fingerprints and bounded
  `opt --version` output, then hashes canonical JSON. It uses an advisory lock,
  refuses an existing output, fsyncs a same-directory temporary file, atomically
  renames it and fsyncs the directory. This is local artifact integrity, not a
  cryptographic signature or remote attestation.

  F265 can additionally reconstruct the continuation proof in an independent
  LLVM process using the exact sealed lowered IR, compiler plugin and `opt`:

      python3 util/replay_ifss_continuation_artifact.py \
        --seal continuations.seal.json \
        --manifest continuations.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt

  Replay first performs the full seal verification, then forces continuation
  lowering off and runs only `ifss-continuation-memory` in a fresh `opt`
  subprocess. The pass must reconstruct a verifier-valid manifest whose JSON
  records exactly equal the sealed records. This rechecks current MemorySSA/AA
  semantics; it is not an independent AliasAnalysis implementation.

- SYMCC_IFSS_LOOP_SUMMARY=0/1 (compile time, default 0): Enable F261/F266/F271
  bounded affine natural-loop summarization after switch lowering and before
  return-exit/continuation lowering.

  Eligible loops have exactly one preheader, conditional header, backedge and
  recurrence update block. Without break exits the canonical form has two loop
  blocks. F271 may add up to three linear post-update check blocks, for at most
  five loop blocks total. The header condition must be unsigned `iv < trip`,
  where `iv` starts at zero and advances by a plain integer add of one. The
  trip value must be loop-invariant and have a proven unsigned maximum no
  greater than 8. Supported bound forms are <=3-bit integers, constants,
  freeze, bounded trunc/zext, select, constant-mask and, and positive-constant
  urem.

  The F261 path accepts 1--8 integer state PHIs whose updates are plain
  `state + constant`. F266 additionally accepts 2--4 same-width states up to
  4096 bits when plain add/sub and constant-multiply update DAGs form a
  unit-diagonal upper-triangular affine recurrence with at least one
  cross-state term. Each row has at most 32 expression instructions. Reverse
  dependencies, non-unit diagonal, cross-width state, `nuw/nsw`, memory,
  call, atomic, fence, extra update instruction, undef/poison source,
  unsupported exits, or unobserved state-only loops remain unchanged.

  Accepted states become `initial + trip * step` in the preheader using the
  same modular integer width. The pass redirects the preheader to the exit and
  deletes the now-unreachable header/latch. Generated arithmetic and the
  redirect carry `bounded-affine-loop-summary-v1` metadata with original
  loop/state sites and bounds.

  F266 writes `x'=Ax+b` as a compact nilpotent closed form using
  `A=I+N`, binomial coefficients for `trip<=8`, and compile-time `N^k`.
  Generated values carry
  `bounded-upper-triangular-loop-summary-v1`. Optional recurrence evidence:

      export SYMCC_IFSS_LOOP_MANIFEST_OUT=loops.jsonl
      python3 util/verify_ifss_loop_recurrence_manifest.py loops.jsonl

  The JSONL records base matrix/offset, sites/initial identities, and all
  derived matrix powers and offsets for trip 0 through the proven bound. The
  verifier recomputes modular matrix algebra and the content fingerprint.
  The path is append-only and currently emits records only for the F266
  triangular form; use a fresh file per compiler process.

  F267 also accepts one post-update equality break: after the recurrence,
  the latch may branch to a distinct break exit on `iv == break_at` and
  otherwise continue to the header. `break_at` must be loop-invariant and use
  the induction width. The summary uses
  `break_taken = break_at < trip` and
  `executions = break_taken ? break_at + 1 : trip`. Normal-exit PHIs must
  consume header state; break-exit PHIs must consume latch updates.

  F271 additionally accepts two or three ordered post-update equality checks.
  The update block completes the recurrence, then each check contains only
  `iv == break_at[i]` and a branch whose true edge reaches its unique break
  exit and whose false edge reaches the next check or the header. Every value
  is loop-invariant, uses the induction width, and is free of undef/poison.
  A fourth check, non-equality predicate, reversed edge, repeated exit,
  non-unique chain predecessor, extra check instruction, or wrong live-out
  phase rejects the loop.

  The priority circuit scans checks in CFG order with
  `better[i] = break_at[i] < winner_at`, initially `winner_at=trip`.
  Strict comparison selects the earliest iteration and preserves the lower
  ordinal on ties. It then uses
  `executions = break_taken ? winner_at + 1 : trip` and emits an ordered
  dispatch chain. Normal PHIs consume header-phase summaries; every selected
  break exit consumes the same post-update summary.

  Optional exit-identity evidence:

      export SYMCC_IFSS_LOOP_EXIT_MANIFEST_OUT=loop-exits.jsonl
      python3 util/verify_ifss_loop_exit_manifest.py loop-exits.jsonl

  F267 records use `post-update-equality-break-v1` and the complete bounded
  trip-by-break table. F271 records use
  `post-update-priority-equality-break-v2`, bind two or three ordered
  condition/exit/value identities and all break live-out sites, and enumerate
  the complete bounded trip-by-break-vector table. The largest accepted
  bound has 9^4=6561 rows. The verifier independently recomputes phase
  mappings, lexicographic `(break_at, ordinal)` winners, executions and the
  content fingerprint. This path is append-only and should be fresh per
  compiler process.

  This changes the instrumented CFG and does not claim source-edge coverage
  equivalence. Use original-binary replay for coverage measurement and compare
  this flag under equal outer CPU budgets.

- SYMCC_HYDRA=0/1 (compile time, default 0): Enable F248/F268/F272/F273/F287/F288
  profile-guided
  Hydra-style control-flow melding before live-continuation export and regular
  SymCC instrumentation. The pass transforms at most one eligible site per
  LLVM module. Production builds should always provide a profile or explicit
  site and should use a fresh shared manifest; the replay driver rejects a
  manifest containing more than one transformed site.

- SYMCC_HYDRA_PROFILE=<path> (compile time): Text profile generated by
  `python3 util/hydra_transform.py profile`. F288 makes
  `--profiled-command-json` mandatory for new CLI-generated profiles. The
  `symcc-hydra-profile-v2` artifact binds the resolved producing argv, stdin
  versus `@@` input mode, executable SHA-256 and command SHA-256; its text form
  carries the artifact, executable and command digests before these
  non-comment rows:

      site score observations interesting solver_time_us

  The compiler chooses the highest-score eligible site not present in the
  denylist. Stable IDs are initialized before transformation and are the same
  IDs exported in runtime `branch_trace`. V2 parsing is strict: a missing or
  malformed header, duplicate site, invalid statistic or unreadable profile
  fails closed without transforming any site. A valid empty profile also
  selects no site. Legacy v1 text remains accepted but has no binary-identity
  claim.

- SYMCC_HYDRA_SITE=<uint64> (compile time): Select one exact stable site and
  override the profile for the current compiler invocation. This is intended
  for replay/bisection and bounded experiments.

- SYMCC_HYDRA_MIN_SCORE=<float> (compile time, default 0): Reject profile
  entries below this score. Invalid/non-finite values become 0.

- SYMCC_HYDRA_DENYLIST=<path> (compile time): Newline-separated stable site IDs
  that must not be transformed. `hydra_transform.py campaign` writes this list
  from transformed-only failures for the next compile/explore iteration.

- SYMCC_HYDRA_MODE=safe|aggressive (compile time, default aggressive):
  `safe` accepts only bounded ALU/compare/cast/select/GEP/freeze arms.
  `aggressive` additionally linearizes simple non-atomic/non-volatile loads and
  implements unmatched stores and guarded tree stores with an immediate
  old-value readback. Aggressive
  output is failure-preserving rather than fully semantics-preserving and must
  never be used as the final failure authority.

- SYMCC_HYDRA_MANIFEST_OUT=<path> (compile time): Append one
  `symcc-hydra-transform-v1` JSON record containing module/function/site,
  profile evidence, mode, aligned/extra/load/store/select counts and
  `requires_original_replay`. F268 equal-arm records additionally contain
  `bounded-multiblock-linear-hydra-v1`, ordered arm block sites, complete
  instruction-site/opcode alignment, output PHI sites, a structure fingerprint,
  and `requires_original_coverage_replay=true`. F272 independently permits one
  to four blocks per arm, with at most 64 flattened instructions in each arm;
  the arm block counts may differ. Its
  `bounded-unequal-linear-hydra-v2` record binds left/right block and instruction
  counts, the deterministic `compatible-lcs-left-tie-v2` algorithm, every edit
  slot's opcode/site/block ordinal, one-sided edit distance, output PHIs and a
  complete structure fingerprint. F273
  `bounded-internal-tree-hydra-v3` records additionally bind each side's
  internal-branch and leaf-edge counts, deterministic DFS-preorder
  parent/incoming-edge/successor topology, branch terminator sites, canonical
  merge-leaf edges, and
  `compatible-lcs-tree-preorder-left-tie-v3`. F287
  `bounded-acyclic-sese-dag-hydra-v4` records instead bind a deterministic
  stable-site-tied topological order, every block's complete canonical
  `(predecessor block ordinal, predecessor successor index)` set, forward
  successors, local-merge and local-PHI counts/sites, merge leaves, LCS slots
  and output PHIs. The independent verifier derives predecessor sets and
  local-merge counts from successor edges, requires declared local-PHI sites
  to equal the LLVM PHI-opcode slots, and recomputes the structure fingerprint.
  F288 additionally records `selection_source`; a v2-selected record binds
  `profile_schema`, `profile_sha256`, `profiled_executable_sha256` and
  `profiled_command_sha256`. Hydra, switch, loop and continuation manifests now
  share a process-safe publisher that constructs a complete payload, acquires
  an exclusive advisory `flock`, uses `O_APPEND` with partial-write/EINTR
  handling, calls `fsync`, and then unlocks. A shared file is therefore safe
  between cooperating compiler processes on a local filesystem, but a fresh
  file is still required per complete build. This is not a remote signature
  or a guarantee for every network filesystem. The
  replay campaign requires exactly one record so a transformed-only failure
  has a unique denylist site. New manifests can be checked directly:

      python3 util/verify_hydra_transform_manifest.py hydra-manifest.jsonl

  Eligibility is deliberately bounded. A pure linear arm has one to four
  blocks. An internal-tree region has one to seven blocks, at most three
  conditional branches and four merge-leaf edges per arm; all non-root blocks
  have one parent, tree-local reconvergence is forbidden, and all leaves reach
  one common merge. F287 separately accepts a reducible acyclic SESE DAG with
  one to ten blocks, at most four conditional branches, eight final-merge
  leaf edges, three multi-predecessor local merges, eight local PHIs and
  64 flattened instructions per arm. It uses the nearest common
  post-dominator as the unique external merge and requires exactly one outer
  predecessor for each root, all other predecessors to stay in the same arm,
  strict forward topological edges, disjoint arms and at least one true local
  merge. Local PHIs are predicated from exact incoming-edge guards before
  their block's ordinary instructions are aligned. Block addresses, escaping
  arm SSA, call/invoke, atomic/volatile or unsupported instructions remain
  forbidden. Loops, exception edges, external arm predecessors, an empty
  alignment or any per-schema budget violation retain their original CFG.
  Inserted selects carry `!symcc.hydra_select`; they preserve ITE dataflow but
  do not become independent `_sym_push_path_constraint` sites. Ordinary source
  selects are unchanged.

- SYMCC_TACE=0/1 (default 1 in the adaptive MPI worker): Enable a two-stage
  TACE-style concrete fast path for large ordinary inputs. The first encounter
  of an input runs QSYM's bounded no-solve dependency profiler; the worker
  caches a sparse focus set by content digest and only symbolizes those bytes
  in the solving execution. An empty/failed profile falls back to full
  symbolization. Explicit target replay and pre-partitioned work bypass this
  path so their symbolic domain is not narrowed.

- SYMCC_TACE_MIN_BYTES=N (default 4096), SYMCC_TACE_PROFILE_TIMEOUT=N
  (default 5 seconds), SYMCC_TACE_CACHE=N (default 2048): minimum input size,
  dependency-profile deadline, and per-worker content-cache bound for the TACE
  path.

- SYMCC_WORKER_DIVERSITY=0/1 (default 0) and SYMCC_FOCUS_PARTITIONS=N
  (default 8): Split large seed work into disjoint byte-focus partitions and
  assign different bounded solver profiles to workers. Unsent partitions stay
  in the carried-work queue so scanning the same seed does not discard them.

- SYMCC_DENSITY_BALANCE=0/1 (default 0): When worker diversity is enabled,
  perform a bounded no-solve dependency-density profile before partitioning.
  Hot input bytes are isolated into narrower partitions; failures and exhausted
  per-round profiling budgets fall back to equal-width splitting.

- SYMCC_KSCHED=0/1 (default 0): Add a K-Scheduler-style rarity frontier score
  to candidate seeds. The coordinator obtains bounded afl-showmap edge sets,
  weights each observed edge by `1 / (frequency + 1)`, caches the score by input
  digest, and gracefully returns zero when the showmap budget is unavailable.

- SYMCC_BRANCH_SHARE=0/1 (default 0): Enable BSFuzz-style sharing of timed-out
  branch sites. Each worker writes `SYMCC_TIMEOUT_OUT`; the coordinator merges
  these sites into `.skip_sites`, and later workers consume it through
  `SYMCC_SKIP_SITES`. This skips repeated expensive attempts but remains opt-in
  because a site-level timeout summary is coarser than a full constraint
  context.

- SYMCC_TIMEOUT=SECONDS (default 30 in the MPI helper): Per-work-item execution
  deadline. The worker reports timeout/killed and the original signed return
  status in engine-neutral telemetry.

- SYMCC_STATIC_DEPENDENCE_OUT=<path> (compile time): Emit a zero-execution
  LLVM dataflow summary mapping branch/select/switch site ids to statically
  known input-byte intervals. The analysis recognizes common stream/socket
  input APIs and `_sym_make_symbolic`, propagates constant-GEP loads through
  SSA, and omits unknown offsets rather than inventing dependencies.

- SYMCC_STATIC_DEPENDENCE=<path> (MPI master): Load the static summary. Once a
  prefix trace identifies the static site behind an open branch, targeted
  replay receives that site's sparse focus set before another solver attempt.

- SYMCC_STATIC_FOCUS=0/1 (default 0): Aggressively use the union of all bounded
  static dependencies as the initial focus set before execution feedback. This
  is opt-in because indirect input wrappers or unknown offsets can make a
  whole-program static summary incomplete.

- SYMCC_EDGE_DEPENDENCE=0/1 (default 1): Maintain a SYMCTS-style
  edge-dependence coverage matrix for the concolic side. The coordinator tracks
  min/max branch-count cells per branch-pair context and schedules corpus inputs
  from under-explored rows when AFL is not providing enough fresh work.

- SYMCC_EDGE_DEP_BRANCHES / SYMCC_EDGE_DEP_CELLS / SYMCC_EDGE_DEP_TRACE
  (defaults 4096 / 262144 / 128): Bounds for the edge-dependence scheduler:
  retained branch rows, retained branch-pair cells, and maximum telemetry trace
  entries consumed per execution.

- SYMCC_DIRECTED_SITES=ID[,ID...] (default empty): Optional directed hybrid
  mode. Prefix-DAG nodes whose branch site id matches this set get additional
  replay priority, and seeds whose telemetry reaches a target site receive a
  contextual scheduling bonus. Values may be decimal or 0x-prefixed integers.

- SYMCC_DIRECTED_DISTANCE=<path> (default empty): Optional directed hybrid
  distance map. The file may be JSON (`{"distances":{"site":distance}}`) or text
  lines such as `0x401234 3.5`; seeds reaching lower-distance sites receive a
  stronger scheduling bonus. `benchmark/run_benchmark.py --directed-distance`
  sets this variable.

- SYMCC_DYNAMIC_COLORATION=0/1 (default 1): Enable coordinator-side
  ColorGo-style dynamic feasibility. Prefix-DAG nodes keep an online
  color_feasibility estimate, a cost-aware MDP value, target infeasibility
  streaks, and solver-cost pressure derived from branch telemetry. The MPI
  scheduler uses those values to favor prefixes that still appear target
  feasible and to demote expensive/stale prefixes. This is a soft scheduling
  signal by default; QSYM hard pruning still requires SYMCC_DIRECTED_PRUNE.

- SYMCC_COLORGO_GAMMA (default 0.82): Discount used by the PrefixDAG Bellman
  backup when propagating child frontier value to parent prefixes.

- SYMCC_COLORGO_MIN_FEASIBILITY (default 0.04): Reporting threshold for
  snapshot counts of dynamically feasible prefixes.

- SYMCC_TACO=0/1 (default 1): Enable TACO-Fuzz-style target-centric seed
  selection inside the prefix DAG. The coordinator tracks target-path visits,
  target-distance progress, and path reward, then boosts under-explored
  near-target paths instead of ranking only by raw seed freshness.

- SYMCC_TACO_EXTENDED_CONDITIONS=0/1 (default 1): When a seed is selected for
  targeted replay, batch same-seed high-queue open branches into the S2F
  actionseed. This approximates TACO-Fuzz's extended path conditions: the
  runtime receives multiple target-centric branch actions for one execution
  and can solve/sample them as their prefixes are reached.

- SYMCC_MULTIGO=0/1 (default 1): Enable MultiGo-style multi-path optimization.
  PrefixDAG maintains per-site execution frequency and estimates target-path
  difficulty with a Poisson exploration model. Path scheduling combines
  difficulty, under-exploration, target distance, and prior reward so the
  hybrid loop can alternate between easy target-reaching paths and harder
  non-optimal paths that preserve target-directed diversity.

- SYMCC_MULTIGO_POISSON_SCALE (default 3.0): Scale parameter used when
  converting site frequency into Poisson exploration probability for path
  difficulty.

- SYMCC_MULTIGO_EXPLORE_FRACTION (default 0.35): Fraction of PrefixDAG
  selection epochs that emphasize difficult/under-explored target paths rather
  than near-target exploitation.

- SYMCC_DIRECTED_PRUNE=0/1 (default 0): Runtime directed pruning for QSYM.
  When enabled with SYMCC_DIRECTED_DISTANCE, the solver skips Z3 attempts for
  branch sites whose static distance is greater than SYMCC_DIRECTED_MAX_DISTANCE.
  Coverage bookkeeping still runs; only testcase generation for pruned sites is
  suppressed.

- SYMCC_DIRECTED_MAX_DISTANCE (default 32.0): Static distance threshold used by
  SYMCC_DIRECTED_PRUNE. Set it to 0 for target-block-only solving, or increase
  it to keep a wider target frontier.

- SYMCC_DIRECTED_PRUNE_UNREACHABLE=0/1 (default 0): If enabled, QSYM also skips
  branch sites absent from the directed distance map once the map has at least
  one valid row. This is aggressive and is intended for complete whole-program
  coloration maps.

- SYMCC_COLOR_TARGETS=<spec[,spec...]> and SYMCC_COLORATION_OUT=<path>
  (compile-time): Emit a ColorGo-style static distance sidecar while compiling a
  SymCC target. Specs may be function names, `file:line` source locations, or
  numeric site ids. The compiler builds a module-level CFG plus direct-call and
  bounded indirect-call over-approximation, computes reverse distance to the
  targets, and writes `site distance` rows that can be fed to
  SYMCC_DIRECTED_DISTANCE. The sidecar also contains comment-prefixed block,
  call, entry/exit, and site summaries; util/merge_directed_distance.py merges
  multi-module fragments into a whole-program distance map. The benchmark
  wrapper's `--directed-targets` option runs this merger per built-in target and stores
  `<target>.directed_distance` beside the binary.

- SYMCC_CONCURRENCY_OUT=<path> (compile-time): Emit Schfuzz-style
  concurrency guidance. The compiler identifies pthread/C11 thread lifecycle
  calls, mutex/rwlock/condition/barrier/semaphore calls, LLVM atomic loads,
  stores, rmw/cmpxchg, and fences. The sidecar contains `#CONC` annotation rows
  and numeric `site distance` rows for conditional branches that can reach those
  concurrency sites.

- SYMCC_CONCURRENCY_GUIDANCE=<path> (default empty): Load a concurrency
  guidance sidecar in the adaptive coordinator. Prefix-DAG and ordinary seed
  ranking treat lower-distance branch sites as higher priority, complementing
  directed target guidance without requiring a deterministic thread scheduler.
  The coordinator also maintains a hierarchical concurrency replay layer:
  seeds that reach lower-distance concurrency frontiers are replayed first, and
  their open opposite branches are targeted before falling back to ordinary
  edge-dependence replay.

- SYMCC_COLOR_INDIRECT=0/1 (default 1) and SYMCC_COLOR_INDIRECT_LIMIT (default
  64): Control ColorGo-style indirect-call over-approximation. The compiler adds
  address-taken functions with compatible call signatures as possible callees,
  capped per indirect call by the limit.

- SYMCC_TASK_GRAPH_OUT=<path> (compile-time): Emit the block, function, call,
  entry/exit, and branch-site summaries needed for DynamiQ-style structural
  task allocation even when no directed target is configured. Multi-module
  fragments can be merged with util/merge_directed_distance.py.

- SYMCC_TASK_GRAPH=<path> (default SYMCC_DIRECTED_DISTANCE when set): Load a
  compiler task graph in the adaptive coordinator. Mutually recursive functions
  are collapsed into deterministic call-graph regions; branch telemetry maps
  prefix targets and corpus inputs to those regions.

- SYMCC_STRUCTURAL_TASKS=0/1 (default 1): Enable feedback-driven structural
  worker ownership when a task graph is available. Every branch-bearing region
  has an owner, productive and under-explored regions receive more workers, and
  completed-run reward, cost, coverage gain, and stagnation trigger periodic
  reallocation. Unknown tasks remain globally runnable and a heavily backlogged
  queue permits controlled work stealing.

- SYMCC_TASK_REBALANCE_INTERVAL (default 30 seconds): Minimum interval between
  structural ownership recomputations. A change in the active-worker limit
  forces an immediate recomputation.

- SYMCC_TASK_CORPUS_PER_REGION (default 8): Number of recent productive seeds
  retained in each structural region's persistent feedback state.

- SYMCC_PATH_COVER=0/1 (default 1 when a task graph is available): Enable
  Empc-style path prioritization. Function-local CFG loops are collapsed into
  SCC nodes, multiple minimum path covers are computed with maximum bipartite
  matching, and prefix targets receive a score based on active-cover support
  and uncovered components. Runtime traces narrow the covers compatible with a
  seed. UNSAT, timeout, and stale targeted paths retire incompatible covers and
  boost predecessor branch states found by bounded dependence traversal.

- SYMCC_MPC_COVERS=N (default 8): Maximum number of distinct minimum path
  covers retained per function. Alternatives are enumerated with bounded
  matched-edge exclusion, avoiding full path enumeration.

- SYMCC_MPC_FUNCTION_NODES=N (default 4096): Maximum basic blocks analyzed in
  one function for path-cover construction. Larger functions keep the ordinary
  PrefixDAG policy rather than blocking compilation or coordinator startup.

- SYMCC_REPLAY_COOLDOWN (default 30): Minimum seconds before a productive or
  difficult seed can be replayed when no fresh cross-seeds are available.

- SYMCC_DAG_REPLAY_SHARE (default 0.25, range 0.0-0.75): Reserve this fraction
  of active SymCC worker capacity for explicit prefix-DAG targets even while AFL
  is still producing fresh queue entries. This prevents the symbolic side from
  sleeping behind local pruning without letting replay consume all workers.

- SYMCC_TARGET_BRANCH (default empty, normally coordinator-managed): Decimal
  prefix-sensitive open-branch identifier to solve during this execution. The
  QSYM runtime sets target_reached in its telemetry when the exact path prefix
  and opposite branch are encountered. Direct use is intended for experiments;
  mpi_fuzzing_helper.py assigns targets automatically.

- SYMCC_OBJECT_TRANSPORT=0/1 (default 1): Send MPI work inputs as SHA-256
  content-addressed objects. Workers materialize missing objects locally, which
  removes the assumption that every rank can dereference the master's filesystem
  path. If disabled, the helper falls back to path-based transport.

- SYMCC_MAX_TRANSPORT_INPUT (default 16777216): Maximum input size, in bytes,
  sent through the content-addressed MPI object protocol. Oversized inputs fall
  back to path-based dispatch on same-node runs.

- SYMCC_BITMAP_DELTAS=0/1 (default 1): Synchronize AFL coverage from master to
  workers using versioned sparse byte-bit deltas. Workers receive a full bitmap
  snapshot only when they fall behind the bounded delta journal or when this
  option is disabled.

- SYMCC_BITMAP_HISTORY (default 64): Number of bitmap delta versions retained
  by the master before forcing lagging workers to refresh from a full snapshot.

- SYMCC_BITMAP_SHARDS=N (default 1): Partition the master's sparse bitmap delta
  journal by AFL bitmap index. Payloads remain equivalent to the unsharded
  bitmap stream; sharding bounds per-journal state and prepares distributed
  coordinators that own disjoint coverage partitions.

- SYMCC_PERSISTENT_STATE=0/1 (default 1), SYMCC_STATE_SHARDS=N (default
  min(64, worker count)): Persist analyzed input SHA-256 digests in deterministic
  shard logs under the SymCC output directory. Restoring these logs avoids
  immediately re-analyzing the same corpus after helper restarts.

- SYMCC_STATE_PARALLEL=0/1 (default 1), SYMCC_STATE_TASK_SHARDS=N (default
  min(256, 4*worker count)), SYMCC_STATE_STEAL_WINDOW=N (default 64): Enable
  seed-replay task sharding in the MPI master. A work
  item is identified by immutable input digest/path, focus slice, target branch,
  and S2F actionseed; the coordinator hashes that state into deterministic
  shards, assigns shard owners to workers, prefers owner-local dispatch, and
  permits bounded work stealing from the ready queue. State-task reward and
  leases are persisted in `.state_tasks.json`. Future live-state engines may
  attach a canonical `symcc-live-continuation-v1` descriptor containing PC
  frames and content-addressed path/store/memory roots; current MPI replay mode
  still does not suspend a process or transport concrete symbolic-memory pages.

- SYMCC_RESUME=0/1 (default 0): Allow mpi_fuzzing_helper.py to reuse an existing
  SymCC output directory. When enabled, scheduler state, analyzed-hash shards,
  state-task shards, and unfinished work leases are restored instead of aborting.

- SYMCC_WORK_LEASES=0/1 (default 1) and SYMCC_WORK_LEASE_TTL (default
  max(120, 4*SYMCC_TIMEOUT) seconds): Persist dispatched but unfinished MPI work
  items in an append-only recovery journal. On resume, stale leases whose input
  files still exist are requeued before fresh AFL seeds.

- SYMCC_MULTI_MASTER_LEASES=0/1 (default 0): Enable a shared fenced lease table
  for deployments with multiple MPI masters/coordinators writing to the same
  SymCC output tree. Before dispatch, a master must atomically claim the work id
  and receive a fencing token. Worker results complete the shared lease only if
  that token still matches, so a stale master cannot mark work done after another
  master has stolen the expired lease.

- SYMCC_MULTI_MASTER_LEASE_DIR=PATH (default
  "$AFL_OUT/<symcc-name>/.work_lease_table"): Directory for the shared fenced
  lease table. Each work id is stored in a deterministic shard as a small JSON
  record; short-lived per-work lock directories serialize claim/complete
  updates, while long-running worker executions are protected by fencing tokens
  rather than filesystem locks.

- SYMCC_MULTI_MASTER_LEASE_SHARDS=N (default 256), SYMCC_MASTER_ID=ID (default
  hostname:pid), and SYMCC_MULTI_MASTER_LOCK_TTL=SECONDS (default 30): Tune the
  shared lease shard count, owner identifier, and stale update-lock cleanup
  threshold. Active leases are heartbeated by the master at roughly one third of
  SYMCC_WORK_LEASE_TTL, capped at 30 seconds.

- SYMCC_COVERAGE_GOSSIP=0/1 (default 1 when multi-master leases are enabled):
  Use persistent coverage-owner shards for final AFL bitmap novelty decisions.
  Each candidate bit is committed under a short shard lock against one
  authoritative OR-state, making hit-count bucket novelty globally unique even
  when coordinators triage identical candidates concurrently. Coordinators
  periodically pull newer shard epochs into their local bitmap and worker delta
  journals.

- SYMCC_COVERAGE_OWNER_DIR=PATH (default
  "$AFL_OUT/<symcc-name>/.coverage_owner") and
  SYMCC_COVERAGE_OWNER_SHARDS=N (default max(16, SYMCC_BITMAP_SHARDS)):
  Shared location and shard count for authoritative coverage state. The current
  implementation requires a filesystem with atomic mkdir/rename semantics.

- SYMCC_COORDINATOR_INDEX=N (default 0), SYMCC_COORDINATOR_COUNT=N (default 1),
  and SYMCC_COVERAGE_OWNER_TTL=SECONDS (default 30): Identify coordinators and
  control heartbeat failover. Shard modulo coordinator count names the preferred
  live owner; another coordinator may proxy an OR-commit while holding the
  shard lock, preserving progress when the preferred owner is unavailable.

- SYMCC_DPOR=0/1 (default 0): Enable bounded schedule exploration for pthread
  targets in the MPI helper. The master injects util/symcc_schedule_rt.c through
  LD_PRELOAD for worker executions, records synchronization traces, and queues
  logical-thread-id replay prefixes for dependent scheduling points on the same
  mutex/rwlock/condition/join object. This is a fuzzing-oriented bounded-DPOR
  layer: it seeks coverage-diverse interleavings and deliberately bounds depth,
  backtracking window, and pending queue size rather than attempting exhaustive
  model checking. When `SYMCC_DPOR_MEMORY`/`SYMCC_SCHEDULE_MEMORY` are enabled,
  the Python explorer also consumes compiler-emitted `read`/`write` trace rows,
  annotates them with SC vector-clock happens-before and locksets, and can
  generate causal source-set replay prefixes for unprotected memory conflicts.
  Explorer state schema v4 persists bounded sleep sets, ordered wakeup-tree
  leaves, observed Mazurkiewicz-equivalence digests, and ConDPOR-style revisit
  identities. Each schedule artifact contains checked
  `symcc-bounded-source-dpor-v1`, `symcc-bounded-wakeup-tree-v1`, and
  `symcc-bounded-condpor-graph-v1` certificates. This remains a bounded fuzzing
  mode: it does not claim unbounded soundness, completeness, or optimality.

- SYMCC_DPOR_WAKEUP_TREE=0/1 (default 1): Enable ordered bounded wakeup-tree
  insertion. The checker implements the Optimal-DPOR weak-initial recursion
  over deterministic per-thread next events, rejects sleep-set and earlier-leaf
  equivalents, and consumes cooperative runtime-ready snapshots when complete
  evidence exists. This proves only the recorded bounded-tree invariants, not
  whole-program Optimal-DPOR optimality.

- SYMCC_DPOR_CONDPOR_GRAPH=0/1 (default 1): Build the bounded execution graph
  used for ConDPOR-style backward revisits. The graph records stable nodes,
  program order, observed/inferred read-from, per-object coherence, add order,
  causal-successor deletion, deterministic bounded maximal extensions, and
  cross-trace revisit identities. Revisit replay prefixes share the existing
  Source-DPOR queue. Changed read values may alter later control flow, so
  observed suffix restoration is evidence for this bounded trace only and is
  not a complete ConDPOR interpreter.

- SYMCC_SCHEDULE_PRELOAD=PATH (default auto-detect build/libsymcc_schedule_rt.so):
  Path to the native schedule runtime used when SYMCC_DPOR=1. The runtime
  intercepts pthread_create, mutex lock/trylock/unlock, rwlock rd/wr/unlock,
  condition wait/signal/broadcast, join, detach, and cancellation. It writes
  "seq tid op object"
  rows to SYMCC_SCHEDULE_TRACE and consumes one tid per line from
  SYMCC_SCHEDULE_PREFIX. Created threads receive monotonically allocated logical
  ids. The same logical id is used as the object for `create`,
  `create_success/create_fail`, `thread_start/thread_exit`, join/detach/cancel
  outcomes, and `thread_retire`, avoiding process-address or opaque-pthread-
  handle identity in lifecycle constraints. The fixed 4096-entry mapping table
  reserves a logical identity before create, binds the handle after success,
  releases joinable entries after successful join, and releases detached
  entries only after both detach and exit. `join_cancelled` preserves the target
  mapping so another thread can still join it.

- SYMCC_DPOR_MEMORY=0/1 (default 0 at compile time): Ask the SymCC compiler
  pass to insert `_sym_notify_schedule_read/write` calls around non-atomic,
  non-volatile LLVM loads and stores. This is intentionally separate from
  SYMCC_DPOR because memory tracing can be very high overhead.

- SYMCC_SCHEDULE_MEMORY=0/1 (default 0 at runtime): Enable the schedule preload
  runtime to turn compiler-emitted memory notifications into `read`/`write`
  trace rows. `SYMCC_DPOR_MEMORY=1` at runtime is also accepted as a shorthand
  for this switch. Without the preload runtime these notification calls resolve
  to no-op functions in the normal SymCC runtime.

- SYMCC_SCHEDULE_MEMORY_BYTES=N (default 8, maximum 4096): Maximum number of
  byte-granular objects emitted for one load/store notification. Byte-granular
  rows let the Python HB/lockset analyzer identify overlapping memory
  conflicts while bounding trace growth.

- SYMCC_SCHEDULE_MEMORY_FILTER=none|stack|owner|shared|dynamic|all (default
  none): Optional provenance filters for compiler-emitted schedule memory
  notifications. `stack` suppresses accesses whose address falls in the current
  thread's pthread stack range. `owner`, `shared`, and `dynamic` enable a
  bounded dynamic ownership table: first same-thread accesses are remembered but
  not logged; when a different logical thread first touches the same byte, the
  runtime marks it shared and emits a compressed prior-access row plus the
  current row when at least one side is a write. `all` combines stack and owner
  filtering. These filters reduce trace volume for experiments; they are not a
  sound alias/provenance analysis.

- SYMCC_SCHEDULE_MEMORY_STACK=0/1 and SYMCC_SCHEDULE_MEMORY_OWNER=0/1 (default
  0): Explicit aliases for enabling the stack and dynamic-owner filters without
  parsing `SYMCC_SCHEDULE_MEMORY_FILTER`.

- SYMCC_SCHEDULE_MEMORY_PROVENANCE=0/1 (default 0): Append a compatible fifth
  trace-field tag to memory rows, such as `prov=stack`, `prov=heap`,
  `prov=module`, `prov=anonymous`, `prov=system`, or `prov=unknown`. The stack
  classification uses pthread stack bounds; the remaining classes come from a
  bounded `/proc/self/maps` lookup. `SYMCC_SCHEDULE_MEMORY_FILTER=tag`,
  `tags`, or `provenance` is accepted as a shorthand. Python trace parsing keeps
  these tags in `ScheduleEvent.tags`; schedule artifacts expose
  `provenance_counts`, and joint schedule/query validation propagates the same
  counts for benchmark stratification.

- SYMCC_SCHEDULE_MEMORY_OWNERS=N (default 65536, maximum 1048576): Number of
  entries in the dynamic owner table. Collisions beyond the bounded probe window
  fall back to logging the access, preserving evidence rather than silently
  dropping potentially shared memory events.

- SYMCC_SCHEDULE_CONSTRAINT_OUT=PATH (default empty): When SYMCC_DPOR is
  enabled, append one `symcc-schedule-constraint-v1` JSONL artifact per
  observed schedule trace. Each record contains the normalized trace digest,
  target branch, current replay prefix, bounded schedulable-event summary,
  SC/HB conflict summary, the replay prefixes generated from those conflicts,
  and checked Source-DPOR, wakeup-tree, and bounded ConDPOR execution-graph
  certificates. This artifact is for reproducible experiments and later joint
  input/schedule solving; it is not a proof of exhaustive or optimal DPOR.

- SYMCC_SCHEDULE_SMT_OUT=PATH (default empty): When SYMCC_DPOR is enabled,
  append one `symcc-schedule-smt-v7` JSONL artifact per observed schedule
  trace. The artifact stores one shared SMT-LIB2 QF_LIA base context plus a
  delta for each conflict-derived replay prefix and a ready-to-run incremental
  `push/check-sat/pop` script. `materialize_schedule_smt_query()` can combine
  the base and one delta into a standalone query. Hard constraints encode a
  position permutation, memory-model-aware program order, exact next-event bindings for
  the replay thread prefix, reversal of its source conflict, complete
  mutex/rwlock critical-section nonoverlap, and condition-wait mutex
  release/reacquire lifetimes. Complete thread evidence additionally requires
  create before child start and target exit before successful join return.
  Vector-clock happens-before edges and
  signal/broadcast wake explanations are emitted as optional Boolean
  assumptions because those synchronization edges or spurious wakeups may
  change under replay. F58 additionally puts bounded read-from/coherence
  constraints for tagged memory events into the authoritative base formula
  under the selected SC, TSO, or RA subset. General runtime enabledness,
  unobserved aliases, and untagged concrete values remain outside the formula,
  so SAT means bounded model admissibility rather than concrete schedule
  reachability. The reader accepts v1 through v7 artifacts for backward
  materialization compatibility.

- SYMCC_SCHEDULE_SMT_MAX_EVENTS=N (default 128, minimum 2, maximum 512):
  Bound the schedulable events represented by each schedule-SMT query. A replay
  candidate whose source-conflict endpoints fall outside this window is not
  emitted as a partial query; the artifact increments `dropped_query_count`
  and sets its truncation flags instead.

- SYMCC_SCHEDULE_SMT_MAX_QUERIES=N (default 64, minimum 1, maximum 512):
  Bound the conflict-derived SMT query deltas exported for one observed trace.
  Additional source-style replay candidates remain available to the DPOR queue,
  but the SMT artifact increments `dropped_query_limit_count` and sets its
  query truncation flag. The artifact stores one shared base context plus
  bounded per-candidate deltas, so this limit controls evidence volume without
  changing schedule exploration.

- SYMCC_SCHEDULE_MEMORY_MODEL=SC|TSO|RA (default SC): Select the authoritative
  bounded memory consistency constraints embedded in each schedule-SMT
  artifact. SC uses a global order and last-write read-from. TSO relaxes
  store-to-load global program order while enforcing same-thread store
  forwarding and FIFO stores. RA uses per-location modification-order ranks,
  read-from, program-order/happens-before closure, and release-write to
  acquire-read synchronization for events tagged
  `mo=relaxed|release|acquire|acq_rel|seq_cst`. Non-SC certificates cannot be
  materialized as pthread-only replay prefixes because that runtime does not
  control hardware memory propagation. RA is a research subset, not full
  C11/C++ atomics: fences, release sequences, RMW, mixed-size accesses,
  non-atomic race UB, and the global seq_cst order are not encoded.

  Schedule SMT uses the portable SMT-LIB signed-integer form for read-from
  initial-source sentinels: `(- 1)`, never the Z3-tolerated bare token `-1`.
  The same printer is used by SC/TSO domains, RA coherence, RMW/seq_cst
  constraints and Query-IR read-value bridges. Research evidence runs every
  installed backend and treats parse errors as failures; current executable
  gates agree on SC=UNSAT and TSO/RA=SAT under system libz3 and cvc5 1.1.2.

- SYMCC_SCHEDULE_SMT_MAX_MEMORY_EVENTS=N (default 32, minimum 0, maximum 64):
  Bound read/write events receiving read-from and coherence variables. Memory
  events outside this cap are recorded as truncation metadata and cannot
  support a full-memory-semantics claim for that trace. Keeping this bound
  separate from `SYMCC_SCHEDULE_SMT_MAX_EVENTS` makes weak-memory formula growth
  explicit in benchmark artifacts.

- SYMCC_SCHEDULE_SMT_SYNC_STATE=0/1 (default 1): Extend
  `symcc-schedule-smt-v7` with bounded mutex/rwlock, condition-variable, and
  thread lifecycle state. The
  exporter pairs pre-call `lock`/`trylock`/`rdlock`/`wrlock` events with their
  `acquire` or failure outcome and a matching `unlock`/`rwunlock`. Only
  critical sections whose acquire and release both occur inside the bounded
  lifecycle window become hard constraints. Incompatible complete sections on
  the same object must not overlap; two `rdlock` sections may overlap. The
  relative order of controlled lock attempts is linked to schedule `pos_*`
  variables, while lifecycle outcomes and releases use `sync_ord_*` variables.
  A `trylock_fail` busy explanation is emitted as an optional assumption and
  is not asserted by default. Open, unmatched, or truncated lifecycles are
  counted in `sync_state` metadata but do not create hard exclusion constraints,
  avoiding false UNSAT from incomplete evidence.

  `pthread_cond_wait` and `pthread_cond_timedwait` additionally emit
  `wait_mutex_release` before blocking and `wait_mutex_acquire` after a normal
  wake or timeout. The exporter closes the waiter's pre-wait mutex section and
  opens a new reacquired section. A successful `wake` receives an optional
  `cond_wake_signal_*` assumption whose integer witness must select a matching
  `signal` or `broadcast` between release and reacquire. One `signal` witness
  cannot serve two asserted wakes, while a `broadcast` witness may be reused.
  The assumption is not asserted by default, preserving POSIX spurious-wakeup
  behavior; timed-out waits never receive a signal witness. The lifecycle
  model also pairs successful create/start/exit, mapped join/detach/cancel
  outcomes, join cancellation, and explicit identity retirement events.
  A child may start before `pthread_create` returns, but never before the
  pre-call create marker; a join attempt may precede target exit and block, but
  `join_success` must follow `thread_exit`. Create and join failures, unmapped
  handles, missing exits, and truncated lifecycles are counted without adding
  hard completion constraints. A cancelled join does not consume the target or
  merge its exit clock. Complete retirement evidence requires target exit and
  the successful join, successful detach, or detached-create trigger to precede
  `thread_retire`. Vector clocks propagate parent state at `thread_start` and
  child completion only at `join_success`.

  The lifecycle window is five times `SYMCC_SCHEDULE_SMT_MAX_EVENTS`, capped at
  512, to accommodate create/start/exit/join/outcome evidence. Set this option
  to 0 to retain the F45 structural event-order model inside the v7 artifact.

- SYMCC_SCHEDULE_SMT_ORDER_ENCODING=partial|permutation (default partial):
  Select the ordering representation for `sync_ord_*` lifecycle events. The
  default `partial` mode declares unbounded integer ranks and emits only strict
  program-order, schedule-link, ownership, wake, create, and join edges. It
  omits per-event `0..N-1` bounds and the global `distinct` constraint.
  Since v6 each controlled lifecycle rank is linked by one scaled anchor
  `sync_ord_i = (L+1) * pos_j`, replacing the former quadratic pairwise links.
  The scale leaves at least L integer slots between adjacent controlled events,
  enough to embed every bounded non-controlled lifecycle event while preserving
  strict order. Any satisfying rank model therefore defines an acyclic partial
  order that can be topologically extended to a total lifecycle order. The
  schedulable `pos_*` variables remain a bounded permutation because replay
  slots require exact positions.

  `permutation` preserves the v4-style bounded all-different lifecycle model
  and pairwise links for differential validation and ablation. Artifacts record
  `lifecycle_order_encoding`, `linear_extension_semantics`,
  `order_link_encoding`, semantic-pair/actual-link counts, anchor stride, and
  bound/distinct counts. Unknown values conservatively fall back to `partial`.

  Every current artifact also contains `symcc-lifecycle-order-ir-v1` and a checked
  `symcc-lifecycle-linear-extension-v1` certificate for the observed trace.
  `schedule_linear_extension_certificate()` can consume complete `pos_*` and
  `sync_ord_*` model assignments, optionally recheck a query's replay slots and
  conflict reversal, select satisfied nonoverlap directions, construct a
  deterministic topological order, and project it to controlled logical thread
  IDs. `verify_schedule_linear_extension_certificate()` independently checks
  the event-position permutation and program order, source ranks,
  fixed/selected edges, scaled anchors, total-order preservation, query
  bindings, digest, and replay projection.

  To materialize a runtime prefix:

      python3 util/symcc_schedule_linearize.py schedule-smt.jsonl \
        --model schedule-model.json --query-index 0 \
        --prefix-out schedule.prefix \
        --certificate-out schedule-certificate.json

  The model JSON must contain `event_positions` and `lifecycle_ranks`, either
  as arrays or maps keyed by `pos_i` and `sync_ord_i`. Omitting `--model`
  materializes the embedded observed certificate. Certificates cover the hard
  lifecycle/order IR and the selected query only; optional observed-HB,
  trylock-busy, condition-wake assumptions, path feasibility, and concrete
  runtime reachability remain outside this certificate. A query whose replay
  slots or conflict endpoints include memory read/write events is still
  certifiable as an SMT order, but is marked `runtime_replayable=false`;
  the pthread prefix writer and CLI reject it because the preload runtime
  directly controls pthread scheduling points, not memory accesses.

  v7 stores an authoritative exact `base_smt2` and a hashed
  `relaxed_base_smt2` that omits complete-section nonoverlap choices. The
  relaxed base is internal to the direct solver only: after each SAT check,
  model ranks are checked against every structured choice and violated
  disjunctions are asserted as libz3 ASTs before re-checking. Only a model with
  no remaining violation can produce a certificate. External materialization
  and `incremental_smt2` continue to use the exact base.

  To solve directly with system libz3 and avoid text-model conversion:

      python3 util/symcc_schedule_solve.py schedule-smt.jsonl \
        --query-index 0 --result-out schedule-result.json \
        --certificate-out schedule-certificate.json \
        --prefix-out schedule.prefix

  Use `--eager` for the exact-base ablation, `--base-only` for the shared
  context, and `--max-refinement-rounds` to bound refinement. A
  `refinement_limit` result is explicitly non-exact and never carries a
  certificate.

- SYMCC_SCHEDULE_QUERY_VALIDATION_OUT=PATH (default empty): When the MPI helper
  launches `symcc_query_service.py` and `SYMCC_SCHEDULE_CONSTRAINT_OUT` is set,
  ask the query service to consume schedule-constraint rows and append
  `symcc-joint-schedule-query-v1` JSONL records. A record binds schedule trace
  digest/replay prefixes to matching Query IR roots, then conservatively reports
  whether the current witness observed the prefix, whether a solver assignment
  satisfies all Query IR roots, or whether the path side remains unknown/UNSAT.
  This remains the inexpensive replay-validation export path.

  For research runs requiring one solver witness, the programmatic
  `QueryStore.solve_joint_schedule_smt()` API consumes a stored Query IR query
  and a `symcc-schedule-smt-v7` artifact, then solves Query IR QF_BV, schedule
  QF_LIA, and tagged read-from byte bridges in one system-libz3 context. It
  emits `symcc-joint-path-schedule-rf-v1`, reruns the bounded Query IR evaluator,
  and independently rechecks hashes, the schedule certificate, RF selectors,
  and byte bindings. Memory trace tags use `sym-byte=N`, `init=0xNN`, and
  `value=0xNN`. Missing tags are not guessed, and the result remains a bounded
  formula witness rather than a whole-program reachability proof.

- SYMCC_DPOR_MAX_DEPTH=N (default 64), SYMCC_DPOR_WINDOW=N (default 32),
  SYMCC_DPOR_PREFIXES=N (default 256), and SYMCC_DPOR_PENDING=N (default
  4096): Bound replay-prefix length, dependent-pair scan window, per-input
  generated prefixes, and the persistent pending queue under
  "$AFL_OUT/<symcc-name>/.dpor_schedule.json".

- SYMCC_SCHEDULE_WAIT_MS=N (default 100 in the preload runtime): Maximum time a
  worker thread waits for the prefix-selected logical thread before falling back
  and continuing. This prevents replay prefixes from deadlocking when the
  selected thread is not enabled under the current input/path.

- SYMCC_SCHEDULE_ENABLED=0/1 (MPI worker default 1),
  SYMCC_SCHEDULE_ENABLED_SETTLE_US=N (default 1000, maximum 1000000), and
  SYMCC_SCHEDULE_ENABLED_MAX_THREADS=N (default 32, maximum 64): Record
  cooperative ready snapshots for controlled pthread scheduling points. A
  thread registers before entering the replay gate; the gate may wait for the
  bounded settle interval so concurrently arriving threads appear in the same
  snapshot. `complete=1` means complete relative to this bounded registry at
  that decision, not that arbitrary application threads are operationally
  enabled. Setting `SYMCC_SCHEDULE_ENABLED=0` disables these extra rows.

- Content-addressed live-state API: `util.distributed_state.LiveStateStore`
  stores versioned SHA-256 expression nodes, parent-linked solver frames,
  symbolic stores, fixed-size concrete/symbolic pages, and memory roots.
  `fork_memory()` performs page-granular copy-on-write and
  `put_continuation()` returns a checkpoint id equal to the CAS object digest.
  Inspect or compare persisted objects with:

      python3 util/symcc_live_state.py STATE_STORE inspect CHECKPOINT_ID
      python3 util/symcc_live_state.py STATE_STORE memory-diff ROOT_A ROOT_B

  Pass `--page-size N` before the subcommand when a non-default page size was
  used. The CLI verifies every digest/reference and deliberately reports
  `native_resume_supported=false`: this format does not restore a native
  instruction pointer, registers, call stack, or external resources.

- Path-dependent schedule events (enabled with the existing
  `SYMCC_DPOR_MEMORY=1` compiler instrumentation): conditional branches and
  switches emit `constraint` rows, and instrumented basic-block entries emit
  `action` rows. The preload runtime links a constraint to the last schedule
  read and records its byte width. ConDPOR backward revisit withholds a
  read-dependent constraint and its control-flow suffix for regeneration rather
  than restoring an observed suffix whose events may no longer exist.

- Operational enabledness artifacts: cooperative `ready` rows include bounded
  `offers=tid:operation:object:auxiliary` records. The Python explorer restores
  mutex/rwlock/join/wait state and embeds a
  `symcc-operational-enabledness-v1` certificate in wakeup, ConDPOR, and
  schedule-constraint artifacts. Status is three-valued
  (`enabled|blocked|unknown`); unsupported mutex types or truncated lifecycle
  evidence stay unknown. A terminal witness additionally requires an explicit
  runtime stop with no pending offers.

- Native atomic schedule tracing: the compiler instruments atomic load/store,
  `atomicrmw`, `cmpxchg`, and fence before LLVM's LowerAtomic pass. Trace tags
  preserve width, success/failure memory order, RMW operation, group identity,
  and `atomic=0|1`. Under `SYMCC_SCHEDULE_MEMORY_MODEL=RA`, the bounded model
  includes RMW immediate-predecessor atomicity, release sequences,
  release/acquire fences, seq_cst ranks, explicit non-atomic race rejection,
  and interval-aware mixed-size read-from. This remains a bounded research
  model, not a complete ISO C/C++ executable semantics.

- SYMCC_LIVE_PROGRAM=PATH (default empty): Enable executable continuation-IR
  state work in the MPI helper. PATH must contain a `symcc-live-program-v1`
  object with functions, blocks, and bounded CPS-like instructions. The master
  creates one CAS checkpoint per input seed; workers restore, execute, fork, and
  return resumable frontier checkpoints through the normal fenced state leases.

- SYMCC_LIVE_LLVM=PATH (default empty): If `SYMCC_LIVE_PROGRAM` is unset,
  lower one `.ll`, `.bc`, C, or C++ module to continuation IR in the MPI master
  and use the resulting program for live-state work. An explicitly configured
  `SYMCC_LIVE_PROGRAM` takes precedence and is never overwritten.

- SYMCC_LIVE_ENTRY=NAME (default `main`): Entry function for LLVM continuation
  lowering. Integer entry arguments up to 64 bits consume symbolic input bytes
  consecutively in little-endian order. An entry whose exact signature is
  `(address-space-0 pointer, integer size)` instead uses the bounded symbolic
  input-buffer ABI: the pointer names a dedicated memory object and the size is
  the concrete byte length of the current seed.

- SYMCC_LIVE_PLUGIN=PATH (default auto-discovered `build/libsymcc.so`) and
  SYMCC_LIVE_COMPILER_ARGS=STRING (default empty): Compiler pass and additional
  shell-quoted Clang arguments used by MPI `SYMCC_LIVE_LLVM` lowering.

- SYMCC_LIVE_PROGRAM_OUT=PATH (compiler pass, default unset): Run the
  `live-continuation-export` module pass and write either a
  `symcc-live-program-v1` executable artifact or a
  `symcc-llvm-continuation-lowering-v1` rejection report. This is normally set
  by `llvm_to_continuation.py`.

- SYMCC_LIVE_STRICT=0|1 (default 0): Turn an LLVM lowering rejection into a
  compiler fatal error. Without strict mode the rejection report remains
  inspectable and ordinary compilation may continue.

- SYMCC_LIVE_FEASIBILITY=0|1 (default 1): Before committing a symbolic
  branch/assume state, lower its CAS path-condition frames to QF_BV and query
  the configured solver. UNSAT states are pruned. Unknown, timeout,
  unavailable solver, or unsupported expression conservatively keeps the
  state and increments `feasibility_unknown`.

- SYMCC_LIVE_SOLVER_TIMEOUT_MS=N (default 1000, range 1..3600000):
  Per-feasibility-query timeout. `SYMCC_QUERY_SOLVER` selects the helper;
  otherwise the executor searches PATH and the local build tree.

- SYMCC_LIVE_INCREMENTAL_SOLVER=0|1 (default 1): Keep one
  `symcc-query-solver --server` process per live worker and key its QF_BV
  contexts by the immutable CAS solver-frame root. Two alternatives from the
  same state reuse the exact context through Z3 push/pop. When a child root is
  absent but its parent root is cached, the helper copies the parent's asserted
  formulas and parses only the new frame delta. A cold or evicted context is
  reconstructed from the complete CAS path. Server/protocol failure opens a
  per-executor circuit breaker and falls back to one-shot `--generic`; solver
  UNKNOWN remains conservative. The cache is disposable and is never part of
  checkpoint identity or correctness.

- SYMCC_LIVE_INCREMENTAL_CONTEXTS=N (default 128, range 1..65536):
  Maximum QF_BV prefix contexts retained by each live worker's solver helper.
  The helper uses bounded FIFO eviction. The MPI worker retains one
  `LiveContinuationExecutor` across continuation leases so exact and
  parent-root contexts can survive normal scheduling boundaries.

- SYMCC_LIVE_INCREMENTAL_ARTIFACTS=N (default
  `max(512,4*contexts)`, range 16..262144): Maximum temporary prefix, delta,
  and target SMT fragments retained by one executor. CAS frame metadata and
  normalized SMT fragments use related bounded LRUs. All temporary files are
  removed when the executor closes.

- Live execution results expose `feasibility_mode`,
  `incremental_context_exact_hits`, `incremental_context_parent_hits`,
  `incremental_context_rebuilds`, `incremental_context_entries`,
  `incremental_server_starts`, `incremental_server_failures`,
  `feasibility_oneshot_checks`, and SMT/frame-cache counters. These are
  per-`resume()` deltas even though the underlying worker cache persists.

- SYMCC_LIVE_MEMORY_LIMIT=N (compiler lowering default 1048576 bytes, range
  64..4194304): Maximum synthetic static-memory image produced by LLVM
  continuation lowering. Only referenced, initialized, address-space 0,
  non-TLS globals enter the image. Exceeding the bound produces a structured
  lowering rejection rather than a truncated object.

- SYMCC_LIVE_INPUT_BUFFER_LIMIT=N (compiler lowering default 65536 bytes,
  range 1..4194304): Maximum reserved capacity of an automatically recognized
  `(pointer,size)` entry input object. The effective capacity is also clamped
  by `SYMCC_LIVE_MEMORY_LIMIT` and the unsigned range of the LLVM size
  parameter. A concrete seed larger than the resulting capacity is rejected;
  reserved capacity never authorizes access beyond the current seed length.

- SYMCC_LIVE_HEAP_OBJECT_LIMIT=N (compiler lowering default 65536 bytes,
  range 1..4194304): Maximum size accepted for one direct
  `malloc(constant-size)` instance. Every accepted site receives a fixed
  synthetic slot pool and remains subject to `SYMCC_LIVE_MEMORY_LIMIT`. The
  modeled allocation is bounded-infallible; allocation-failure paths are not
  explored.

- SYMCC_LIVE_DYNAMIC_HEAP_LIMIT=N (compiler lowering default 4096 bytes,
  range 1..SYMCC_LIVE_HEAP_OBJECT_LIMIT): Physical capacity reserved for each
  slot of a dynamic-size `malloc` or `calloc` site. The requested symbolic
  size is stored separately as the object's logical bound. Zero, arithmetic
  overflow, a request above this limit, or a full site pool returns null in
  the continuation IR. Dereferences constrain both conditional liveness and
  the logical requested size; reserved backing bytes do not enlarge the
  target-visible object.

- SYMCC_LIVE_HEAP_SITE_CAPACITY=N (compiler lowering default 4, range 1..64):
  Number of simultaneously live synthetic instances reserved for each direct
  allocator call site. Fixed-size `malloc` retains the legacy infallible
  contract and reports pool exhaustion as a model-bound error. Dynamic
  `malloc`/`calloc` uses a nullable contract: a symbolic first-free selector
  returns a stable slot or null, and live/size/init expressions survive
  checkpoint migration. Every reserved slot consumes continuation
  memory-image capacity.

- SYMCC_LIVE_ALIAS_LIMIT=N (compiler lowering default 16, range 1..256):
  Maximum number of candidate addresses emitted for one symbolic memory
  operation. For a pointer PHI/select union this is the total across every
  object case, not a per-case allowance. The compiler accepts one integer
  variable offset term with a fixed nonzero scale in each provenance arm.
  Empty or larger alias sets produce a structured rejection; the address is
  never silently reduced to its concrete witness.

- SYMCC_LIVE_STATE_STORE=PATH (default
  `$AFL_OUT/<symcc-name>/.live_states`): Shared content-addressed object store
  used by executable continuation workers. The current MPI implementation
  requires every participating rank to see the same store. CAS replication for
  a non-shared filesystem is not implemented.

- SYMCC_LIVE_PAGE_SIZE=N (default 4096, minimum 64): Page size for continuation
  concrete/symbolic copy-on-write memory. A store must be reopened with the same
  page size used to create its roots.

- SYMCC_LIVE_STEPS_PER_LEASE=N (default 1000, minimum 1) and
  SYMCC_LIVE_STATES_PER_LEASE=N (default 1, minimum 1): Bound instructions and
  in-lease state expansion before resumable checkpoints return to the MPI
  frontier. Only frontier checkpoints count as generated scheduler work;
  states that halt within the lease do not inflate reward.

- SYMCC_MAX_TRANSPORT_INPUT=N (existing default 16 MiB): Also bounds a seed used
  to create an initial live continuation. Oversized live seeds are rejected
  rather than expanded into an unbounded number of input-expression objects.
  Once created, a checkpoint is self-contained and resumes even if AFL has
  moved the original queue file.

- Executable continuation CLI:

      python3 util/llvm_to_continuation.py target.ll \
        --output program.json --entry main
      python3 util/symcc_live_state.py STORE run-llvm target.c \
        --entry main --input-hex 4142 --max-steps 1000 --max-states 64
      python3 util/symcc_live_state.py STORE run-program PROGRAM.json \
        --input-hex 4142 --max-steps 1000 --max-states 64
      python3 util/symcc_live_state.py STORE resume CHECKPOINT \
        --max-steps 1000 --max-states 64

  Supported operations are `const`, `input`, `input_size`, `binary`, `unary`,
  `pointer_offset`, `load`, `store`, `heap_alloc`, `heap_free`, `assume`,
  `select`, `branch`, `jump`, `call`, `return`, and `halt`.
  Automatic LLVM lowering is intentionally narrower than the hand-authored IR:
  it supports bounded integer SSA, scalar mem2reg, PHI edge copies, select,
  switch, direct non-variadic internal calls with bounded integer/pointer
  arguments and returns, initialized static global objects, constant GEP,
  non-atomic integer load/store up to 8 bytes, and an exact
  `(pointer,size)` entry ABI. Fixed-size entry-block allocas that survive
  mem2reg are lowered as frame-local stack objects when every load has a
  dominating full-width store and all pointer offsets are constant. Direct
  `malloc` declarations with one fixed nonzero size are lowered to bounded
  fixed-capacity call-site heap pools; `free` accepts null or the exact base of
  a currently selected slot.
  A GEP with one symbolic integer offset term can be lowered when its no-wrap
  in-object candidate domain can be enumerated and the candidate count does
  not exceed `SYMCC_LIVE_ALIAS_LIMIT`. Pointer width must equal the
  DataLayout GEP index width. Pointer-valued `select` and acyclic pointer PHI
  nodes may merge supported roots, including different objects and a one-term
  symbolic GEP in each arm. Constant or one-term GEP may also follow such a
  union. The exported lowering advertises `bounded-pointer-union` when this
  path is used.
  Programs carry target endianness, initial `memory_hex`, non-overlapping
  `memory_objects={name,kind,address,size,read_only,logical_size}` metadata, and
  a `symcc-live-input-buffer-v1` descriptor when applicable. Checkpoint
  creation maps every concrete seed byte to the input object's symbolic COW
  memory and stores `@input:length`; the executor independently rechecks
  object bounds/read-only status and uses the actual seed length for input
  accesses. Stack objects additionally carry
  `{kind=stack,function,initialization=runtime-write-tracked}`. Stack stores
  persist per-byte initialization markers in the checkpoint symbolic store;
  loads require those markers and the unique active frame owned by the
  declaring function. This permits a direct callee to access caller-owned
  stack storage. Return removes only the popped depth's stack markers and SSA
  locals, so writes into a still-active caller frame survive.
  Heap objects carry
  `{kind=heap,site,slot,capacity,lifetime=runtime-alloc-free,
  allocation=bounded-pool-infallible}`. The allocator chooses the first free
  slot and persists `@heap:live:<base>`; heap stores persist per-byte
  `@heap:init:<address>` markers. Loads require both liveness and complete
  initialization. Free clears the selected slot's live marker and all of its
  initialization markers, so deterministic slot reuse cannot observe old
  contents. Pool exhaustion, double free, use after free, and uninitialized
  heap reads are rejected during execution. The validator retains backward
  compatibility for the legacy one-object
  `allocation=bounded-infallible` artifact.
  Symbolic-address loads join candidate values with finite nested ITEs.
  Symbolic-address stores perform guarded per-byte read-over-write updates;
  overlapping candidates compose rather than overwrite one another. The OR of
  valid address guards is persisted as a path condition. Each guard also
  includes the signed `alias_index_min <= alias_index <= alias_index_max`
  contract, preventing bit-vector multiplication wrap from admitting an
  `inbounds` poison path. Chained `inbounds` GEPs intersect both dynamic base
  and result intervals so an invalid intermediate pointer cannot be hidden by
  a valid final address. Non-inbounds wrapped-object aliases are conservatively
  outside the current bounded subset. Stack/heap
  initialization markers are also guarded expressions, so conditional writes
  remain correct across checkpoint resume.
  A pointer union memory operation uses `alias_cases` rather than the legacy
  single-object `aliases` list. Each case contains one object's candidate
  addresses, a nonempty list of select/PHI equality guards, and an optional
  signed alias-index interval. The executor recomputes object ownership per
  case and conjoins these guards with the numeric address condition. This
  permits cross-object finite ITE loads and guarded stores without inferring
  provenance from synthetic numeric addresses. Null load arms and read-only
  store arms contribute no valid candidate, so their selection guard becomes
  infeasible under the memory operation's domain.
  A fixed-size malloc site uses `bounded-pool-infallible` heap objects with stable
  `site`, `slot`, and `capacity` fields. Its `heap_alloc` instruction carries
  the same slot-ordered `addresses` list and capacity. Each possible returned
  slot is a guarded pointer-provenance case; therefore multiple live instances
  of one site retain independent bounds, liveness, and initialization.
  Constant or one-term symbolic GEP may be rooted after an acyclic pointer
  select/PHI or heap-pool result; the runtime address still derives from the
  real pointer SSA while the finite object alternatives are transformed in
  parallel.
  Dynamic-size malloc and calloc sites instead use
  `bounded-pool-nullable` plus
  `logical_size=runtime-allocation-size`. Their `heap_alloc` operation carries
  a symbolic size or calloc factor pair, maximum physical capacity and
  nullable contract. Calloc multiplication wrap is rejected in the target
  bit width and selected logical bytes receive conditional zero writes.
  `heap_realloc` implements a bounded in-place allocator strategy for
  non-null supported heap bases: it preserves `min(old,new)` initialization,
  invalidates newly exposed bytes, frees on zero size, and returns null while
  preserving the old object when the new size exceeds physical capacity.
  Pointer `eq`/`ne` lowering exposes allocator failure branches.
  A non-entry function with pointer arguments records
  `pointer_params=[{index,bits}]` and appends one 1-bit hidden parameter per
  pointer in `pointer_domains=[{index,parameter}]`. Every direct call carries
  matching `pointer_args` and `pointer_domains=[{index,argument}]`. The domain
  operand is a real BV expression: it ORs the actual pointer's finite
  provenance arms and ANDs each arm's select/PHI guards and signed dynamic-index
  bounds. A callee therefore requires both `formal==candidate-address` and the
  corresponding hidden domain value to be true before a memory operation.
  Pointer-returning functions additionally record `pointer_return_bits` and
  `pointer_return_domain=true`; return instructions carry `pointer_bits` plus
  `pointer_domain`, and call sites bind it through `pointer_domain_dst`.
  Generated artifacts advertise `caller-domain-pointer-certificate`.
  Caller-owned stack objects remain attached to their original active frame
  depth across callee checkpoints. Returning a callee-owned stack object is
  rejected before artifact emission.
  A function pointer formed locally from internal function constants, pointer
  casts, `select`, or an acyclic pointer PHI can be lowered to bounded
  `indirect_call` dispatch. Address-taken targets receive stable nonzero
  `function_id` values; the instruction records a BV `target`, its width, and
  up to 64 `{function,id,guards}` cases. The executor conjoins selector
  equality with select/PHI guards, checks feasibility, and forks one ordinary
  continuation frame per feasible target. Functions additionally carry
  `param_bits` and `return_bits`, while calls carry `result_bits`; validator
  and runtime both recheck this typed ABI. Generated artifacts advertise
  `bounded-indirect-call-dispatch`.
  Pointer-returning indirect targets use the same bounded dispatch. The
  compiler unions each target's finite object-return summary, transports the
  selected callee's 1-bit return-domain certificate through
  `pointer_domain_dst`, and also includes indirect call sites when summarizing
  pointer formal parameters. Every target must share the exact pointer
  parameter/domain and pointer-return typed contract.
  Direct declarations of `memcmp` and `bcmp` have a deterministic read-only
  effect summary when the length is a compile-time constant from 0 through 64.
  The compiler expands the call to ordinary byte `load`, equality, unsigned
  ordering and `select` instructions. The result is canonicalized to
  `-1`, `0`, or `1` in the declared integer width; C only specifies its sign.
  Zero length returns zero without resolving either pointer. Since the summary
  uses core continuation IR, all existing object bounds, logical input/heap
  size, liveness, initialization, pointer-union guards and solver checks remain
  active. Generated artifacts advertise
  `bounded-external-effect-summary`.
  Direct declarations and LLVM intrinsics for `memcpy`, `memmove`, and
  `memset` are also summarized when the length is a compile-time constant from
  0 through 64. They lower to ordinary byte loads/stores, so page-COW memory,
  object bounds, logical input/heap size, liveness, initialization, stack
  ownership, pointer-union guards, and caller-domain certificates retain their
  normal semantics. `memmove` snapshots every source byte before the first
  destination write. `memcpy` is accepted only when every finite
  source/destination candidate interval is statically proven disjoint.
  `memset` writes the low 8 bits of its value operand, including a symbolic
  value. Zero length performs no memory access; a declaration call still
  returns the original destination pointer. Volatile intrinsics fail closed.
  Direct declarations of `strlen`, `strcmp`, and `strncmp` use bounded
  NUL-aware summaries. A generated byte load may carry a 1-bit `guard`; its
  definedness obligation is `!guard || access_defined`, and its value is zero
  when inactive. This prevents bytes after NUL from requiring object,
  logical-length, liveness, or initialization validity. `strlen` and `strcmp`
  require termination/difference within the finite object extent and global
  64-byte bound. `strncmp` requires a compile-time `0..64` length and need not
  observe NUL when the bound is reached; zero length does not resolve either
  pointer. Generated artifacts advertise `guarded-memory-access` and
  `bounded-nul-string-summary`.
  Direct declarations of `memchr` and `strchr` produce bounded
  pointer-returning search summaries. `memchr` requires a compile-time
  `0..64` length and reads the complete declared region; `strchr` stops
  guarded reads after the first match or NUL. Both select the first match and
  attach finite source-object/offset provenance to every non-null result.
  Generated artifacts advertise `bounded-pointer-search-summary`.
  Direct declarations of `strcpy` and `strncpy` produce bounded string-copy
  summaries only when every finite source/destination object pair is proven
  distinct. All possible source bytes are snapshot before the first write.
  `strcpy` uses 1-bit guarded stores to write through the first NUL while
  preserving the inactive destination suffix. `strncpy` requires a
  compile-time `0..64` length, writes exactly that many bytes, and pads with
  zero after source termination. A guarded store requires
  `!guard || access_defined`, performs byte-wise `ITE(guard,new,old)`, and
  conditionally updates stack/heap initialization markers. Zero-length
  `strncpy` resolves neither pointer. Both calls return destination with its
  finite pointer provenance. Generated artifacts advertise
  `guarded-memory-write` when required and
  `bounded-string-copy-summary`.
  Integer `udiv`, `sdiv`, `urem`, and `srem` lower with explicit nonzero
  divisor assumptions; signed division also excludes `INT_MIN / -1`.
  Symbolic shifts lower with an unsigned `amount < bitwidth` assumption.
  `nuw` and `nsw` on add/sub/mul/shl, plus `exact` on division/right shift,
  lower to ordinary BV proof instructions followed by 1-bit assumptions.
  These assumptions are part of the content-addressed solver prefix and are
  rechecked after migration. Artifacts using them advertise
  `llvm-defined-value-guards`. Freeze of an already-defined bounded integer is
  an identity; freeze of direct undef/poison is rejected because the current
  portable IR has no stable nondeterministic-choice primitive.
  Pointer-valued loads and stores are accepted for a bounded provenance
  subset. A scalar global pointer may be initialized directly with another
  bounded data global or null. A dynamic stack/heap pointer cell must use one
  exact storage SSA value and have one pointer store that dominates its load;
  path-conditional reaching stores and non-pointer overwrites fail closed.
  Pointer-width bytes use ordinary page-COW memory, while the compiler attaches
  loaded-value equality guards to the stored pointer's finite provenance.
  Loaded data pointers can therefore continue through GEP, memory access, and
  pointer argument/return contracts. Artifacts advertise
  `bounded-pointer-memory`.

  Function-pointer cells use the same pointer-width bytes but encode the
  exporter's stable internal function ID. Scalar global initializers and exact
  stack/heap stores may therefore be loaded and dispatched through the existing
  typed `indirect_call` contract. Artifacts advertise
  `bounded-function-pointer-memory`.

  Fixed one-dimensional global pointer arrays are accepted as bounded pointer
  tables. A symbolic GEP index is first constrained by the existing finite
  alias domain; a subsequent load reconstructs all data or function candidates
  and filters them with loaded-address/function-ID equality. Artifacts advertise
  `bounded-pointer-table`.

  A pointer cell at a join may also be recovered when every direct predecessor
  contains exactly one full-width pointer store to the exact same storage value
  and there are no other stores or non-pointer overwrites to that cell. This
  bounded reaching-definition proof works for both data and function pointers
  and advertises `bounded-pointer-memory-merge`.

  LLVM `invoke` is accepted only when its call site is `nounwind`, its direct
  internal target is `nounwind`, or every target in a complete bounded indirect
  target set is `nounwind`. The call artifact carries `normal_target`; return
  transfers there through any PHI edge-copy block. Proven-dead unwind blocks
  are omitted. Artifacts advertise `bounded-nounwind-invoke`. Potentially
  throwing invokes and all executable landingpad/catch/cleanup semantics remain
  unsupported.

  Direct integer `freeze undef` and `freeze poison` lower to a typed
  nondeterministic choice. The executor persists a global dynamic-instance
  counter in the continuation symbolic store, so loop executions receive
  distinct SMT symbols and checkpoint resume preserves their identity. All
  uses of one SSA result share its expression. Artifacts advertise
  `stable-nondeterministic-freeze`. This does not yet replace the
  defined-value assumptions used for poison-producing arithmetic flags.

  Pointer-cell reaching definitions use a bounded CFG fixed point, not only
  direct predecessors. Each block carries a last-writer set and an
  uninitialized-path bit; a full exact-slot store kills the incoming version,
  while writer-free blocks union all live predecessors. This supports
  dominating defaults, nested overwrites, forwarding blocks, loop-invariant
  cells, and loop-carried full pointer stores. Acyclic and cyclic artifacts
  advertise `acyclic-pointer-memory-ssa` or
  `bounded-cyclic-pointer-memory-ssa`. Uninitialized paths,
  non-pointer/atomic/volatile reaching writers, partial writes, and storage
  expressions without exact SSA identity fail closed.

  Constant GEP chains used as pointer-cell addresses are canonicalized to a
  target-DataLayout `(base, modular-offset)` identity. Equivalent nonzero GEP
  instructions therefore share reaching definitions and advertise
  `canonical-pointer-cell-identity`; distinct offsets stay independent.
  Symbolic GEPs and alias-equivalent different bases still require exact SSA
  identity.

  Deterministic scalar external summaries cover `abs`, `labs`, `llabs`,
  `htons`, `ntohs`, `htonl`, and `ntohl` with exact integer ABIs. Absolute
  value excludes the unrepresentable signed minimum through a solver
  assumption. Network-order conversion follows the target DataLayout, not the
  host; LLVM `bswap` 16/32/64 uses the same core BV permutation. Artifacts
  advertise `bounded-scalar-external-summary`. Locale, errno, FP/libm, time,
  randomness, I/O, and user-defined external state remain unsupported.

  Scalar LLVM `ctpop`, `ctlz`, and `cttz` overloads from 1 through 64 bits are
  expanded to bounded core-BV DAGs. Artifacts advertise
  `bounded-bitcount-intrinsic`. For `ctlz`/`cttz`, the `is_zero_poison` immarg
  must be a constant i1: false defines zero as the source bit width, while true
  emits a nonzero solver assumption. Vector, VP, target-specific, and wider
  overloads remain unsupported.

  Scalar LLVM `bitreverse`, `fshl`, and `fshr` overloads from 1 through 64
  bits are expanded to core-BV permutations and advertise
  `bounded-bit-permutation-intrinsic`. Funnel shift amounts are reduced modulo
  the source width as required by LLVM. Vector/VP and target-specific bit
  manipulation intrinsics remain unsupported.

  Scalar LLVM `sadd.sat`, `uadd.sat`, `ssub.sat`, `usub.sat`, `sshl.sat`,
  and `ushl.sat` overloads from 1 through 64 bits are lowered to core-BV
  overflow predicates and min/max clamps. Artifacts advertise
  `bounded-saturating-arithmetic-intrinsic`. Saturating shifts additionally
  require `amount < bitwidth`; violation is an infeasible defined-value path.
  Fixed-point and vector/VP saturation remain unsupported.

  Scalar LLVM signed/unsigned `add/sub/mul.with.overflow` overloads from 1
  through 64 bits expose their `{wrapped-value,i1}` result through bounded
  `extractvalue` indices 0 and 1. Artifacts advertise
  `bounded-overflow-arithmetic-intrinsic`; this does not enable general
  aggregate IR.

  Integer and address-space-0 pointer `llvm.ssa.copy` preserve the operand
  value and advertise `bounded-ssa-copy-intrinsic`. Data-pointer provenance
  and typed function-pointer target sets are forwarded through the copy.
  Floating, vector, token, metadata, and nonzero-address-space overloads remain
  unsupported.

  Scalar LLVM `abs`, `smax`, `smin`, `umax`, and `umin` overloads from 1
  through 64 bits advertise `bounded-scalar-selection-intrinsic`. The
  `llvm.abs` INT_MIN flag must be a constant i1; true emits a definedness
  assumption, while false preserves INT_MIN as required by LLVM.

  Integer `llvm.expect` and `llvm.expect.with.probability` are lowered to their
  first value and advertise `llvm-optimization-hint-identity`. The probability
  form requires a constant double in [0,1]. Expected values are hints, never
  solver assumptions.

  Global, stack, heap, null, input-buffer, and finite-union pointers may be
  queried through scalar `llvm.objectsize`. Fixed objects return the exact
  remaining size from the current constant offset and artifacts advertise
  `bounded-objectsize-intrinsic`. With a constant true dynamic flag,
  pointer-size input buffers and nullable malloc/calloc objects use their
  runtime logical size, subtract the target-width pointer offset, and advertise
  `bounded-dynamic-objectsize-intrinsic`. A runtime-sized object queried with
  dynamic=false returns the minimum/maximum unknown sentinel, never allocation
  capacity. Bounded in-place realloc provenance is retained per finite pointer
  alternative through GEP/cast/select/PHI, so mixed realloc/fixed-object unions
  use each alternative's own request size on success and the configured null
  semantics on failure. All
  three control flags must be constant i1. Moving realloc, unknown
  external/custom allocations, vectors, and widths above 64 remain unsupported.

  A scalar integer `freeze` may defer poison along bounded use chains of
  bounded casts, core integer binary operations, `icmp`, and integer
  `ssa.copy`. Sources include division/remainder definedness, shift range,
  `exact`, and `nuw`/`nsw`. The compiler emits
  `ite(defined, wrapped-result, nondet)` and advertises
  `bounded-deferred-poison-freeze`; transitive chains additionally advertise
  `bounded-transitive-deferred-poison`. Deferred division uses a safe selected
  divisor so an unselected poison result cannot trigger a host divide-by-zero.
  Integer selects use path-sensitive arm definedness and advertise
  `bounded-select-deferred-poison`; acyclic PHI merges stage/commit defined bits
  on CFG edges and advertise `bounded-phi-deferred-poison`. One exact
  same-block scalar store/load pair with no other memory operation may carry a
  definedness sidecar and advertise `bounded-memory-deferred-poison`.
  Distinct pointer SSA values are accepted only when DataLayout proves the
  same stripped base and exact constant byte offset; this stronger proof
  advertises `canonical-address-memory-deferred-poison`.
  The exact store/load pair may cross at most 64 memory-effect-free CFG edges
  when every traversed block has a unique successor and its successor has a
  unique predecessor. This advertises
  `bounded-cross-block-memory-deferred-poison`; joins and cycles fail closed.
  A bounded integer poison value may cross a direct-call return:
  the function, return, and call carry `return_defined`, `defined`, and
  `defined_dst`, respectively, and the executor transports the bit while
  popping the callee frame. Artifacts advertise
  `bounded-cross-function-deferred-poison`. Indirect calls and non-integer
  returns remain defined-only. In the opposite direction, a direct-call
  integer argument may append a one-bit
  parameter described by matching `defined_params`/`defined_args` mappings;
  this advertises `bounded-cross-function-argument-poison`. The typed call
  validator checks mapping equality and one-bit widths before execution.
  These return/argument channels may cover up to 64 exact direct callsites.
  Return poison requires every call result to reach freeze; an argument channel
  passes constant true at callsites whose actual argument is known defined.
  Multi-callsite artifacts advertise
  `bounded-multicallsite-deferred-poison`.
  When a deferred-poison formal parameter reaches the callee return through a
  bounded transparent integer slice, the argument and return channels compose
  and advertise `bounded-transitive-call-deferred-poison`. This slice covers
  core integer binary operations, casts, comparisons, selects, acyclic PHIs,
  and integer `ssa.copy`; cyclic, aggregate, vector, memory-mediated, indirect,
  and mixed-use transfer still fail closed.
  A deferred-poison value may have multiple consumers when an all-use proof,
  bounded to 256 value visits, shows that every use reaches a supported freeze
  sink through the same transparent operations and direct-call/memory
  contracts. Such artifacts advertise
  `bounded-multiconsumer-deferred-poison`. Each freeze receives its own stable
  nondeterministic choice. Any ordinary consumer, cycle, unsupported use, or
  exhausted analysis budget restores the defined-only approximation.
  One exact scalar store may feed up to 64 same-address, same-type loads along
  a linear, memory-effect-free CFG version. A same-address full-width store or
  function exit terminates the version; reverse scans bind every load to its
  nearest store while allowing earlier exact loads. All loaded values must
  satisfy the all-use freeze proof. Successful artifacts advertise
  `bounded-multiaccess-memory-deferred-poison`. Unknown memory effects,
  different addresses, cycles, partial writes, and atomic/volatile accesses
  fail closed. Acyclic branches and joins are accepted within a 64-block
  budget only when a reverse all-predecessor proof resolves every load to the
  same exact store; these artifacts advertise
  `bounded-branch-memory-deferred-poison`. Path-dependent clobbers fail closed.
  A direct-predecessor merge may instead carry path-dependent definedness when
  every incoming block has one successor and its last memory effect is an
  exact full-width store. The compiler writes each store's one-bit condition
  in the corresponding edge block and advertises
  `bounded-memory-definedness-phi`. Function metadata records the load,
  destination, merge block, and incoming endpoints; the validator requires
  exactly one i1 assignment per edge followed by a jump to the declared merge.
  Incoming store values may use a validator-checked direct-call argument or
  return defined bit. This composes the F117/F118 call ABI with the edge
  contract and advertises
  `bounded-interprocedural-memory-definedness-phi`; unproven parameters,
  indirect calls, and mixed call uses are not inferred.
  Each incoming edge may traverse a bounded predecessor subgraph of up to 64
  memory-free blocks when all paths in that subgraph resolve to one exact
  store, advertising `bounded-multilevel-memory-definedness-phi`. A loop
  header may use the same contract when every entry/backedge incoming state
  has an exact full store; the header-dominating-backedge form advertises
  `bounded-cyclic-memory-definedness-phi`. A bounded backedge subgraph with
  no writer may instead carry the previous iteration's one-bit sidecar by
  assigning the defined destination to itself. Such contracts advertise
  `bounded-cyclic-memory-definedness-carry`, mark both `cyclic` and `carry`,
  and identify carry endpoints. The validator requires an exact i1
  self-identity assignment and enforces `carry => cyclic`. A store/carry
  mixture may be transferred through one final backedge only for a canonical
  direct-arm diamond: one arm ends in an exact store, the other resolves to
  carry, and both have the same conditional-branch predecessor. The edge
  emits an i1 select between store-defined and prior-defined, advertises
  `bounded-conditional-memory-definedness-carry`, and marks the endpoint
  `conditional_carry`. The validator requires exactly one self-referencing
  select arm. Store/carry arms may cross bounded unique-predecessor,
  memory-compatible forwarding chains when both chains resolve to distinct
  successors of the same conditional branch and the store chain contains the
  proven exact writer. This advertises
  `bounded-forwarded-conditional-memory-definedness-carry` and marks
  `forwarded_conditional_carry`. Multi-way joins, nested conditions, and
  multiple stores normally fail closed. A multi-way join is accepted when
  complete reaching-source tuples form exactly Store and Carry groups and
  every endpoint in each group independently maps to the same outer branch
  arm. This advertises
  `bounded-multiarm-conditional-memory-definedness-carry` and marks
  `multiarm_conditional_carry`. Distinct StoreInst sources may be coalesced
  only in the one-bit definedness domain when bounded source analysis proves
  every stored value cannot create or receive deferred poison. Each endpoint
  is still checked against its own writer, while numeric memory retains the
  actual values. This advertises
  `bounded-equivalent-defined-store-memory-carry` and marks
  `equivalent_defined_stores`. Mixed defined/poison writers are not
  coalesced. Distinct writers of the exact same poison-capable LLVM SSA value
  may also share a definedness source. The reaching source records every
  writer member so each store can independently prove its sink and propagate
  the shared condition; this advertises
  `bounded-shared-poison-store-memory-carry` and marks
  `shared_poison_stores`. Different SSA producers are never inferred
  equivalent. A strict two-level Store/Store/Carry tree may keep the two
  writer conditions distinct: exactly three singleton source groups must
  resolve to an inner two-store split and an outer store-versus-carry split.
  Because continuation selects eagerly resolve operands, the inner condition
  and both stored values must dominate the final incoming edge. The edge
  emits an inner writer-defined select followed by the outer carry select,
  advertises `bounded-nested-conditional-memory-definedness-carry`, and marks
  `nested_conditional_carry`. Four to eight singleton Store/Carry sources may
  form a deeper bounded tree when unique-predecessor ancestor analysis can
  recursively partition every leaf by a common conditional branch. Exactly
  one leaf must be Carry, the reconstructed depth must be 3--6, and every
  predicate and stored value must dominate the final incoming edge. The edge
  emits postorder i1 selects, advertises
  `bounded-recursive-memory-definedness-condition-tree`, and records
  `recursive_conditional_carry`, `condition_tree_depth`, and
  `condition_tree_leaves`. The validator reconstructs the tree from the root
  assignment and requires exact metadata, one carry leaf, no cycles, no
  unreachable recursive temporaries, and the full-binary node count.
  Non-singleton source groups without the proof below, more than eight leaves,
  greater depth, path-local eager operands, and incomplete branch partitions
  fail closed.
  F139 admits a non-singleton source group when complete source identity has
  already proved all of its endpoints equivalent and every endpoint maps each
  selected ancestor branch to the same successor. The group remains one tree
  leaf while numeric stores and post-store control paths remain distinct.
  Such artifacts advertise
  `bounded-grouped-recursive-memory-definedness-condition-tree` and mark
  `grouped_recursive_conditional_carry`; the validator requires this marker to
  imply the recursive-tree contract. A source repeated at different structural
  positions in the tree still requires a shared-leaf DAG or condition
  reduction in F139. F140 accepts the bounded Store-only case by detecting a
  source group's conflicting `branch -> successor` positions and expanding
  those endpoints into separate tree leaves that reference the same proven
  definedness condition. Expanded trees retain the 4--8 leaf and depth 3--6
  limits and still require exactly one Carry leaf. They advertise
  `bounded-repeated-source-recursive-memory-definedness-condition-tree` and
  mark `repeated_source_recursive_conditional_carry`. Repeated Carry positions,
  Boolean minimization, and unbounded/shared-node DAGs fail closed in F140.
  F141 also expands a position-conflicting no-write Carry group. Recursive
  artifacts record `condition_tree_carry_leaves`; the validator reconstructs
  the select tree and requires the actual self-reference count to match this
  field. Ordinary recursive trees require exactly one Carry leaf, while
  `bounded-multicarry-recursive-memory-definedness-condition-tree` artifacts
  mark `multicarry_recursive_conditional_carry` and require 2--8. The fixed
  depth-two F137 contract continues to require one direct root self arm.
  Multiple independent scalar cells may carry separate definedness PHIs in the
  same merge block. Header and backward scans skip another non-atomic,
  non-volatile scalar access only when target-DataLayout constant base/offset
  regions prove it disjoint: non-overlapping intervals of one base, or distinct
  static global objects. Every cell retains its own reaching-source and edge
  assignment. Participating contracts mark `multicell`, artifacts advertise
  `bounded-multicell-memory-definedness-phi`, and the validator requires at
  least two marked contracts for one merge block. Symbolic offsets, overlap,
  calls, partial writes, and unknown object identity still fail closed.
  F143 also proves two different lowerable static storage objects disjoint
  when each base is a `GlobalVariable` or entry-block static `AllocaInst`.
  These contracts additionally mark `identified_objects`, advertise
  `bounded-identified-object-multicell-memory-definedness-phi`, and require at
  least two such markers in one merge block. The marker always implies
  `multicell`. Dynamic allocas, ordinary pointer arguments, heap identities,
  noalias call results, symbolic bases, and escaping cross-function objects
  remain outside this bounded proof.
  F144 additionally recognizes two different fixed `malloc` sites when each
  call is direct, external, address-space zero, has one nonzero constant size,
  and fits `SYMCC_CONTINUATION_MAX_HEAP_OBJECT`. At least one side of the
  pair must be such a heap object; the other may be another fixed heap site or
  an F143 static object. Contracts mark `fixed_heap_objects`, advertise
  `bounded-fixed-heap-object-multicell-memory-definedness-phi`, imply
  `multicell`, and require a same-block group of at least two. Zero or dynamic
  malloc, calloc, realloc, custom allocators, repeated dynamic instances of
  one site, noalias arguments/returns, and unknown lifetime effects fail
  closed.
  F145 expands pointer `select` and acyclic pointer `phi` values into finite
  constant regions rooted in F143/F144 objects. Constant GEP offsets are
  accumulated with signed-overflow checks; each domain is limited by
  `SYMCC_LIVE_ALIAS_LIMIT` (default 16), and every region pair across the two
  domains must be disjoint. Contracts mark `finite_pointer_domains`, advertise
  `bounded-finite-pointer-domain-multicell-memory-definedness-phi`, imply
  `multicell`, and require at least two same-block markers. Cyclic PHIs,
  symbolic GEP offsets, null/unknown bases, overlapping alternatives, and
  guard-correlated overlap fail closed.
  F146 retains literal `(i1 condition, polarity)` guards for select
  alternatives. A spatially overlapping pair is excluded only when the two
  conjunctions require opposite values of the exact same LLVM condition SSA
  value. Any compatible overlap rejects the proof. Contracts mark
  `guard_correlated_pointer_domains`, advertise
  `bounded-guard-correlated-pointer-domain-multicell-memory-definedness-phi`,
  imply `multicell`, and require at least two same-block markers. PHI-edge
  correlation, equivalent-but-distinct predicates, arbitrary path
  constraints, and SMT guard reasoning remain unsupported.
  F147 also records `(PHI merge block, incoming predecessor)` guards. Two
  alternatives from different predecessors of the same merge are mutually
  exclusive; alternatives from the same predecessor remain compatible.
  Contracts mark `phi_correlated_pointer_domains`, advertise
  `bounded-phi-correlated-pointer-domain-multicell-memory-definedness-phi`,
  imply `multicell`, and require two same-block markers. Cyclic PHIs and
  inferred cross-block edge equivalence remain unsupported.
  F148 accepts one-term symbolic GEP offsets when LLVM `ConstantRange` yields
  a bounded signed index interval. Constant and scale are applied with
  overflow checks, and every possible start offset plus access width must
  remain separated. Contracts mark `symbolic_index_intervals`, advertise
  `bounded-symbolic-index-interval-multicell-memory-definedness-phi`, imply
  `multicell`, and require two same-block markers. Multi-term affine offsets
  and relational index constraints remain unsupported.
  F149 adds bounded byte-lane definedness composition for byte-aligned integer
  loads of 2--8 bytes. A reverse walk through at most 64 acyclic
  single-predecessor blocks assigns each address-order byte lane to its nearest
  non-atomic scalar store; a typed constant global initializer may supply
  lanes that no runtime store covers. Unique poison-capable store sidecars are
  combined with a one-bit AND immediately after the load. Overlapping writes
  therefore retain the older writer only for bytes not replaced by the newer
  store. Functions advertise `bounded-byte-lane-memory-definedness` and emit
  `byte_lane_memory_definedness` contracts containing `load`, `defined`,
  `block`, `bytes`, optional `initial`/`cross_block`, and an exact `lanes`
  vector. Participating stores carry `byte_lane_store` and, when needed,
  `byte_lane_defined`. The production validator checks store IDs and widths,
  adjacent sidecar definitions, complete lane coverage, the post-load AND
  dataflow, and capability/contract consistency. Branch/loop lane PHIs,
  symbolic overlap, region-copy sources, atomic/volatile accesses, unknown
  calls, non-byte-aligned scalars, and accesses wider than eight bytes remain
  unsupported.
  F150 extends the same lane schema across a direct CFG merge. Each 2--64-way
  predecessor is analyzed independently and must provide a complete lane
  vector through an acyclic unique-predecessor corridor. Its synthetic edge
  block reduces only that path's poison-capable store sidecars into the shared
  load defined destination; an edge with only defined/initial sources writes
  true. Functions advertise
  `bounded-byte-lane-memory-definedness-phi` and emit
  `byte_lane_memory_definedness_phis` contracts with `incoming` edge blocks
  and lane vectors. The validator requires each endpoint block to end in a
  jump to the declared merge, reconstructs its local AND/true transfer, and
  rejects missing lanes, cross-edge source substitution, unreferenced stores,
  or capability/contract mismatch. An uncovered lane may not cross an
  upstream multi-predecessor join; loop/backedge lane carry and recursive
  conditional lane trees remain unsupported.
  F151 adds a bounded per-lane fixed point for a single loop header. A
  2--8-byte load owns one stable one-bit state variable per address-order byte.
  Entry edges initialize each lane from a complete writer or typed constant
  global state; backedges write a new store sidecar for overwritten lanes and
  self-carry untouched lanes. The header ANDs all lane variables after the
  numeric load. This advertises
  `bounded-cyclic-byte-lane-memory-definedness-phi` and emits
  `cyclic_byte_lane_memory_definedness_phis` with `lane_defined` and complete
  per-edge `store`/`initial`/`carry` vectors. The proof is enabled only when a
  function-wide memory-effect scan shows that the modeled stores and target
  load form an alias-closed region; any additional potentially aliasing access
  or unknown memory effect fails closed. The production validator reconstructs
  every edge transfer, requires carry to read the same lane variable, checks
  store sidecars, and proves by dependency sets that the aggregate AND consumes
  every lane. Conditional partial stores, irreducible/multi-header loops,
  symbolic overlap, region copies, cross-call effects, atomics, volatile
  accesses, and widths above eight bytes remain unsupported.
  F152 recognizes one strict conditional write/carry diamond on the backedge.
  The two direct branch arms must merge at one join; exactly one arm contains
  one constant-offset partial scalar writer and the other has no aliasing
  writer. Synthetic arm-to-join edge blocks update every lane: the store edge
  writes the matching sidecar/true for overwritten lanes and self-carries the
  rest, while the carry edge self-carries all lanes. This advertises
  `bounded-conditional-cyclic-byte-lane-memory-definedness-phi` and emits
  `conditional_cyclic_byte_lane_memory_definedness_phis` with explicit branch,
  arm, join, edge, polarity, and lane-transfer metadata. The validator
  reconstructs the branch topology, both edge transfers, the join-to-header
  all-carry path, a complete non-carry seed endpoint, and the header AND.
  Forwarded arms, switches, multiple writers, nested/recursive conditions,
  multiple conditional updates, symbolic overlap, region copies, calls,
  atomics, and volatile accesses fail closed.
  F172 permits bounded forwarding corridors in the F171 double-composed tree.
  This advertises
  `bounded-forwarded-double-composed-multigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_double_composed_multigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true` plus the F171 group/composition markers. Validation
  reconstructs the actual tree before rechecking both per-group source
  differences. Branching/shared corridors, three-group composition, more than
  one override per group, symbolic overlap, region copies, calls, atomics, and
  volatile accesses fail closed.
  F153 permits up to 16 unconditional unique-predecessor forwarding blocks on
  each conditional arm. Both corridors must originate at different successors
  of the same nearest branch, remain disjoint, and terminate at the two
  predecessors of one join. Writer analysis covers the complete corridor.
  This advertises
  `bounded-forwarded-conditional-cyclic-byte-lane-memory-definedness-phi` and
  emits `forwarded_conditional_cyclic_byte_lane_memory_definedness_phis`;
  transfer metadata distinguishes branch `store_successor`/`carry_successor`
  from arm endpoints and sets `forwarded`. Validation reconstructs every jump
  and exact predecessor set for the header, corridors, and join before checking
  lane updates. Nested branches, multi-predecessor corridors, switches, cycles,
  more than 16 forwarded blocks, multiple writers, and multiarm updates fail
  closed.
  F154 recognizes one strict two-level, three-leaf conditional update tree.
  The root branch selects either one direct arm or a uniquely reached inner
  branch; the inner true/false successors form the other two direct arms. All
  three arms must merge at one join with exact predecessor/successor sets.
  Exactly two arms each contain one constant-offset partial scalar writer and
  the remaining arm is a pure carry. Each arm-to-join synthetic edge updates a
  complete lane vector, so no path evaluates another arm's writer sidecar.
  This advertises
  `bounded-multiarm-conditional-cyclic-byte-lane-memory-definedness-phi` and
  emits `multiarm_conditional_cyclic_byte_lane_memory_definedness_phis` with
  root/inner branches, route-labelled arms, exact edges, and per-lane
  store/carry sources. Validation reconstructs the complete two-level CFG,
  exact predecessor sets, two distinct writer sidecars, one all-carry arm,
  join-to-header carry, the non-carry seed, and the header AND. Forwarded
  multiarm arms, deeper or wider trees, switches, sequential updates,
  symbolic overlap, region copies, calls, atomics, and volatile accesses fail
  closed.
  F168 permits bounded corridors in the F163 mixed two-group tree. This
  advertises
  `bounded-forwarded-mixed-multigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_mixed_multigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true`, `multiple_groups=true`, `group_count=2`,
  `mixed_groups=true`, and `composed_group_count=1`. Validation reconstructs
  both complete group partitions and proves the unique leaf-local override's
  nonempty internal-set difference. Two composed groups, forwarded
  multi-carry, nested or third groups, shared or branching corridors, symbolic
  overlap, region copies, calls, atomics, and volatile accesses fail closed.
  F170 permits exactly three direct, pure, pairwise-disjoint internal groups
  in the existing 4--8-leaf tree budget. Each group has at least two leaves
  and the tree retains at least one carry leaf. This advertises
  `bounded-trigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `trigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `multiple_groups=true`, `triple_groups=true`, and `group_count=3`.
  Validation rebuilds all three complete descendant/reference partitions and
  checks every pair for disjointness. Forwarding, local overrides, nested or
  four-or-more groups, symbolic overlap, region copies, calls, atomics, and
  volatile accesses fail closed.
  F173 permits bounded unique-predecessor forwarding corridors in the F170
  three-group tree. This advertises
  `bounded-forwarded-trigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_trigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true`, `multiple_groups=true`, `triple_groups=true`, and
  `group_count=3`. Validation reconstructs every corridor and the actual tree
  before rebuilding all three complete source partitions and checking every
  pair for disjointness. Local overrides, nested or four-or-more groups,
  shared/branching corridors, symbolic overlap, region copies, calls, atomics,
  and volatile accesses fail closed.
  F174 permits exactly one partially overlapping leaf-local override in one
  of three direct groups. All groups retain at least two pure leaves and the
  eight-leaf tree retains one carry leaf. This advertises
  `bounded-composed-trigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `composed_trigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `multiple_groups=true`, `triple_groups=true`, `mixed_groups=true`,
  `composed_triple_groups=true`, `group_count=3`, and
  `composed_group_count=1`. Validation checks all pairwise-disjoint group
  partitions and the unique local source's nonempty internal-lane difference.
  Forwarding, exact/full overrides, a second composed group, nested or
  four-or-more groups, symbolic overlap, region copies, calls, atomics, and
  volatile accesses fail closed.
  F175 permits bounded unique-predecessor forwarding corridors in the F174
  composed three-group tree. This advertises
  `bounded-forwarded-composed-trigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_composed_trigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true` plus all F174 group/composition markers. Validation
  reconstructs the actual tree before rechecking all three complete
  partitions, every pairwise-disjoint relation, and the unique local source's
  nonempty internal-lane difference. Shared/branching corridors, a second
  composed group, nested or four-or-more groups, symbolic overlap, region
  copies, calls, atomics, and volatile accesses fail closed.
  F171 permits exactly one partially overlapping leaf-local override in each
  of two direct groups. Both groups retain at least two pure leaves and the
  tree retains a carry leaf. This advertises
  `bounded-double-composed-multigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `double_composed_multigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `multiple_groups=true`, `group_count=2`, `mixed_groups=true`,
  `double_composed_groups=true`, and `composed_group_count=2`. Validation
  requires the two local writers to belong to different groups and proves
  both nonempty internal-set differences. Forwarding, more than one override
  per group, three-group composition, symbolic overlap, region copies, calls,
  atomics, and volatile accesses fail closed.
  F169 permits 2--8 distinct all-carry leaves in the forwarded F166 composed
  tree. This advertises
  `bounded-forwarded-multicarry-composed-repeated-source-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_multicarry_composed_repeated_source_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true`, `composed_repeated_source=true`, `multicarry=true`,
  and the exact `carry_leaves` count. Validation reconstructs the corridor
  tree, recomputes all-carry vectors, and rechecks the composed internal-set
  difference. Multiple groups, shared or branching corridors, symbolic
  overlap, region copies, calls, atomics, and volatile accesses fail closed.
  F167 permits bounded corridors in the pure two-group F162 tree. This
  advertises
  `bounded-forwarded-multigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_multigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true`, `multiple_groups=true`, and `group_count=2`.
  Validation reconstructs the tree first and then proves two disjoint complete
  descendant/reference partitions with identical lane sets inside each group.
  Mixed overrides, nested or third groups, shared or branching corridors,
  symbolic overlap, region copies, calls, atomics, and volatile accesses fail
  closed.
  F166 permits those corridors in one F160 per-lane composed tree with exactly
  one all-carry leaf. This advertises
  `bounded-forwarded-composed-repeated-source-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_composed_repeated_source_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `forwarded=true` and `composed_repeated_source=true`. Validation
  reconstructs the actual tree before proving the pure group lane set, the
  leaf-local partial writer, and the nonempty internal-set difference.
  Forwarded multi-carry, multiple groups, shared or branching corridors,
  symbolic overlap, region copies, calls, atomics, and volatile accesses fail
  closed.
  F155 permits up to 16 unconditional unique-predecessor forwarding blocks on
  each of F154's three arms. Reverse corridor discovery must reach the nearest
  root or inner conditional branch, the three corridors must be disjoint, and
  the root's other successor must still enter the inner branch directly.
  Writer analysis covers every corridor block while lane state updates remain
  on the three endpoint-to-join synthetic edges. This advertises
  `bounded-forwarded-multiarm-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_multiarm_conditional_cyclic_byte_lane_memory_definedness_phis`.
  Each arm distinguishes its branch `successor` from its join endpoint and the
  transfer sets `forwarded`. Validation reconstructs each bounded jump chain,
  exact predecessor sets, corridor disjointness, writer membership, the
  two-writer/one-carry partition, join, seed, and header AND. A forwarded
  root-to-inner decision path, nested branches, multi-predecessor corridors,
  deeper trees, switches, and more than 16 arm blocks fail closed.
  F156 generalizes direct conditional lane updates to one strict binary source
  tree with 4--8 leaf predecessors, maximum depth 6, and at most 64 branch plus
  leaf blocks. Recursive traversal must cover the join's exact predecessor set;
  every child has its branch as the only predecessor, shared leaves and cycles
  are rejected, and only one complete root is permitted. At least two leaves
  each contain one distinct partial scalar writer and at least one leaf is a
  pure carry. Every leaf updates the full lane vector on its own synthetic
  edge. This advertises
  `bounded-recursive-conditional-cyclic-byte-lane-memory-definedness-phi` and
  emits `recursive_conditional_cyclic_byte_lane_memory_definedness_phis` with
  root, join, depth, explicit branch nodes, and lane-bearing leaf nodes. The
  validator recursively rebuilds the exact tree and actual depth before
  checking leaf edges, writer sidecars, lane assignments, join, seed, and
  header AND. Forwarded recursive leaves, repeated/grouped writers, sequential
  updates, trees outside the bounds, symbolic overlap, region copies, calls,
  atomics, and volatile accesses fail closed.
  F157 permits up to 16 unconditional unique-predecessor blocks on every
  recursive branch-to-child edge, including both decision and leaf corridors.
  The complete tree remains bounded to 64 branch, leaf, and corridor blocks.
  Intermediate blocks may not be reused by another tree edge. Leaf writer
  discovery spans its terminal corridor while state updates remain on the
  actual leaf endpoint edge. This advertises
  `bounded-forwarded-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`;
  branch targets retain actual corridor entries, each leaf records its
  `successor`, and the transfer sets `forwarded`. Validation follows real
  jumps to the next declared branch or leaf, reconstructs unique predecessor
  and corridor membership sets, recalculates tree depth, and checks writer
  membership plus all F156 lane invariants. Nested conditional corridors,
  shared or multi-predecessor blocks, more than 16 blocks per edge, and
  repeated/grouped writer sources fail closed.
  F158 accepts one grouped partial writer in an internal branch block of an
  otherwise direct F156 tree. The strict unique-parent structure must prove
  that the writer block is the ancestor of at least two leaves; exactly that
  complete descendant-leaf set references the shared writer sidecar. Group
  leaves may not contain an overriding alias writer. At least one additional
  leaf-local writer and one carry leaf remain mandatory. This advertises
  `bounded-grouped-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `grouped_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `grouped=true`. Validation reconstructs branch children, derives the
  internal writer's complete descendant set, compares it to all leaves that
  reference the repeated store ID, and requires every other store to be
  leaf-local and unique. Multiple groups, nested overrides, forwarding in a
  grouped tree, repeated leaf positions, symbolic overlap, region copies,
  calls, atomics, and volatile accesses fail closed.
  F159 permits leaves inside the single F158 group to override the internal
  source with a nearer leaf-local writer. Every override must have the same
  canonical base, constant offset, and byte width as the internal writer, so
  it completely replaces the same lane set; at least two other descendant
  leaves continue to reference the internal source. This advertises
  `bounded-repeated-source-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `repeated_source_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `repeated_source=true`. Validation derives override positions as the
  internal branch's descendants minus repeated-source leaves, requires each
  override to have one unique leaf-local store, and compares its exact store
  lane set with the repeated source. Different-range partial composition,
  multiple groups, forwarding in a repeated-source tree, non-dominating
  repetition, region copies, symbolic overlap, calls, atomics, and volatile
  accesses fail closed.
  F160 permits one partially overlapping leaf-local writer inside that group.
  Lane transfer follows nearest-source order: the leaf-local writer wins for
  covered bytes, the internal writer supplies its remaining covered bytes,
  and all other bytes carry the prior loop state. At least two pure group
  leaves must retain the same complete internal lane set, while every composed
  leaf must retain at least one internal lane and use exactly one local writer.
  This advertises
  `bounded-composed-repeated-source-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `composed_repeated_source_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `composed_repeated_source=true`. Validation reconstructs per-store,
  per-leaf lane sets and requires the composed internal set to equal the
  complete group set minus the local override lanes. Complete shadowing,
  mixed exact and partial overrides, multiple internal groups, forwarding,
  symbolic overlap, region copies, calls, atomics, and volatile accesses fail
  closed.
  F161 permits 2--8 distinct pure all-carry leaves in an F160 composed tree.
  This advertises
  `bounded-multicarry-composed-repeated-source-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `multicarry_composed_repeated_source_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `multicarry=true` and the exact `carry_leaves` count. Validation
  reconstructs every leaf and independently counts vectors whose lanes are
  all carry; the count must match the declaration and every carry leaf must
  retain the recursive tree's unique-parent and independent-edge invariants.
  Shared carry nodes, one or more than eight carry leaves, forwarding,
  multiple internal groups, symbolic overlap, region copies, calls, atomics,
  and volatile accesses fail closed.
  F162 permits exactly two direct, disjoint internal writer groups. Each
  internal writer must have at least two descendants, and its complete
  descendant-leaf set must exactly equal the leaves that reference that store
  ID. No leaf may belong to both groups or contain a local override; no third
  store source is admitted. This advertises
  `bounded-multigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `multigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `multiple_groups=true` and `group_count=2`. Validation independently
  rebuilds both descendant partitions and their lane sets. Nested, overlapping,
  forwarded, or three-or-more groups, group-local overrides, symbolic overlap,
  region copies, calls, atomics, and volatile accesses fail closed.
  F163 permits exactly one of the two F162 groups to contain one partially
  overlapping leaf-local override. Both groups still require at least two pure
  leaves. This advertises
  `bounded-mixed-multigroup-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `mixed_multigroup_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with `mixed_groups=true` and `composed_group_count=1`. Validation reconstructs
  each complete group lane set, requires the one local source to be leaf-local,
  and proves that the composed leaf retains exactly the internal lanes not
  covered by the local writer. Complete shadowing, overrides in both groups,
  exact/partial mixing, forwarding, nested or third groups, symbolic overlap,
  region copies, calls, atomics, and volatile accesses fail closed.
  F164 permits bounded forwarding corridors in the pure single-group F158
  tree. Every branch-to-child edge may contain at most 16 unconditional
  unique-predecessor blocks, with at most 64 reconstructed tree/corridor
  nodes overall. This advertises
  `bounded-forwarded-grouped-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_grouped_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with both `forwarded=true` and `grouped=true`. Validation first reconstructs
  every actual jump, predecessor set, leaf corridor, and the exact recursive
  depth, then independently proves that the internal writer's descendant set
  equals its repeated store-ID references. Repeated/composed overrides,
  multiple groups, shared or branching corridors, symbolic overlap, region
  copies, calls, atomics, and volatile accesses fail closed.
  F165 permits those bounded corridors in the F159 same-range override tree.
  This advertises
  `bounded-forwarded-repeated-source-recursive-conditional-cyclic-byte-lane-memory-definedness-phi`
  and emits
  `forwarded_repeated_source_recursive_conditional_cyclic_byte_lane_memory_definedness_phis`
  with both `forwarded=true` and `repeated_source=true`. Validation reconstructs
  the complete corridor tree before deriving the unique internal writer,
  pure descendant lane set, and exact same-range override partition. Partial
  overlap, multi-carry, multiple groups, shared or branching corridors,
  symbolic overlap, region copies, calls, atomics, and volatile accesses fail
  closed.
  A no-store path reaching the continuation entry may contribute a defined
  state for a direct scalar global with a same-type constant integer
  initializer. Internal callees do not assume that globals are reinitialized. The
  edge writes true while runtime numeric memory reads the initial image; this
  advertises `bounded-initial-memory-definedness-merge`. A constant-offset
  global aggregate subcell is also accepted when target-DataLayout address
  normalization and LLVM `ConstantFoldLoadFromConst` prove a typed
  `ConstantInt` initial value. Independently recomputed equivalent GEPs use
  the canonical-address proof; the artifact advertises
  `bounded-initial-subobject-definedness-merge` and marks both `initial` and
  `initial_subobject`. The production validator requires
  `initial_subobject => initial`. Symbolic-index subcells, stack/heap initial
  state, and undef/poison initializers are not inferred.

  Pointer-memory provenance merges a global cell's static initializer with
  all exact runtime reaching stores. Finite symbolic GEP pointer values are
  enumerated within their proven object/index domain and selected by the
  actual loaded address, advertising `bounded-symbolic-pointer-memory`.
  Artifacts containing both initial and runtime definitions advertise
  `pointer-initial-definition-merge`; data provenance and function-target
  discovery consume the same merged definition set.
  Nondeterministic identity follows the persisted F93 instance counter.
  Poison through symbolic aliasing/cyclic/multi-access memory, arbitrary
  cross-function operations, self-dependent PHIs, or multiple consumers
  remains in the defined-only subset.

  Other pointer entry signatures, a second symbolic GEP term or multi-term GEP,
  pointer/index-width-mismatched DataLayout,
  symbolic alias sets larger than the configured bound, dynamic/scalable alloca,
  stack loads without a dominating initializer, fixed-size malloc pool
  exhaustion as a target-visible failure path,
  moving realloc, realloc-null, custom allocators, arbitrary symbolic-union free,
  cyclic pointer PHI, multi-term caller-side symbolic GEP, callee-stack pointer
  escape, function pointers loaded from arguments/global/heap memory,
  recursive indirect calls, heap-graph escape through
  memory/external context,
  nested/runtime-mutated pointer tables, loop or multi-level memory merges,
  escaped pointer cells, ordered pointer comparison, vector/FP, recursion,
  exceptions, symbolic or over-64-byte memory/string/region length,
  region copies whose disjointness cannot be proven, other external calls,
  TLS/nonzero address spaces,
  atomic/volatile access, nonlinear poison propagation,
  and poison-sensitive vector/FP operations produce a rejection report or an
  explicit bounded-runtime error. Symbolic addresses outside the finite
  contract are rejected instead of concretized.
  Therefore
  `continuation_ir_resume_supported=true` does not imply arbitrary native
  instruction resume.

- Research-grade benchmark protocol:

      python3 benchmark/research_protocol.py plan SPEC.json \
        --output protocol.json
      python3 benchmark/research_protocol.py verify protocol.json
      python3 benchmark/research_protocol.py run protocol.json \
        --output-dir research_results --resume
      python3 benchmark/research_protocol.py verify protocol.json \
        --results-dir research_results

  A spec defines `targets`, named `configurations` (argv, environment,
  `cpu_cores`), `repeats`, equal `cpu_budget_seconds`, `random_seed`, and
  `phase=tuning|confirmatory`. Confirmatory plans require at least 20 repeats.
  The executor sets `SYMCC_EXPERIMENT_ID`, `SYMCC_RUN_ID`, `SYMCC_PAIR_ID`,
  `SYMCC_RESEARCH_PHASE`, `SYMCC_RESEARCH_CONFIGURATION`,
  `SYMCC_RANDOM_SEED`, and
  `SYMCC_CPU_BUDGET_SECONDS` plus `SYMCC_CPU_CORES` for child commands,
  enforces CPU affinity and per-cell wall budget, retains failures/timeouts,
  and hashes all raw artifacts. The inner benchmark uses the declared core
  count, rather than inferring it from mode/np, when recording CPU and wall
  budgets.
  Provenance includes tracked and untracked worktree content, recursive dirty
  submodules, and file or directory corpus trees; a dirty checkout is therefore
  identified by content rather than by commit id alone.
  A configuration may set `wall_grace_seconds` (default 0, maximum 3600) for
  MPI/fuzzer teardown and artifact collection after the campaign wall budget.
  It is recorded separately as `wall_timeout_seconds` and is not added to the
  campaign coverage/CPU denominator. The child command must enforce its target
  timeout at `cpu_budget_seconds / cpu_cores`; the outer executor kills the
  process group only after campaign budget plus grace.

- benchmark/run_benchmark.py --bin-dir DIR (default `OUTPUT/bin`): Build into
  or, with `--skip-build`, reuse binaries from a directory independent of the
  per-run result directory. Confirmatory protocol cells should share one
  immutable prebuilt directory and list it in the protocol `inputs`, so compile
  time is outside the run budget and the exact binaries are tree-hashed.

- benchmark/run_benchmark.py --timeseries SECONDS: Sample authoritative AFL
  edge coverage for serial, MPI, hybrid, and AFL-only runs. Every tick snapshots
  the initial corpus and all live output queues; hybrid additionally includes
  unfiltered SymCC, GRIMOIRE, and honggfuzz corpora. During the campaign it only
  creates hard links. Content de-duplication and showmap replay are deferred
  until the child campaign has stopped, so measurement does not steal its
  assigned CPUs. Target `.args` are forwarded to both execution and every
  replay. Empty/unavailable measurements are omitted instead of encoded as
  genuine zero coverage, and a final corpus point is recorded when the run
  stops between ticks. Keep snapshots on the same filesystem as the work
  directory and provision equal `wall_grace_seconds` for post-run replay.
  Nested MPI wall/per-execution/idle timeouts and AFL/hybrid initialization
  waits are capped by the runner's `--timeout`; short campaigns are never
  silently extended to historical 10s or 30s minimums.

- Paired analysis:

      python3 benchmark/analyze_ablation.py results/benchmark_data.csv \
        --timeseries results/coverage_timeseries.csv \
        --metric coverage_auc --metric edge_cov_pct \
        --baseline-mode baseline --strict-confirmatory \
        --output-dir results/analysis

  The analyzer reports total/success/failure/timeout/censored counts, paired
  median-difference bootstrap intervals, paired sign-flip randomization,
  direction-aware A12/Cliff's delta, and Holm correction. `--time-to-target N`
  adds right-censored target time from the supplied time series.

- Executable research evidence: generate and verify a versioned v2 bundle
  covering bounded Source-DPOR equivalence, joint path/schedule/RF solving,
  SC/TSO/RA litmus obligations, live-state COW/restore, weak-initial
  wakeup/ready evidence, and bounded ConDPOR graph/revisit:

      python3 util/research_evidence.py --output evidence.json
      python3 util/research_evidence.py --verify evidence.json

  The artifact records formula/input hashes, bounds, exact backend capabilities,
  expected oracles, environment, and explicit claim exclusions. A single
  available libz3 backend is recorded as such and is not called independent
  cross-solver consensus. This evidence is functional I/T evidence, not a
  replacement for equal-CPU repeated benchmark results.

- SYMCC_AFL_DATA_COVERAGE=0/1 (default 1 for --hybrid-adaptive, 0 otherwise in
  the benchmark harness): Build and inject util/afl_data_coverage_rt.c through
  AFL_PRELOAD. The preload runtime intercepts memcmp/strcmp-family calls in the
  target process and writes matched-prefix progress directly into AFL's native
  shared coverage bitmap, resolving either exported __afl_area_ptr or the
  __AFL_SHM_ID SysV shared-memory map. AFL's normal queue retention logic can
  then keep inputs that improve constant/data comparisons even when edge
  coverage is unchanged. For AFL++ PCGUARD targets the preload reserves the
  first 65536 map IDs before forkserver negotiation, so instrumented edge IDs
  start after the data namespace. Comparison sites use module-relative
  identities and therefore remain stable across PIE/ASLR processes.

- AFL_DATA_COVERAGE=0/1 (default 1 inside the preload runtime): Emergency
  runtime switch for disabling the native AFL data-coverage preload when it is
  already present in AFL_PRELOAD.

- SYMCC_AFL_DATA_MAP_SIZE=N (default 65536, range 1--65536): Narrow the hash
  range used inside the reserved native data namespace. This does not resize
  the AFL map. In particular, AFL++'s internal __AFL_MAP_SIZE is an allocation
  bound and is intentionally not used as the data hash range.

- SYMCC_AFL_HINT_MUTATOR=0/1 (default 1 for --hybrid-adaptive, 0 otherwise in
  the benchmark harness): Enable an AFL++ Python custom mutator that consumes
  SymCC hint tokens and poly-cache entries. The benchmark harness auto-detects
  AFL++ Python mutator support, sets AFL_PYTHON_MODULE to
  util.afl_symcc_hint_mutator by default, and leaves existing user settings
  untouched.

- SYMCC_HINT_DIR=PATH (default "$AFL_OUT/symcc01/extras" in adaptive hybrid
  runs): Directory watched by the AFL++ mutator for SymCC changed-byte hint
  tokens.

- SYMCC_POLY_CACHE_MUTATOR=PATH (default "$AFL_OUT/symcc01/.poly_cache" in
  adaptive hybrid runs): Poly-cache file read by the AFL++ mutator. If unset,
  the mutator falls back to SYMCC_POLY_CACHE. Rows may include a sixth
  full-matrix field in the form `lower:upper:offset=coefficient,...;...`; when
  present, the mutator samples inside the correlated linear constraints rather
  than treating byte ranges independently.

- SYMCC_HINT_MUTATOR_RESCAN=SECONDS (default 1.0): Minimum interval between
  hint/poly-cache rescans inside afl-fuzz.

- SYMCC_HINT_MUTATOR_COUNT=N (default 4, maximum 32): Number of custom-mutator
  outputs AFL++ should request for an input when hints or cache entries exist.

- SYMCC_HINT_MUTATOR_TOKENS=N / SYMCC_HINT_MUTATOR_TOKEN_MAX=N: Bound the
  number and maximum size of hint tokens scanned by the AFL++ mutator.

- SYMCC_HINT_MUTATOR_CACHE_LINES=N (default 4096): Maximum number of recent
  poly-cache lines scanned by the AFL++ mutator.

- SYMCC_HINT_MUTATOR_POLY_ATTEMPTS=N (default 128, range 8..4096): Number of
  bounded attempts used by the AFL++ mutator to recover a feasible full-matrix
  polytope point when applying a cached abstraction to an unrelated AFL seed.

- SYMCC_HINT_MUTATOR_STRING_LINES=N (default 4096): Maximum number of recent
  `symcc-string-constraint-v1` JSONL rows scanned by the AFL++ mutator when
  `SYMCC_STRING_CONSTRAINTS` or `SYMCC_STRING_CONSTRAINT_OUT` is set.

- SYMCC_AFL_PROFILES=0/1 (default 1 in adaptive hybrid when --aflpp-profiles is
  not off): Enable xFUZZ/KRAKEN-style AFL++ runtime profile orchestration. The
  runner can distribute AFL instances across power schedules, MOpt, CmpLog, and
  available AFL++ compile-time variants such as LAF/CompCov, CTX, Ngram, and
  LAF+CTX.

- SYMCC_AGENTIC_OUT=PATH (default empty): Experimental agentic-concolic hook.
  When set, the MPI master appends JSONL summaries for high-value solver tasks
  and open-prefix work. The core fuzzer does not call an LLM; this is an
  offline/export interface.

- SYMCC_AGENTIC_HINTS=PATH (default empty): Experimental JSON hints consumed by
  the MPI master. Hints are keyed by input sha256 or path and may override
  focus_bytes, focus_set, target_branch, strategy, s2f_actions, and route for a
  dispatched work item.

- SYMCC_AGENTIC_CMD=COMMAND (default empty): Optional online agentic hook. For
  each completed concolic execution with telemetry, an asynchronous backend
  sends the exported task JSON to COMMAND on stdin and expects one hint JSON
  object on stdout. Invalid JSON, non-zero exits, and timeouts are ignored.

- SYMCC_AGENTIC_BACKENDS=<JSON-or-path>: Provider portfolio for real external
  agent backends. Each entry has `type: command` plus `command`, or `type:
  http`/`chat-completions` plus `url`, optional `headers`, `protocol`, `model`,
  and `system_prompt`. Header values of the form `env:NAME` read credentials
  from the environment. Direct hint JSON, `{hint: ...}`, chat-completion
  `choices[].message.content`, and text-content envelopes are accepted. All
  outputs are reduced to the bounded scheduling-field whitelist before use.

- SYMCC_AGENTIC_TIMEOUT=SECONDS (default 2.0): Per-query backend timeout.
  Queries run outside the MPI scheduling loop and are applied on a later visit
  to the same content digest/path.

- SYMCC_AGENTIC_WORKERS (default 2), SYMCC_AGENTIC_FAILURE_THRESHOLD (default
  3), SYMCC_AGENTIC_COOLDOWN (default 30 seconds), SYMCC_AGENTIC_CACHE (default
  2048): Bound asynchronous concurrency, open a per-provider circuit breaker
  after repeated failures, and cache validated hints by canonical task digest.

- SYMCC_AGENTIC_BUILTIN=0/1 (default 1 in adaptive mode): Enable the built-in
  deterministic agentic planner. It keeps a persistent bandit-style state over
  solver strategies, target branches, and per-input route memories, then emits
  the same strategy, focus_bytes, target_branch, and s2f_actions hints as the
  external hook.

- SYMCC_AGENTIC_ROUTE=hybrid|cottontail|concollmic|gordian|off (default
  hybrid): Select the built-in planner's LLM-inspired routing policy.
  Cottontail route learns structure-local comparison-taint focus slices;
  ConcoLLMic route learns actionseed-style target solving; Gordian route sends
  solver-hostile tasks to sampling/ghost-code-style exploration. This policy is
  deterministic and does not call a model by itself.

- SYMCC_AGENTIC_STATE=PATH (default "$AFL_OUT/<symcc-name>/.agentic_planner.json"):
  State file for the built-in planner.

- SYMCC_VERIFIED_PROPOSALS=PATH (default empty): Incrementally consume JSONL
  semantic candidate proposals. Accepted kinds are inverse, surrogate,
  heap_partition, solve_complete, query_hole_completion,
  history_acquisition, targeted_transform, and semantic. A record supplies
  either `candidate: {"hex": ...}` / `{"text": ...}`, or a source_path plus
  bounded offset patches, append, and/or truncate operations. Proposals are data
  only; executable code and commands are not accepted.

  Example:
    {"kind":"inverse","source_path":"/tmp/seed","target_branch":123,
     "patches":[{"offset":4,"hex":"504b0304"}]}

  The worker executes the materialized candidate against the real target. For
  a nonzero target_branch, telemetry must report the same target id and
  target_reached=true. A verified candidate then enters normal AFL bitmap
  triage and is marked retained only if it owns globally novel coverage bits.
  Proposal state and content-addressed candidates are persisted below
  `.verified_proposals` in the SymCC output directory.

- SYMCC_PROPOSAL_PARSER=COMMAND (default empty): Optional independent parser
  validity oracle applied only after the real target/branch gate succeeds.
  `{input}` in the shell-split command is replaced with the candidate path; if
  absent, the path is appended. Exit status zero accepts syntax, any other
  status, launch error, or timeout rejects the proposal. Stdout/stderr are
  discarded. Parser acceptance never substitutes for target replay or AFL
  novelty.

  If COMMAND contains `{trace}`, it is replaced with a fresh output path and
  the parser must atomically or directly write either the v1 tree format:
    {"schema":"symcc-parser-structural-trace-v1",
     "parser":"tree-sitter-json-0.25","accepted":true,
     "nodes":[
       {"symbol":"document","state":"root","start":0,"end":12,"parent":-1},
       {"symbol":"string","state":"object-value","start":5,"end":10,
        "parent":0}]}

  `accepted` must agree with the process exit status. Nodes use half-open byte
  spans, parents must precede and contain children, labels are bounded printable
  ASCII, and the whole trace is capped at 4096 nodes/1 MiB. A malformed trace,
  an exit-status mismatch, or no node enclosing a grammar replacement span
  rejects the proposal. The smallest enclosing node contributes parser
  implementation, nonterminal/state, and ancestor chain to a stable structural
  context ID. Every node on the selected ancestry is additionally normalized as
  `symcc-parser-production-v1`: the LHS/state, ordered RHS child labels, and
  terminal-gap digests form a stable production ID. Repeated nonterminals on
  the ancestry produce mutual-recursion cycle paths; every same-symbol direct
  child produces a separate recursive slot, including multi-slot productions.
  The resulting `symcc-parser-cfg-fragment-v2` contains at most 32 productions,
  16 cycles, and 32 bounded subtree instances. Direct siblings must be
  disjoint and ancestry is capped at 32.
  At most 128 concrete bytes surrounding each descendant are retained as a
  bounded derivation template; empty, overlapping, or oversized recursion is
  not induced. Each production also has a shape ID that excludes terminal-gap
  contents. A subtree instance binds that shape and production to its complete
  yield, terminal-gap bytes, and ancestry path. Instance yields and total
  terminal gaps are independently capped at 256 bytes. If instance evidence
  would exceed the 64 KiB fragment limit, non-selected instances are
  deterministically removed first; CFG/cycle evidence is preserved whenever
  it still fits. Trace files are removed after validation; their SHA-256,
  selected symbol/state, context/production/shape/instance IDs, canonical CFG
  fragment, and bounded recursion evidence remain in proposal-state schema 12.

  F227 provides an executable persistent Tree-sitter implementation of this
  command contract. Start one service per parser/experiment:

    python3 util/tree_sitter_incremental_parser.py serve \
      --socket /tmp/symcc-tree-sitter-json.sock \
      --language-module tree_sitter_json \
      --parser-name tree-sitter-json-0.24

  Then configure the MPI master:

    SYMCC_PROPOSAL_PARSER='python3 util/tree_sitter_incremental_parser.py parse --socket /tmp/symcc-tree-sitter-json.sock --input {input} --trace {trace} --cache {cache}'

  The service requires `tree-sitter>=0.25,<0.27` and a language provider such
  as `tree-sitter-json`; the executable JSON conformance provider is listed in
  `requirements.txt`. `serve` retains at most 256 native TSTree objects and
  serializes access through a mode-0600 Unix socket. Options `--max-trees`,
  `--max-nodes`, and `--max-input-bytes` set hard bounds. Use `ping` to obtain
  cold/incremental/reused-node telemetry and `shutdown` for a clean stop.
  `SYMCC_PROPOSAL_PARSER_TIMEOUT` must cover the client RPC and parse time.

  For an incremental manifest, the service reconstructs the exact edit,
  copies the accepted base TSTree, calls `Tree.edit`, and passes that old tree
  to `Parser.parse`. A reuse receipt contains only offered base nodes whose
  native Tree-sitter node ID occurs in the new tree. Tree-sitter defines equal
  IDs across old/new incremental trees as actual node reuse. The proposal
  manager then independently rechecks each mapping's symbol, parse state,
  mapped span, epsilon flag, and candidate-yield SHA-256. A missing in-memory
  base tree is a valid cold-parse fallback; an invalid manifest, trace, or
  receipt cannot authorize a proposal.

  This adapter exports Tree-sitter's concrete syntax tree as structural trace
  v2. It is a real native incremental parser integration, but Tree-sitter does
  not expose a complete ambiguous GLR/SPPF forest; packed alternatives still
  require a parser that emits structural trace v3/v4.

- SYMCC_PROPOSAL_PARSER_CACHE=0/1 (default 1): Cost-faithfully enable the
  `{cache}` manifest path. When disabled, every parser validation is cold:
  the manager does not create a manifest, retain a trace-cache entry, or count
  a cache request even if COMMAND contains `{cache}`. This is the F228 cold
  ablation control; parser acceptance and structural trace validation remain
  enabled.

- SYMCC_PARSER_RESEARCH_ARTIFACT=PATH (default
  `$SYMCC_RESEARCH_RUN_DIR/parser_research_artifact.json` when a sealed run
  directory exists): Atomically write
  `symcc-parser-research-artifact-v1` at MPI initialization, periodic state
  saves, and graceful/finally shutdown. The canonical SHA-256 binds proposal
  state schema 12, cache mode, protocol/run/pair/configuration/seed/CPU
  metadata, manager-observed parser wall time, parser-reported native parse
  time, trace bytes, request/offer/receipt/zero-reuse counts, verified
  Tree-sitter node-ID proofs, reused/invalidated nodes, acceptance, and cache
  capacity. These metrics are audit evidence and never authorize a proposal.

  `benchmark/research_protocol.py` recognizes
  `parser_incremental_ablation`, expands `parser-cold` and
  `parser-incremental` with identical command/core/grace settings, and sets
  `SYMCC_PARSER_REQUIRE_ARTIFACT=1`. A successful run with a missing,
  corrupted, or cross-run artifact is retained as failed. Analyze verified
  scalars with:

    python3 benchmark/analyze_ablation.py benchmark_data.csv \
      --parser-artifact RESULTS_DIR \
      --metric proposal_parser_mean_wall_time_us

  Proposal state schema 12 persists cumulative counters and accepts states
  v1--v11. Restore rejects impossible request/offer/receipt/proof nesting,
  totals below their latest value, or counters above signed 64-bit bounds.

  F229 provides a real complete ambiguous-forest provider for this contract.
  A persistent Lark 1.3 generalized Earley service constructs the SPPF
  directly (`ambiguity="forest"`) instead of enumerating parse trees:

    python3 util/lark_sppf_parser.py serve \
      --socket /tmp/symcc-lark.sock \
      --grammar benchmark/grammars/target.lark \
      --start start \
      --parser-name target-lark-earley

  Configure the proposal manager with:

    SYMCC_PROPOSAL_PARSER='python3 util/lark_sppf_parser.py parse --socket /tmp/symcc-lark.sock --input {input} --trace {trace}'

  The adapter requires `lark>=1.3,<1.4`, uses byte mode and the
  `dynamic_complete` lexer so trace spans are exact candidate byte offsets and
  lexical ambiguity is retained. Symbol nodes, LR(0) intermediate items,
  packed productions, and token nodes are encoded as a forward shared DAG.
  Packed-production wrapper nodes preserve two derivations even when their
  child lists are identical. Lark's priority-stable first packed derivation is
  alternative zero; any SPPF sharing that would give this selected derivation
  multiple primary parents is cloned only along that primary projection.
  Non-primary sharing remains shared.

  Zero-width Lark subforests cannot be written directly because structural
  trace v3 requires epsilon nodes to be leaves. The adapter collapses those
  subforests, promotes the trace to v4, and emits every distinct observed
  nullable dependency as a rule for the manager's independently recomputed
  SCC/least-fixed-point certificate. More than 32 nullable rules, a cyclic
  (infinitely ambiguous) SPPF, more than 4096 encoded nodes, more than 16384
  edges, more than eight alternatives per symbol, or a trace over 1 MiB fails
  closed. These bounds guarantee that an accepted trace is complete within
  the declared representation; no partial forest is silently labeled
  complete.

  `--max-nodes`, `--max-edges`, and `--max-input-bytes` may lower the hard
  limits. The mode-0600 Unix service compiles one immutable grammar once and
  serializes requests. `ping` reports grammar digest, Lark version, accepted/
  rejected/failure counts and Earley time; `shutdown` removes the socket.
  Syntax rejection emits a valid negative trace and returns one. Internal,
  cyclic, or resource-bound failures return two and cannot authorize a
  proposal. This service is generalized Earley/SPPF in Python; it is not
  described as a native-C GLR/GLL or incremental-forest implementation.

  F233 adds an independent generalized LR provider:

    python3 util/parglare_sppf_parser.py serve \
      --socket /tmp/symcc-parglare.sock \
      --grammar benchmark/grammars/target.pg \
      --parser-name target-parglare-glr

    SYMCC_PROPOSAL_PARSER='python3 util/parglare_sppf_parser.py parse --socket /tmp/symcc-parglare.sock --input {input} --trace {trace}'

  The adapter requires `parglare>=0.21,<0.22`. `GLRParser` runs with shift,
  empty-shift, and lexical preference disabled and `build_tree=true`; its
  `Forest.result` Parent/possibility graph is encoded directly, without
  reading `Forest.solutions` or enumerating trees. Parent nodes become grammar
  symbols, each NodeNonTerm production becomes an `@packed` wrapper, terminal
  possibilities become `@token` wrappers, and shared child Parent objects
  remain shared. The manager accepts proof
  `parglare-glr-complete-sppf-v1` only with the parglare telemetry schema,
  grammar SHA-256, bounded version, and the same independently recomputed
  node/alternative/edge/nullable/cost relationships as Lark.

  Candidate bytes are decoded one-to-one with Latin-1 before GLR parsing, so
  parglare character positions remain byte offsets. Grammar authors must
  therefore express non-ASCII terminals in that byte-oriented alphabet; this
  is not Unicode-codepoint parsing. The same 4096-node, 16384-edge,
  eight-alternative, 64-child, 32-nullable-rule, and 1 MiB bounds apply.
  Cyclic SPPFs, including infinite nullable ambiguity, fail closed. This is an
  independent pure-Python GLR/SPPF oracle for differential validation, not a
  native or incremental implementation.

  F230 makes the F229 provider proof-carrying at the manager boundary.
  `forest_telemetry` must use proof `lark-earley-complete-sppf-v1` and bind a
  valid grammar SHA-256 and bounded Lark version. The manager recomputes the
  encoded node, alternative, edge, and nullable-rule counts from the validated
  trace; it also checks accepted/complete equivalence, raw/clone/encoded
  relationships, elapsed bounds, v3/v4 consistency, and rejects simultaneous
  Tree-sitter incremental and Lark forest telemetry.

  Proposal state schema 12 accumulates forest traces, complete traces, proofs,
  raw/encoded nodes, primary-only clones, packed alternatives, edges, nullable
  rules, and Earley parse time. It accepts state v1--v11; restore checks
  `complete <= proof <= forest trace <= parser validation`, size/cost bounds,
  and forest time no greater than total parser-reported time. The existing
  sealed parser artifact includes all `proposal_parser_forest_*` scalars and
  derived complete rate/mean size/mean time. The artifact also seals the
  normalized parser-command SHA-256 and the sorted set of observed grammar
  SHA-256 values; state restoration rejects forest records whose grammar
  identity is missing or changed.

- SYMCC_PARSER_FOREST_MODE=off|selected|complete: Experiment binding used by
  F230's `parser_forest_ablation`. The MPI master copies this value into parser
  artifact metadata. It does not select a parser by itself; the protocol also
  sets `SYMCC_PROPOSAL_PARSER`. The artifact verifier requires off/selected
  cells to have zero complete-forest traces and requires the metadata mode to
  match the sealed configuration.

  `benchmark/research_protocol.py` accepts `parser_forest_ablation` with one
  `base_configuration`, `selected_parser_command`, `forest_parser_command`,
  and the precomputed `forest_grammar_sha256`. It expands equal-CPU
  `parser-forest-off/selected/complete` cells, disables the F212 cache in all
  three, and requires `parser_research_artifact.json`. This is a semantic and
  cost calibration, not an incremental-parser speedup test.

- SYMCC_PARSER_CROSS_MODE=off|paired: Experiment binding for F231's
  candidate-identical dual-oracle calibration. `off` forbids paired evidence.
  `paired` requires `cross_parser_telemetry` on every observed complete-forest
  trace and copies the mode into the sealed parser artifact. The variable does
  not select either parser; `SYMCC_PROPOSAL_PARSER` must invoke
  `util/cross_parser_oracle.py`.

- SYMCC_PARSER_CROSS_PRIMARY_SHA256 and
  SYMCC_PARSER_CROSS_SECONDARY_SHA256: Protocol-generated SHA-256 identities
  of the child parser argv. The primary is normally the Lark complete-SPPF
  command and remains the proposal admission oracle. The secondary is normally
  the Tree-sitter selected-CST command and contributes calibration evidence
  only. The artifact verifier requires the observed ordered command pair to
  match these values.

  `cross_parser_oracle.py` requires exact `{input}` and `{trace}` argv tokens
  in each child command, rejects shell execution and `{cache}`, and runs the
  two child processes concurrently under independent timeouts. Return codes
  zero and one mean accepted and rejected; any other code, timeout, malformed
  trace, nested cross receipt, or output over 1 MiB fails closed. The wrapper
  binds the candidate SHA-256, canonical primary/secondary trace digests,
  parser names, acceptance bits, return codes, child command digests, and
  elapsed times.

  Proposal state schema 13 accepts v1--v12 and adds the four candidate-paired
  outcomes: both-accept, primary-only, secondary-only, and both-reject. The
  manager independently runs the ordinary v1--v4 validator on the embedded
  secondary trace, checks that the four cells sum to paired traces and that
  agreement equals both-accept plus both-reject, and persists the ordered
  command pair. The sealed artifact repeats these identities and invariants.

  `benchmark/research_protocol.py` accepts `parser_cross_calibration` with one
  base configuration plus `selected_parser_command`, `forest_parser_command`,
  `paired_parser_command`, and `forest_grammar_sha256`. It generates equal-CPU
  `selected/complete/paired` cells with parser cache disabled. The paired cell
  additionally requires one complete-forest trace per cross-parser trace.
  Aggregate acceptance rates from separate cells are not a substitute for
  this same-candidate confusion matrix.

  F232 extends proposal state to schema 14 and derives parser-neutral
  structural correspondence after both child traces have passed validation.
  For the primary it records unique non-epsilon byte spans from both the
  alternative-zero projection and the complete encoded forest. For the
  secondary it records the selected-tree spans. Repeated Symbol, intermediate,
  and packed nodes with the same yield count once; the full-input root span is
  removed when a non-root span exists. Internal byte boundaries are compared
  separately.

  The state and sealed artifact accumulate primary-selected, primary-forest,
  secondary, shared, and union span counts plus primary/secondary/shared/union
  boundary counts. Restore and artifact verification require the exact set
  identities `union = left + right - intersection`, selected spans to be a
  subset of forest spans, and structural pairs to equal both-accept pairs.
  Research metrics expose micro-averaged selected-span precision/recall/
  Jaccard, forest-span precision/recall/Jaccard, and boundary Jaccard.
  Schema-13 states migrate with their acceptance quadrants intact and zero
  historical span evidence; no unobserved correspondence is reconstructed.

  F234 extends proposal state to schema 15 with proof-carrying grammar
  correspondence. This is derived only for both-accepted child traces. The
  manager takes each validated alternative-zero projection, transparently
  removes provider-only symbols whose names start with `@`, and computes a
  recursive parser-neutral shape from `(start,end,epsilon)` plus ordered
  relative child extents. The implementation uses an explicit stack and
  remains bounded by the existing 4096-node trace limit.

  A symbol observation is retained only when one `span+shape` bucket has
  exactly one grammar node on each side. A bucket with unresolved multiplicity
  increments `parser_cross_ambiguous_symbol_spans` and contributes no guessed
  mapping. A production observation additionally requires equal, non-empty
  ordered direct-child partitions after transparent wrappers are removed.
  Consequently these counters are sample-conditioned structural evidence,
  not a declaration that two symbol names or CFG languages are equivalent.

  Every record persists canonical
  `symcc-parser-correspondence-v1` JSON and its SHA-256. Restore recomputes the
  canonical encoding, label and shape bounds, sorted unique mapping keys,
  observation sums, and
  `production_correspondences <= symbol_correspondences
   <= min(primary_symbols, secondary_symbols)`.
  Schema-1 through schema-14 states remain readable and receive zero
  historical correspondence fields.

  The sealed parser research artifact adds
  `parser_cross_symbol_correspondence` and
  `parser_cross_production_correspondence`. Entries bind both parser names,
  both symbols, production states where applicable, a production shape digest,
  and the support count. Manager and benchmark verifiers independently check
  sorting, uniqueness and sums. Metrics include primary/secondary symbol
  alignment rates and production-to-symbol alignment rate. These maps are
  observational diagnostics only; the primary child remains the sole parser
  admission oracle.

  Before interpreting a zero-disagreement paired calibration as grammar
  agreement, run a bounded exhaustive audit where the input alphabet permits:

    python3 util/parser_equivalence_audit.py \
      --primary-command "PRIMARY ... {input} ... {trace}" \
      --secondary-command "SECONDARY ... {input} ... {trace}" \
      --alphabet-hex 002c3a6162 \
      --max-length 4 \
      --counterexample-limit 32 \
      --output parser_equivalence_artifact.json

  Enumeration is shortlex and includes the empty input. The alphabet contains
  1--16 distinct bytes and is canonicalized into ascending byte order. The
  exact domain `sum(|alphabet|^i, i=0..max_length)` cannot exceed 65536.
  Every case uses the ordinary paired wrapper and manager structural validator.
  Any timeout, child internal return code, malformed trace, invalid provider
  proof, or incomplete enumeration exits 2 and no complete artifact is
  published.

  Add `--require-equivalent` to return 1 after writing the artifact when a
  primary-only or secondary-only counterexample exists. Without that flag,
  disagreement is a successful research observation. Verify a stored artifact
  independently with:

    python3 util/parser_equivalence_audit.py \
      --verify parser_equivalence_artifact.json

  `symcc-parser-bounded-equivalence-v1` binds the exhaustive-domain proof,
  command digests, four acceptance quadrants, full transcript digest, elapsed
  time, and a bounded shortlex counterexample prefix. Its `equivalent` field
  means only equivalence over the declared finite byte domain.

  A parser that can expose epsilon reductions or a bounded packed parse forest
  may instead emit `symcc-parser-structural-trace-v2`. Every node then has
  `epsilon: true|false`; epsilon is true exactly for a zero-width span, and an
  epsilon node cannot have children. A node may additionally name up to eight
  alternatives as direct-child index lists:
    {"schema":"symcc-parser-structural-trace-v2",
     "parser":"glr-json-1","accepted":true,
     "nodes":[
       {"symbol":"choice","state":"value","start":0,"end":1,"parent":-1,
        "alternatives":[[1],[2]]},
       {"symbol":"empty","state":"epsilon","start":0,"end":0,"parent":0,
        "epsilon":true},
       {"symbol":"token","state":"atom","start":0,"end":1,"parent":0}]}

  Alternatives must be unique, ordered, internally non-overlapping child lists
  whose union is exactly the node's direct children. Alternative zero is the
  concrete parser-selected tree used for replacement-context localization;
  other alternatives contribute evidence but cannot hijack the selected
  ancestry. The manager canonicalizes each retained family as
  `symcc-parser-production-v2`, with epsilon included in both production and
  shape identities, and emits `symcc-parser-cfg-fragment-v3`. Primary ancestry
  productions are retained first; distinct packed alternatives fill the
  remaining deterministic 32-production budget. Instances remain capped at 32
  and the complete fragment at 64 KiB.

  A zero-width selected instance is executable evidence only when its
  production is an empty-RHS epsilon production with one empty terminal gap.
  After target replay and independent parser acceptance, semantic state schema
  v16 may learn a context/shape-restricted `epsilon` rule that deletes the
  matched source token. It is subject to the same target, parser, ECT-shape,
  Pareto scheduling, and AFL-retention gates as a nonempty subtree
  substitution. V1 traces, v2 CFG fragments, proposal states v1--v10, and
  semantic states v1--v18 remain load-compatible.

  A parser with an actual shared packed parse forest may emit
  `symcc-parser-structural-trace-v3`. V3 nodes omit `parent`; `roots` names one
  to eight node indexes, and every alternative contains forward child indexes
  only. Forward edges make the graph acyclic. Child spans must remain inside
  the parent and be ordered/non-overlapping within one alternative. All nodes
  must be reachable from a root. Root zero plus recursively chosen alternative
  zero must form the concrete selected tree: a selected node cannot have two
  primary parents. Shared nodes remain legal across non-primary alternatives.

  The complete input trace remains capped at 4096 nodes, 16384 edge
  occurrences, and 1 MiB. Extraction first reserves the selected ancestry,
  then expands a deterministic breadth-first packed closure of at most 32
  nodes and 128 edges. `symcc-parser-cfg-fragment-v4` binds
  `symcc-parser-packed-node-v1` IDs to parser/order/symbol/state/span/epsilon/
  yield hash and `packed-edge-v1` IDs to parent/child/alternative/slot.
  Every deep instance uses `symcc-parser-subtree-instance-v2`, whose identity
  includes the shared node and complete root-to-node edge path. A `truncated`
  marker distinguishes a bounded projection from a complete forest.

  Semantic state v16 introduced, and current v19 retains, an ordered local
  `child_edge_ids` binding for every packed instance's concrete production
  alternative. On restore, these
  edges must form an exact slot 0..RHS-arity-1 bijection and match the parent,
  alternative, and child symbol/state. A missing, reordered, partial, or
  cross-parent binding rejects that instance and its derived rules. V15
  migration infers the list only when the accumulated legacy edge set is
  unique and complete. This prevents a content-addressed node reused by
  multiple forests from accidentally mixing their child-edge sequences.

  Semantic ingestion independently recomputes the node, edge, production,
  shape, instance, gap, and yield identities; checks DAG order, containment,
  roots, selected path, alternative slots, and path connectivity; and rejects
  the whole fragment on mismatch. Non-primary deep instances may join an ECT
  shape class, but cannot generate until an independently accepted selected
  tree maps the source lexical context to that same shape. Semantic state
  retains at most 8192 packed nodes and 32768 edges. Node/edge eviction
  cascades through every dependent instance and rule-shape link.

  A parser that also exposes grammar-level nullability may emit
  `symcc-parser-structural-trace-v4`. It retains the v3 forward packed DAG and
  adds one to 32 rules of the form:
    {"lhs":["A","state"],"rhs":[["B","state"],["C","state"]]}
  Each RHS has at most eight `(nonterminal,state)` dependencies; an empty RHS
  is a base nullable rule. Rules are canonicalized as
  `symcc-parser-nullable-rule-v1`. The manager computes dependency SCCs and the
  least fixed point: base proofs have depth zero, and a rule proves its LHS at
  depth `1 + max(child depths)` only after every RHS symbol is proved. Ties use
  `(depth, rule ID)`, so the certificate is deterministic. A pure recursive
  SCC such as `A -> B, B -> A` has no nullable proof; adding `B -> epsilon`
  proves `B` at depth zero and `A` at depth one.

  The resulting `symcc-parser-cfg-fragment-v5` includes the canonical rules,
  cyclic SCC identities, and exact least-fixed-point proofs. Semantic
  ingestion recomputes the entire certificate before changing state, then
  unions accepted rules by parser under a 4096-rule hard bound and recomputes
  the global fixed point. Derived proofs and SCCs in a state file are never
  trusted on restore. A production shape becomes deletion-capable only when
  its own parser/LHS/state is globally proved nullable and the source lexical
  context was independently mapped to that selected shape. Thus grammar-level
  cycles do not relax the forward-DAG requirement and cannot create an
  unscoped empty mutation. Nullable source rules first appeared in proposal
  state v8 and semantic state v13. Current proposal state v11 and semantic
  state v25 retain them and recompute all derived authorization after restart
  or reference eviction.

  Shared-DAG fragments with a primary production of two to eight child slots
  can additionally induce synchronized multi-nonterminal transactions. No new
  parser assertion is trusted for this step. The semantic layer requires a
  complete alternative-zero edge sequence, one independently verified primary
  child instance per slot, and exact reconstruction of the accepted parent
  yield from its terminal gaps and child yields. It indexes each child shape's
  distinct accepted yields and searches a bounded combination space: two to
  four slots must change together, at most two canonical alternatives are
  considered per slot, at most four transactions are retained per parent
  instance, and the global hard limit is 4096.

  `symcc-parser-sync-transaction-v2` binds the parser, parent shape,
  production, and instance; every ordered slot edge; source and target
  instances; unchanged terminal gaps; the changed-slot bitmap; and the
  reconstructed yield hash. It additionally binds each inferred slot-relation
  ID and whether the proposed assignment satisfies it. Results already
  observed as accepted instances of
  the parent shape are skipped. A `synchronized` grammar rule is eligible only
  when the current source bytes exactly equal its transaction's source parent
  yield and the lexical context is certified with the same parent shape. It
  then performs one splice of the complete reconstructed parent subtree; no
  parser-invalid single-slot intermediate is emitted. The proposal carries
  `grammar_sync_transaction_id` for audit and still requires target replay,
  independent parser acceptance, and AFL novelty.

  Sync transactions and rule links are derived data. Semantic state v22 writes
  them for inspection but ignores them as authority on load, rebuilding them
  from revalidated productions, nodes, edges, and instances. Instance, edge,
  production, or grammar-rule eviction recomputes or withdraws every dependent
  transaction. Proposal state v10 persists the transaction provenance digest.

  Relation-aware scheduling is derived from those reconstructed accepted
  parents. A parent production shape needs at least two concrete observations,
  and every current observation must satisfy a relation before it is retained.
  For each ordered slot pair, the strongest matching predicate is selected in
  this order:

    1. exact byte equality;
    2. ASCII uint64 decimal equality;
    3. left decimal value equals right byte length;
    4. right decimal value equals left byte length;
    5. byte-length equality.

  Decimal operands contain 1--20 ASCII digits and must fit uint64. Relation
  IDs bind parser, parent shape, slot pair, and predicate. A newly accepted
  counterexample therefore weakens or removes a relation on the next rebuild;
  persisted relation/support fields are audit data and are not trusted.

  The per-parent product examines at most 256 combinations and globally stores
  at most 4096 relations and 4096 transactions. Up to four transactions are
  retained per parent: three highest-ranked relation-compatible candidates
  plus, when available, one relation-breaking exploration reserve. Relations
  are scheduling evidence only. They never reject a candidate, authorize a
  shape, or replace target replay, independent parser acceptance, or AFL
  novelty. Snapshot fields are `slot_relations`, `slot_relation_support`,
  `slot_relation_kinds`, `sync_relation_conforming`, and
  `sync_relation_exploration`.

  If COMMAND contains both `{trace}` and `{cache}`, the latter is replaced by
  a fresh read-only incremental-cache manifest path. The first parse is
  `mode: cold`. After a complete trace passes all ordinary checks, the manager
  stores its exact bytes and input in a content-addressed cache of at most 256
  entries. For a later proposal whose `source_path` content has a valid cached
  trace from the identical parser command, the manifest becomes
  `mode: incremental`.

  `symcc-parser-incremental-cache-v1` contains the base input/trace paths and
  SHA-256 values, a longest-common-prefix/suffix edit script, and a conservative
  invalidation frontier. Edits whose deleted plus inserted region exceeds
  `SYMCC_PROPOSAL_PATCH_BYTES` use cold mode. Nodes touching the edit or its
  16-byte guard are invalidated; at most 512 nodes fully inside the unchanged
  prefix/suffix are offered with mapped spans and yield hashes. The parser may
  use the base trace and offered nodes internally, but must still emit a full
  v1--v4 structural trace for the candidate.

  A cache-aware parser may add:
    {"incremental_cache":{
      "schema":"symcc-parser-incremental-reuse-v1",
      "manifest_sha256":"...",
      "reused_nodes":[{"base_index":1,"candidate_index":1}]}}
  The manager checks the manifest digest, unique mapping, offered base index,
  candidate symbol/state/span/epsilon, and candidate yield hash. A missing
  receipt means the parser performed a full fallback and remains valid. A
  malformed or false receipt rejects the trace. A corrupt/missing cache entry
  is deleted and automatically falls back to cold parsing. Cache reuse never
  substitutes for process exit status, target replay, full trace validation,
  parser acceptance, or AFL novelty.

  Proposal state v10 persists bounded cache metadata and per-record manifest,
  base, invalidated/reused-node, and hit counters. Trace and input contents
  remain separate content-addressed files and are rehashed lazily before every
  reuse. These counters establish functional use, not a parser speedup claim;
  wall-time improvement requires an external parser that actually consumes the
  manifest and an equal-CPU benchmark.

  Independently accepted v4/v5 CFG fragments also update an accepted-forest
  PCFG scheduler. Only the complete concrete derivation rooted at `roots[0]`
  and following alternative zero is counted. The canonical fragment SHA-256
  deduplicates observations; after 8192 retained digests, learning saturates
  instead of evicting a digest and risking double counting. Production
  families are keyed by `(parser,LHS,state)` and use symmetric
  Dirichlet/Jeffreys smoothing with alpha 0.5:
    P(shape | family) =
      (selected_count + 0.5) /
      (family_selected_count + 0.5 * known_shapes)

  Alternative ordinals are local to one parser forest and are stored on the
  concrete subtree instance. Global probability hyperedges are instead
  canonicalized by node, production, and ordered child-node IDs. Semantic
  state v15 introduced validated family counts, at most 8192 fragment
  observations, and explicit packed-root membership. Each
  `symcc-parser-packed-root-evidence-v1` identity binds the accepted fragment
  digest, parser, and root node; v15 restores roots only from revalidated
  evidence, while v14 migration labels its inferred graph frontier separately.
  Semantic state v16 retained the same evidence and added exact packed
  instance child-edge provenance. Current v19 also stores bounded conditional
  evidence described below.
  Inside masses are
  recomputed in reverse topological order and outside masses in forward order
  after every load or graph/reference eviction; derived probability tables
  are never trusted from disk.

  Posterior likelihood and an information/reachability score derived from
  count uncertainty plus outside mass are scheduling objectives only. They
  cannot reject a low-probability production, authorize an ECT mutation, or
  replace target replay, independent parser acceptance, and AFL novelty.
  Snapshot fields include `pcfg_families`, `pcfg_observations`,
  `pcfg_selected_productions`, `pcfg_inside_nodes`, `pcfg_outside_nodes`,
  `pcfg_packed_alternatives`, normalized entropy, maximum posterior, and
  observation-capacity saturation.

  Semantic state v17 introduced a hierarchical production context:
    `symcc-parser-production-context-v1` =
      (parser, child family, parent production shape, RHS slot)
  Roots use an empty parent shape and slot -1. A complete accepted concrete
  tree atomically contributes both unconditional and context selections.
  Every selected node must have a primary instance whose exact local
  `child_edge_ids` cover all RHS slots. Missing instances, duplicate primary
  ancestry, partial slots, or edge mismatch leave only an empty fragment
  deduplication record and update no counts.

  For a non-root context c, the posterior is shrunk toward the unconditional
  family posterior P0 with beta 2.0:
    P(shape | c) =
      (context_count(shape) + 2.0 * P0(shape)) /
      (context_selected_count + 2.0)
  Root contexts use P0 directly. With no context evidence, this formula
  exactly falls back to P0 and preserves nonzero mass for known unobserved
  shapes.

  Because a shared packed node can occur below different parent shapes,
  contextual inference uses `(node, context)` states rather than overwriting
  the unconditional node mass. At most 32768 states run reverse-topological
  inside and forward-topological outside propagation. Contextual alternative
  posterior/reachability joins the existing PCFG Pareto objectives but remains
  scheduling evidence only. At most 8192 observed contexts and 8192 fragment
  witnesses are retained.

  V17 and current v19 restore recompute every context identity, verify that the
  parent shape/slot can produce the named child family, and require context fragment
  digests to belong to the accepted PCFG observation set. Counts and complete
  fragment selection lists are reconciled to an atomic fixed point, so a
  tampered selection withdraws all evidence from that fragment and any
  dependent mismatched counts in one load. V16 and older states have no
  conditional evidence and use the unconditional fallback. Derived context
  inside/outside tables are never persisted. Snapshot fields are
  `pcfg_contexts`, `pcfg_context_observations`,
  `pcfg_context_selected_productions`, `pcfg_context_inside_states`,
  `pcfg_context_outside_states`, `pcfg_context_alternatives`, and
  `pcfg_context_mean_nll_bits`. The NLL field is an online training-evidence
  diagnostic, not held-out perplexity.

  Semantic state v18 adds update-before prequential calibration. Before any
  count from an accepted fragment is applied, each selected node records a
  `symcc-parser-pcfg-prequential-v1` receipt with the fragment/node/context/
  shape identity and these sufficient statistics:

    global selected count before the fragment;
    global family total before the fragment;
    number of known family shapes at prediction time;
    context selected count before the fragment;
    context total before the fragment.

  All selections in one fragment use batch-before-update semantics. The
  receipt stores no probability: restore recomputes global and context
  predictions with alpha 0.5 and beta 2.0. At most 32768 receipts are retained;
  the evidence saturates without eviction, while ordinary PCFG/context
  learning continues under its independent 8192-fragment bound.

  Per context, deterministic receipt-ID order produces prequential global and
  context NLL bits, prediction wins, and
    gain_bits = global_nll_bits - context_nll_bits.
  A context receives nonzero scheduling weight only after two observations and
  positive cumulative gain:
    weight =
      min(1, observations / 8) *
      min(1, max(0, gain_bits) / 2)
    effective_posterior =
      global_posterior +
      weight * (raw_context_posterior - global_posterior)

  Negative gain, absent receipts, or later prediction drift therefore restores
  the global posterior exactly. Context-state alternative artifacts expose
  `raw_posterior`, `posterior` (the effective value), and
  `calibration_weight`. V17 migration retains raw context counts but uses zero
  weight because training-fit evidence is not a substitute for update-before
  prediction evidence.

  V18 restore checks canonical receipt identity, unique
  `(fragment,node,context,shape)` events, context-fragment membership, matching
  family/parent/slot, bounded integer sufficient statistics, and before-counts
  strictly earlier than final revalidated counts. Invalid receipts withdraw
  calibration only; they do not alter grammar counts or authorize mutations.
  Derived calibration tables are never persisted. Snapshot fields are
  `pcfg_prequential_receipts`, `pcfg_prequential_capacity`,
  `pcfg_prequential_saturated`, `pcfg_prequential_observations`,
  `pcfg_prequential_global_nll_bits`,
  `pcfg_prequential_context_nll_bits`,
  `pcfg_prequential_context_gain_bits`,
  `pcfg_prequential_context_wins`, `pcfg_calibrated_contexts`, and
  `pcfg_mean_context_weight`.

  Semantic state v19 adds ordered recency calibration. New
  `symcc-parser-pcfg-prequential-v2` receipts bind an
  `observation_index`: the number of accepted PCFG fragment records before the
  current fragment. All selected nodes from one fragment share an index, and
  distinct fragments cannot share one. Receipt v1 remains valid migration
  evidence but has no inferred time order.

  The current window covers the latest 16 accepted fragment indexes and
  advances from the full PCFG observation stream, not merely from receipts.
  Thus empty accepted-tree evidence, an absent context, or saturated receipt
  storage still ages old calibration. Each context exposes recent global/
  context NLL, gain, wins, and selection count. Once a context has any v2
  evidence, its scheduling weight uses only recent statistics:

    fewer than 2 recent selections -> weight 0;
    recent gain <= 0              -> weight 0;
    no event in the window        -> weight 0 and stale = 1;
    otherwise                     -> the F216 gain/sample formula.

  This lets recent adverse evidence override positive lifetime gain and lets
  later positive evidence recover from historical loss. V18 v1-only contexts
  retain the cumulative F216 gate. Mixed v1/v2 state is allowed after migration;
  the first v2 evidence switches that context to recency mode.

  V19 restore additionally checks observation-index range, one index per
  fragment, one fragment per index, and the v2 canonical digest. Removing an
  index from a v2 receipt changes its schema identity and cannot silently
  downgrade it to v1. Snapshot fields are
  `pcfg_calibration_recent_fragments`, `pcfg_recency_contexts`,
  `pcfg_stale_contexts`, `pcfg_recent_observations`,
  `pcfg_recent_global_nll_bits`, `pcfg_recent_context_nll_bits`,
  `pcfg_recent_context_gain_bits`, and `pcfg_recent_context_wins`.
  The fixed window is a reproducible policy baseline, not an adaptive-window
  change detector with statistical false-alarm guarantees.

  Semantic state v20 adds a bounded adaptive calibration window over v2
  receipts. Receipts for the same context and accepted-fragment index are one
  detection unit: their log-loss gains
    d = log2(context_probability / global_probability)
  are averaged after clipping each value to [-4, 4] bits. At most the latest
  64 context-bearing fragments are replayed, and every candidate cut retains
  at least eight fragments on each side.

  For a scan with m legal cuts, the detector assigns
    adjusted_delta = 0.05 / m
  and uses the bounded two-sample Hoeffding threshold
    epsilon =
      4 * sqrt(
        2 * ln(2 / adjusted_delta) *
        (1 / left_fragments + 1 / right_fragments))
  A cut is accepted only when the absolute difference between the clipped
  left/right means exceeds epsilon. The positive-margin cut with the largest
  margin is selected, its left prefix is discarded, and detection resumes as
  later fragments arrive.

  Scheduling uses the retained suffix but not the clipped detector values.
  Global and context NLL are averaged within each accepted fragment and then
  summed across retained fragments. The F216 gain/sample formula uses this
  unmodified adaptive gain and the retained fragment count. This prevents one
  large tree from masquerading as many independent calibration samples. The
  F217 fixed-16 metrics remain available, and no context evidence in that
  recent window still forces `stale = 1` and zero weight.

  Every accepted cut emits a
  `symcc-parser-pcfg-adaptive-cut-v1` certificate containing the context,
  window and cut indexes, both sample/receipt counts, clipped means,
  difference, epsilon, margin, clip bound, delta allocation, and a digest of
  the ordered receipt IDs. `verify_pcfg_adaptive_certificate` reconstructs
  these values and the certificate ID from canonical receipts. Certificates
  are serialized only as audit output; restore ignores them and recomputes all
  adaptive state. They never authorize a grammar proposal.

  Snapshot fields are `pcfg_adaptive_max_fragments`,
  `pcfg_adaptive_min_fragments`, `pcfg_adaptive_clip_bits`,
  `pcfg_adaptive_delta`, `pcfg_adaptive_certificates`,
  `pcfg_adaptive_contexts`, `pcfg_adaptive_fragments`,
  `pcfg_adaptive_receipts`, `pcfg_adaptive_truncated_fragments`,
  `pcfg_adaptive_global_nll_bits`, `pcfg_adaptive_context_nll_bits`,
  `pcfg_adaptive_context_gain_bits`, and `pcfg_adaptive_context_wins`.
  The 0.05 bound is a per-scan union bound over candidate cuts, not an
  anytime-valid false-alarm guarantee across an unbounded execution.

  Semantic state v21 adds a bounded grandparent probabilistic-circuit expert.
  Its canonical context is
    (parser, child family,
     parent production shape and RHS slot,
     grandparent production shape and RHS slot).
  Only complete accepted alternative-zero trees contribute evidence. At most
  8192 circuit contexts and 32768 circuit receipts are stored.

  The raw circuit posterior is hierarchical:
    parent_raw =
      (parent_selected + 2 * global) / (parent_total + 2)
    circuit_raw =
      (circuit_selected + 2 * parent_raw) / (circuit_total + 2)
  so an unseen circuit context is exactly the parent distribution. Before
  applying one fragment's counts,
  `symcc-parser-pcfg-circuit-prequential-v1` records all three selected/total
  sufficient-stat layers, the known-shape count, the two-level context path,
  and the accepted-fragment index.

  Circuit calibration compares the finer expert with both coarser models:
    robust_gain =
      min(global_nll - circuit_nll,
          parent_nll - circuit_nll)
  The circuit receives positive weight only when this robust gain is positive
  with sufficient retained evidence. Receipts from one fragment are one
  adaptive sample; the same 64-fragment, minimum-8+8 bounded detector is
  applied to clipped robust gain. Cuts use
  `symcc-parser-pcfg-circuit-cut-v1` and can be checked with
  `verify_pcfg_circuit_certificate`.

  A packed context-state v2 carries the immediate parent context and optional
  circuit context. The alternative mass is still
    posterior * product(child inside mass)
  and alternatives still sum within a state. When the circuit gate is active:
    final_posterior =
      (1 - circuit_weight) * parent_effective_posterior +
      circuit_weight * circuit_raw_posterior
  This convex mixture remains normalized. Zero, negative, stale, absent, or
  legacy evidence recovers `parent_effective_posterior` exactly.

  V21 restore validates both production/RHS levels, reconciles circuit counts
  against complete fragment witnesses, checks circuit receipts against final
  global/parent/circuit counts and the shared fragment-index bijection, and
  recomputes every weight, certificate, and packed mass. Persisted
  `pcfg_circuit_certificates` are audit output only. V20 and older states do
  not synthesize circuit evidence.

  Snapshot fields are `pcfg_circuit_contexts`,
  `pcfg_circuit_observations`, `pcfg_circuit_selected_productions`,
  `pcfg_circuit_mean_nll_bits`, `pcfg_circuit_receipts`,
  `pcfg_circuit_receipt_capacity`, `pcfg_circuit_receipts_saturated`,
  `pcfg_circuit_calibrated_contexts`, `pcfg_circuit_mean_weight`,
  `pcfg_circuit_stale_contexts`,
  `pcfg_circuit_adaptive_certificates`,
  `pcfg_circuit_adaptive_fragments`,
  `pcfg_circuit_adaptive_truncated_fragments`,
  `pcfg_circuit_adaptive_global_nll_bits`,
  `pcfg_circuit_adaptive_parent_nll_bits`,
  `pcfg_circuit_adaptive_nll_bits`, and
  `pcfg_circuit_adaptive_robust_gain_bits`.

  Semantic state v22 adds a bounded ordered-sibling autoregressive factor.
  For every non-first child in a complete accepted alternative-zero parent,
  its canonical context is
    (parser, child family, parent production shape, current RHS slot,
     immediately preceding child's selected production shape).
  At most 8192 sibling contexts and 32768 sibling receipts are retained.

  The sibling raw posterior uses the finest available ancestor raw posterior
  as its beta-2 prior:
    sibling_raw =
      (sibling_selected + 2 * ancestor_raw) / (sibling_total + 2)
  where `ancestor_raw` is circuit raw when a grandparent context exists and
  parent raw otherwise. Before any count from the accepted fragment is
  applied, `symcc-parser-pcfg-sibling-prequential-v1` records global, parent,
  optional circuit, and sibling sufficient statistics plus the shared
  fragment index.

  Calibration requires the sibling expert to beat every coarser baseline:
    robust_gain =
      min(global_nll - sibling_nll,
          parent_nll - sibling_nll,
          circuit_nll - sibling_nll)
  Without a circuit context, `circuit_nll` equals `parent_nll`. The retained
  fragment count and robust gain determine `sibling_weight`; stale, absent,
  non-positive, or insufficient evidence yields zero. The same bounded
  per-fragment adaptive detector emits
  `symcc-parser-pcfg-sibling-cut-v1`, independently verifiable with
  `verify_pcfg_sibling_certificate`.

  Packed context-state v3 includes the optional sibling context. Within one
  parent alternative, child inside masses are combined by a left-to-right
  shape-indexed forward message, not an independence product. Artifact-level
  outside coefficients use the matching forward prefix and backward suffix,
  so right-sibling dependencies remain distinct on a shared packed DAG.
  `child_factor_steps` records each previous/selected shape and referenced
  child state/artifact for audit. The final child posterior is
    final_posterior =
      (1 - sibling_weight) * ancestor_effective_posterior +
      sibling_weight * sibling_raw_posterior
  and remains normalized.

  V22 restore validates the parent current/left RHS path, reconciles sibling
  counts with complete fragment witnesses, checks receipts against final
  global/parent/optional-circuit/sibling counts and all shared fragment-index
  bijections, then recomputes weights, certificates and messages. Persisted
  sibling certificates are audit output only. V21 and older states do not
  synthesize sibling evidence.

  Snapshot fields are `pcfg_sibling_contexts`,
  `pcfg_sibling_observations`, `pcfg_sibling_selected_productions`,
  `pcfg_sibling_mean_prequential_nll_bits`, `pcfg_sibling_receipts`,
  `pcfg_sibling_receipt_capacity`, `pcfg_sibling_receipts_saturated`,
  `pcfg_sibling_calibrated_contexts`, `pcfg_sibling_mean_weight`,
  `pcfg_sibling_stale_contexts`,
  `pcfg_sibling_adaptive_certificates`,
  `pcfg_sibling_adaptive_fragments`,
  `pcfg_sibling_adaptive_truncated_fragments`,
  `pcfg_sibling_adaptive_global_nll_bits`,
  `pcfg_sibling_adaptive_parent_nll_bits`,
  `pcfg_sibling_adaptive_circuit_nll_bits`,
  `pcfg_sibling_adaptive_nll_bits`,
  `pcfg_sibling_adaptive_robust_gain_bits`,
  `pcfg_sibling_factor_steps`, and
  `pcfg_sibling_factor_transitions`.

  Semantic state v23 adds a separate anytime-valid audit tier for the parent,
  grandparent-circuit, and ordered-sibling prequential gain streams. It does
  not replace the responsive v20 per-scan cut used by the scheduling gate.
  Each fragment-level gain is clipped to [-4, 4] bits and normalized to
  x = (gain + 4) / 8 in [0, 1].

  A forward confidence sequence is launched at each context-local fragment
  ordinal j. Its launch budget and the budget for its kth look are
    alpha_j = 0.05 * 6 / (pi^2 * j^2)
    alpha_jk = alpha_j * 6 / (pi^2 * k^2)
  The kth two-sided Hoeffding interval has radius
    sqrt(ln(2 / alpha_jk) / (2 * k))
  and the confidence sequence is the running intersection of these intervals.
  At most the latest 64 launches are active. A certificate is emitted only
  when two sequences launched at least eight fragments apart, each with at
  least eight observations, have disjoint running intervals.

  Under the explicit context-wise null that normalized gains are bounded and
  have one constant conditional mean,
    E[x_t | F_(t-1)] = mu,
  the double inverse-square allocation satisfies
    sum_j sum_k alpha_jk <= 0.05.
  Hence the probability of any certified false alarm over arbitrarily many
  scans is at most 0.05 for that context. This is not a simultaneous guarantee
  over every learned context, and nonstationary/adversarial conditional means
  are outside the null. The finite 64-launch implementation only removes
  rejection opportunities, so it does not weaken that bound.

  The certificate schemas are
  `symcc-parser-pcfg-anytime-cut-v1`,
  `symcc-parser-pcfg-circuit-anytime-cut-v1`, and
  `symcc-parser-pcfg-sibling-anytime-cut-v1`. They bind the guarantee and null
  names, both spending rules, launch ordinals and observation indexes, sample
  means, running intervals, tightening ages, final radii, separation gap,
  clipping range, and the ordered receipt digest. Verification reconstructs
  the complete artifact from canonical update-before receipts. Serialized
  certificates remain derived audit output; v23 restore ignores them and
  recomputes them. V22 input is accepted and gains the new audit tier only
  from receipts that pass the existing fixed-point validation.

  Snapshot fields are `pcfg_anytime_construction`,
  `pcfg_anytime_guarantee`, `pcfg_anytime_spending_scale`,
  `pcfg_anytime_certificates`, `pcfg_anytime_certified_contexts`,
  `pcfg_circuit_anytime_certificates`,
  `pcfg_circuit_anytime_certified_contexts`,
  `pcfg_sibling_anytime_certificates`, and
  `pcfg_sibling_anytime_certified_contexts`.

  Semantic state v24 adds a bounded second-order sibling-history factor for
  children at RHS slot two or later. Its canonical context is
    (parser, child family, parent production shape, current RHS slot,
     selected shape at slot - 2, selected shape at slot - 1).
  This models a non-adjacent dependency after controlling the immediately
  preceding sibling. The history table is capped at 8192 contexts and 32768
  update-before receipts.

  The raw history posterior is a beta-2 shrinkage estimator whose prior is the
  immediate-sibling raw posterior:
    history_raw =
      (history_selected + 2 * sibling_raw) / (history_total + 2)
  and the effective distribution is the normalized convex mixture
    final_posterior =
      (1 - history_weight) * sibling_effective_posterior +
      history_weight * history_raw_posterior.
  Missing, stale, adverse, insufficient, saturated, or legacy history evidence
  therefore recovers the v22 sibling model exactly.

  `symcc-parser-pcfg-history-prequential-v1` records all five update-before
  sufficient-stat layers. Calibration uses
    robust_gain =
      min(global_nll - history_nll,
          parent_nll - history_nll,
          circuit_nll - history_nll,
          sibling_nll - history_nll),
  so the second-order factor must improve on every available coarser expert.
  Responsive cuts use `symcc-parser-pcfg-history-cut-v1`; the independent
  F223 audit uses `symcc-parser-pcfg-history-anytime-cut-v1`. Both public
  verifiers reconstruct probabilities, fragment aggregation, evidence
  digests, thresholds or confidence sequences, and IDs from canonical
  receipts.

  Packed context-state v4 retains the last two selected child shapes.
  Forward messages transition over bounded tuple histories and suffix messages
  propagate exact artifact-level outside coefficients for this order-two
  chain. `previous_sibling_shape_ids` and `next_sibling_shape_ids` expose the
  tuple transition while the legacy singular previous-shape field remains
  available. This is exact for the bounded second-order factor represented in
  the packed forest; it is not an arbitrary-order, bidirectional, cross-parent,
  symbol-table, checksum, or query-conditioned probabilistic circuit.

  V24 restore recomputes context IDs, validates both preceding RHS production
  shapes, reconciles count/fragment witnesses to a fixed point, checks all five
  count layers and shared fragment-index bijections, and rebuilds calibration,
  certificates, and factor messages. Stored derived artifacts are never
  trusted. V23 and older states cannot synthesize history evidence.

  Snapshot fields are `pcfg_history_contexts`,
  `pcfg_history_observations`, `pcfg_history_selected_productions`,
  `pcfg_history_receipts`, `pcfg_history_receipt_capacity`,
  `pcfg_history_receipts_saturated`,
  `pcfg_history_calibrated_contexts`, `pcfg_history_mean_weight`,
  `pcfg_history_stale_contexts`,
  `pcfg_history_adaptive_certificates`,
  `pcfg_history_anytime_certificates`,
  `pcfg_history_anytime_certified_contexts`, and
  `pcfg_history_factor_states`.

  Semantic state v25 adds an append-only online allocation ledger and a
  separate cross-context FWER audit. It does not change the v20 responsive
  scheduling cuts or the v23 context-wise certificates. When a parent,
  grandparent circuit, immediate-sibling, or second-order history context is
  first registered, it receives the next global ordinal c and
    context_delta_c =
      0.05 * 6 / (pi^2 * c^2).
  Ordinals and spent alpha are never recycled after a context becomes inactive.
  The ledger is capped at 32768 entries; saturation disables global
  certification for later contexts instead of reusing old budget.
  The registration observation itself is excluded from the global test stream,
  so the outer allocation is fixed before any observation used by that test.

  Inside context c, the v23 repeated-forward construction spends
    launch_alpha_cj =
      context_delta_c * 6 / (pi^2 * j^2)
    look_alpha_cjk =
      launch_alpha_cj * 6 / (pi^2 * k^2).
  Therefore the sum over every registered context, launch, and look is at most
  0.05. Under the stated null for each true-null context that normalized gains
  are bounded and have a constant conditional mean, the union bound controls
  the probability of one or more false certified changes across all four
  context kinds and arbitrary stopping times. No independence between context
  streams is assumed.

  Global certificates use
  `symcc-parser-pcfg-global-anytime-cut-v1`. In addition to the v23 confidence
  sequence evidence they bind the context kind, allocation ID and ordinal,
  context/global alpha, outer spending rule, append-only contract, and the
  digest of the allocation-ledger prefix through that ordinal.
  `registration_observation_excluded=true` records the predictability guard.
  `verify_pcfg_global_anytime_certificate` reconstructs the allocation prefix,
  model-specific robust-gain units, all three spending levels, confidence
  intervals, and certificate ID.

  V25 restore validates a contiguous ordinal sequence, canonical allocation
  IDs, first-observation indexes, exact alpha values, uniqueness, and the
  presence and first index of every context with retained receipts. A missing,
  reordered, altered, or incomplete v25 ledger disables the entire global
  audit tier; it does not discard grammar evidence or weaken ordinary
  scheduling fallback. V24 and older states deterministically construct an
  initial ledger from fully validated ordered receipts. Persisted global
  certificates are derived output and are ignored on restore.

  Snapshot fields are `pcfg_anytime_global_guarantee`,
  `pcfg_anytime_global_delta`, `pcfg_anytime_context_allocations`,
  `pcfg_anytime_context_allocation_capacity`,
  `pcfg_anytime_context_allocations_saturated`,
  `pcfg_anytime_allocation_ledger_valid`,
  `pcfg_anytime_allocated_delta`,
  `pcfg_global_anytime_certificates`, and
  `pcfg_global_anytime_certified_contexts`.

- SYMCC_PCFG_CONTEXT_ORDER=global|parent|circuit|sibling|history|0..4
  (default history/4): Select the finest enabled probabilistic grammar
  context for a controlled ablation. The levels are nested:
    0 global production family,
    1 parent production/slot,
    2 grandparent circuit,
    3 immediate ordered sibling,
    4 second-order sibling history.
  Disabled levels do not collect their contexts, update-before receipts,
  calibration state, responsive/anytime certificates, or packed factor
  states. Sibling frontiers retain one selected shape at level 3 and two at
  level 4. Level 0 skips contextual inside/outside completely. This is
  therefore a mechanism-and-cost ablation, not a scalar-score switch. An
  invalid value is reported by the MPI master and falls back to history.
  The selected order and level are included in semantic mappings and grammar
  snapshots; the semantic evidence schema remains v25. Restoring a state
  written at another order fail-closes by clearing all PCFG counts, receipts,
  certificates, allocations and derived masses before rebuilding neutral
  forest structure; `pcfg_state_order_mismatch_reset=1` records this event.
  Validated CFG/ECT grammar structure is retained.

- SYMCC_PCFG_RESEARCH_ARTIFACT=PATH (default
  `$SYMCC_RESEARCH_RUN_DIR/pcfg_research_artifact.json` when a sealed research
  run is active): Atomically write `symcc-pcfg-research-artifact-v1`. The
  artifact binds semantic schema, selected context order, protocol
  experiment/run/pair/configuration, seed and CPU budget to the complete
  scalar grammar snapshot and a canonical SHA-256. Metrics include
  prequential/adaptive NLL, robust gain, calibrated/fallback state,
  certificate count/detection delay, allocated alpha, ledger saturation,
  context/receipt/state/transition counts, and grammar yield.
  `benchmark/research_protocol.py` verifies the semantic digest and protocol
  binding in addition to hashing the complete run artifact tree.

- SYMCC_PCFG_REQUIRE_ARTIFACT=0|1 (normally set automatically by
  `pcfg_context_ablation`): A successful sealed PCFG ablation without a valid
  final artifact is recorded as failed. Timeout and other failed runs remain
  retained as failures rather than being discarded.

- SYMCC_PROPOSAL_PARSER_TIMEOUT=SECONDS (default 1.0, range 0.01--60):
  Wall-clock limit for one parser oracle invocation. Grammar proposals carry a
  stable context ID derived from branch, input-size bucket, and bounded
  left/right token neighborhoods. When a structural trace is available,
  semantic state schema v25 persists `(rule, lexical context) -> structural
  context/production` aliases and lexical-context-to-production-shape
  correspondence.
  Two parser rejections suppress that rule only in the selected structural
  context; parser acceptance clears the local suppression. Rule-level parser
  counts, aliases, and at most 256 rejected contexts per rule persist. When a
  verified proposal survives AFL novelty triage, its feature delta is also
  accumulated for that rule/structural-context pair. Candidate ordering adds a
  bounded inverse-square-root bonus to unseen or low-coverage pairs; retention
  feedback without an unused verified observation is rejected.

  Parser validation also updates a separate logical 64K grammar-coverage
  count bitmap keyed by `(rule, structural path, production)`. It is stored
  sparsely with saturating 8-bit counters, stable owner digests, event counts,
  and collision telemetry. This bitmap does not consume AFL edge/data coverage
  and therefore measures parser-production exercise independently. Its
  diminishing novelty bonus is combined with, but does not replace, target
  validity, parser acceptance, or AFL-retained feature yield.

  Parser-accepted v2 fragments also populate a bounded incremental ECT
  correspondence graph. Shape IDs retain parser, LHS/state, and ordered RHS
  labels while deliberately excluding concrete terminal bytes; instance IDs
  bind a shape to a production, concrete subtree yield, terminal gaps, and
  full selected ancestry. The semantic layer recomputes every hash before
  learning. Concrete yields from the same shape become `subtree` grammar
  alternatives, but are proposed only for lexical contexts previously
  certified with that shape. Candidate-local contexts are recorded after
  replacement so retained outputs can continue the correspondence chain.
  The graph is capped at 4096 shapes and 8192 instances, uses reference-safe
  cascading eviction, and is restored only after all production/yield/path
  invariants pass. This is bounded observed-subtree substitution, not complete
  parser grammar inference or a claim that two different parser
  implementations use equivalent nonterminals.

- SYMCC_PROPOSAL_MAX_BYTES=N (default 16777216) and
  SYMCC_PROPOSAL_PATCH_BYTES=N (default 65536): Bound the materialized candidate
  and total data introduced by transformations.

- SYMCC_SEMANTIC_FALLBACK=0/1 (default 1 when the adaptive scheduler is
  enabled): Enable a local semantic-constraint fallback planner in the MPI
  master. The planner summarizes telemetry into branch classes such as
  byte-local, token-progress, wide/nonlinear, timeout-prone, and opaque. It then
  emits the same validated hints as the agentic hook: S2F actionseed rows,
  strategy selection, target_branch for targeted work, and compact focus ranges.
  This gives the executor portfolio a deterministic fallback policy before
  spending expensive exact Z3 effort on solver-hostile branches.

- SYMCC_SEMANTIC_ACTIONS=N (default 8), SYMCC_SEMANTIC_EXACT_BYTES=N (default
  16), and SYMCC_SEMANTIC_FOCUS_SPAN=N (default 128): Bound the number of
  semantic actionseed rows per dispatch, the taint span considered byte-local
  enough for exact solving, and the maximum focus range emitted by the semantic
  planner. State is persisted in
  "$AFL_OUT/<symcc-name>/.semantic_fallback.json".

- SYMCC_SMT_ALGORITHM_SCHEDULER=0/1 (default 1 when adaptive scheduling is
  enabled): Enable SMTgazer-style clustered Bayesian scheduling over bounded
  solver-algorithm sequences. The default space includes exact Z3,
  fast-then-exact, optimistic-layered, and polyhedral-then-exact sequences. Each
  dispatch records SYMCC_ALGORITHM_SEQUENCE, SYMCC_ALGORITHM_TOKEN, and
  SYMCC_ALGORITHM_PROPENSITY so benchmark trajectories can be evaluated
  off-policy.

- SYMCC_SMT_ALGORITHM_SPACE=<json-or-path>: Override the default algorithm
  sequence space. The JSON format is {"sequences":[{"name":"...",
  "stages":[{"name":"...","overrides":{"ENV":"VALUE"}}]}]}. Overrides are
  sanitized with the same allowlist as the self-configuring parameter portfolio.

- SYMCC_SMT_ALGORITHM_PRIOR=<path>: Load an offline
  `symcc-smt-sequence-policy-v1` artifact produced by
  `util/smt_sequence_training.py`, or a
  `symcc-smt-sequence-ensemble-policy-v1` artifact produced by
  `util/smt_sequence_optimizer.py`. The loader verifies the canonical SHA-256,
  feature/objective/training schemas, all bounded X-means split BIC values,
  final cluster geometry, IPS effective sample sizes, censored PAR-2 moments,
  empirical-Bayes shrinkage, confidence lower bounds, support decisions, and
  recommendations. An invalid artifact or an action absent from the current
  algorithm space is ignored. A valid recommendation is not forced: it uses the
  existing 90% preference / 10% exploration path, and an explicit recommendation
  from the online conservative policy takes precedence. Multi-stage sequences
  already active for a seed are not interrupted. Assignments export
  `SYMCC_ALGORITHM_PRIOR_SHA256`, `SYMCC_ALGORITHM_PRIOR_CLUSTER`, and
  `SYMCC_ALGORITHM_PRIOR_SEQUENCE`; scheduler state records recommendation and
  match counts. An F240 ensemble artifact can recommend multiple actions with
  integer-second stage budgets. Matching assignments additionally export
  `SYMCC_ALGORITHM_PRIOR_SCHEDULE_INDEX`,
  `SYMCC_ALGORITHM_PRIOR_SCHEDULE_LENGTH`, and
  `SYMCC_ALGORITHM_BUDGET_SEC`. The worker clamps the budget to
  `[1, SYMCC_TIMEOUT]` before resolving the executor's real process timeout.

- SYMCC_OFFLINE_POLICY=0/1 (default 1 when the SMT algorithm scheduler is
  enabled) and SYMCC_OFFLINE_TRAJECTORY=<path>: Record interference-aware
  trajectory events for each completed solver-sequence assignment. Rewards
  include coverage gain, timeout/cost, duplicate generated cases, and current
  worker concurrency. The online coordinator only promotes a sequence prior when
  conservative SNIPS/doubly-robust estimates have enough effective samples and a
  lower-bound improvement over the behavior policy. Offline reports can be
  reproduced with:

      python3 util/offline_policy.py "$AFL_OUT/<symcc-name>/.offline_trajectory.jsonl"

  F239 context-specific training uses the same trajectory:

      python3 util/smt_sequence_training.py \
        "$AFL_OUT/<symcc-name>/.offline_trajectory.jsonl" \
        --output "$AFL_OUT/<symcc-name>/.smt_sequence_policy.json" \
        --timeout-sec 30 --max-clusters 8 --min-cluster-size 8

      python3 util/smt_sequence_training.py \
        --verify "$AFL_OUT/<symcc-name>/.smt_sequence_policy.json"

  Train on a completed tuning campaign, then set
  `SYMCC_SMT_ALGORITHM_PRIOR` for a separate holdout/confirmatory campaign.
  Do not train and evaluate on the same run when reporting performance.
  `timed_out` or killed events are right-censored and charged PAR-2 `2T`;
  older trajectory rows without explicit `timed_out` remain loadable but have
  weaker censoring provenance. Training bounds are configurable with
  `--max-events`, `--max-clusters`, `--min-cluster-size`,
  `--max-iterations`, `--bic-margin`, `--cost-weight`,
  `--min-propensity`, `--max-weight`, `--prior-strength`,
  `--confidence-z`, `--min-samples`, `--min-effective-samples`, and
  `--min-improvement`.

  F243 changes the default context contract from
  `symcc-smt-context-features-v1` (9 dimensions) to
  `symcc-smt-context-features-v2` (16 dimensions). The original ordered prefix
  remains bias, log input size, difficulty, timeout ratio, unknown ratio,
  dependency ratio, data uncertainty, branch pressure, and targeted. The
  appended dimensions are mean Query IR nodes/query, mean distinct input
  bytes/query, maximum bit width, and comparison/nonlinear/bitwise/structural
  operator ratios. Sizes use bounded logarithmic transforms and operator
  counts are divided by total Query IR nodes.

  QSYM telemetry reports the raw sufficient statistics as `query_exports`,
  `query_ir_nodes`, `query_ir_input_bytes`, `query_ir_max_bits`,
  `query_ir_comparison_ops`, `query_ir_nonlinear_ops`,
  `query_ir_bitwise_ops`, and `query_ir_structural_ops`. They are zero when no
  Query IR was successfully exported, including campaigns without
  `SYMCC_QUERY_SPOOL`. Offline trajectories preserve the raw counts so future
  feature schemas can be recomputed without rerunning the target.

  Existing v1 F239, F240, and F241 artifacts remain loadable without changing
  their digest: the verifier derives geometry and tree dimension from the
  exact sealed feature contract, and the scheduler projects a v2 context to
  its first nine dimensions. Existing nine-dimensional scheduler moment state
  is zero-extended on load. Unknown dimensions, reordered feature names, or
  malformed vectors are rejected rather than guessed.

  F240 bagged/boosted budgeted sequence training:

      python3 util/smt_sequence_optimizer.py \
        "$AFL_OUT/<symcc-name>/.offline_trajectory.jsonl" \
        --output "$AFL_OUT/<symcc-name>/.smt_sequence_ensemble.json" \
        --timeout-sec 30 --max-clusters 8 --min-model-samples 8 \
        --bag-estimators 7 --boost-rounds 5 --tree-depth 3 \
        --max-schedule-length 3 --slice-fractions 0.25,0.5,1

      python3 util/smt_sequence_optimizer.py \
        --verify "$AFL_OUT/<symcc-name>/.smt_sequence_ensemble.json"

  The optimizer learns completion, censored PAR-2 ratio, and adjusted reward
  with bounded inverse-propensity-weighted shallow CART bagging plus residual
  boosting. A bounded beam search evaluates global and per-X-means-cluster
  schedules under a shared timeout. `--uncertainty-z` controls completion/reward
  lower bounds and cost upper bounds; `--min-schedule-improvement` prevents a
  multi-action schedule from replacing the best single action without a
  conservative predicted improvement. Other bounds are `--min-leaf`,
  `--max-thresholds`, `--learning-rate`, `--beam-width`, `--reward-weight`,
  `--min-propensity`, `--max-weight`, and `--seed`.

  New trajectories record `instance_id` (input content SHA-256 when available),
  `solved`, and `budget_sec`. A censored stage is charged `2*budget_sec`, not
  `2*SYMCC_TIMEOUT`; old rows without the field use the global timeout.
  Executor-specific `timeout_scale` still applies after the schedule budget, so
  hold it fixed and record it in comparative experiment manifests.

- SYMCC_SEMANTIC_PROPOSALS=0/1 (default 1 when adaptive scheduling is enabled)
  and SYMCC_SEMANTIC_TOKEN_DIR=<dir>: Enable built-in semantic candidate
  generation before the verified-proposal funnel. The generator extracts bounded
  comparison cores, proposes inverse candidates, transfers data-coverage token
  exemplars, ranks IFSS-like relevance slices for Hydra-style targeted
  core-copy/swap/boundary/truncate transformations, performs bounded
  token-grammar `solve_complete` completion from AFL extras/string tokens and
  observed comparison-core fragments, and mutates UCSan alias/heap partitions.
  Every candidate still goes through target replay and global AFL bitmap triage
  before retention.

- SYMCC_GRAMMAR_RULES=N (default 2048, minimum 32, hard maximum 8192):
  Bound persistent online token-grammar productions. Rules are inferred from
  comparison-taint lexical spans plus configured token/string fragments and
  include literal, delimited, key-value, segment, choice, sequence, optional,
  repetition, and parser-induced bounded recursive forms. A recursive rule
  represents one validated `prefix + Nonterminal + suffix` expansion and
  applies at most one layer per proposal; low-yield, unretained rules are
  evicted first.

- SYMCC_GRAMMAR_MAX_SPAN=N (default 128, minimum 8, maximum 1024): Maximum
  number of bytes to which a comparison-taint core may expand while locating
  lexical token boundaries. Closed quote/bracket cores take precedence over
  outward expansion.

- SYMCC_GRAMMAR_DERIVATION_DEPTH=N (default 3, range 1--8): Maximum number of
  times one parser-accepted recursive CFG template may be composed around the
  current token in a single proposal. Each intermediate derivation is emitted
  separately and checked against `SYMCC_PROPOSAL_MAX_BYTES`; epsilon cycles are
  never learned. The state retains canonical productions, mutual/direct cycle
  paths, multi-slot provenance, and a one-to-many rule-to-cycle relation.

- SYMCC_GRAMMAR_PARETO=0/1 (default 1): Rank grammar and subtree rules with an
  explicit multi-objective frontier instead of the legacy scalar weighted
  score. The maximized objectives are target validation yield, AFL edge-feature
  yield, dynamic data-comparison progress, independently verified String-model
  yield, parser-production novelty, ECT subtree novelty, accepted-production
  posterior likelihood, packed-forest information/reachability, and scheduling
  age. Missing data/String or PCFG observations use a neutral Bayesian prior
  rather than being interpreted as success.

  For bounded cost, each context first forms a 256-rule archive by round-robin
  preservation of every objective's extremes. It then computes exact
  non-dominated fronts within that archive and uses normalized crowding
  distance to retain diverse trade-offs. The age objective and persisted
  `last_attempt_observation` prevent a valid but temporarily dominated rule
  from being permanently starved. Set this option to 0 for the F202/F203
  scalar-score ablation. Semantic state schema v25 persists Pareto counters,
  per-rule data/String observations, fairness state, and PCFG count evidence;
  it remains compatible with v1--v24.

- SYMCC_PARETO_CORPUS=0/1 (default 1): Maintain a bounded multi-objective
  metadata archive for seeds observed by the adaptive scheduler. Admission and
  replacement use six maximized objectives: owned AFL edge-feature gain,
  dynamic/static data-progress gain, concrete-verified String-model yield,
  structural-site diversity, path-hash ownership, and reward/cost efficiency.
  An existing entry that dominates a new seed rejects its metadata admission;
  a new entry that dominates existing entries replaces them.

  This archive never removes or rewrites AFL queue files. It controls only
  SymCC replay/scheduling metadata and contributes a bounded scheduling bonus,
  so AFL's authoritative coverage ownership and crash retention remain intact.
  On capacity overflow, an epsilon grid protects one extreme for every
  objective and evicts a low-utility entry from the densest remaining cell.

- SYMCC_PARETO_CORPUS_ENTRIES=N (default 4096, range 8--65536):
  Maximum number of seed metadata entries in the Pareto archive.

- SYMCC_PARETO_CORPUS_BINS=N (default 8, range 2--32):
  Number of epsilon-grid bins per objective for bounded density replacement.
  Adaptive scheduler state schema v12 persists all entries, counters, objective
  evidence, and eviction telemetry while accepting v1--v11 state.

  Grammar completion uses splice rather than fixed-width overwrite, so it can
  create shorter or longer inputs within `SYMCC_PROPOSAL_MAX_BYTES`. Proposal
  manifests bind a stable `grammar_rule_id`; concrete target validation updates
  rule validity and authoritative AFL retention updates rule/coverage yield.
  The generator state records attempted, validated, verified and retained rule
  coverage. None of these statistics bypass target replay or bitmap triage.

- SYMCC_QUERY_GRAMMAR_HOLES=0/1 (default 1 when both semantic proposals and
  the async QueryStore are enabled): Join a solver-materialized Query IR model
  with online grammar completion. QueryStore candidate manifests carry the
  exact Query IR input-byte read set and actual model-assignment offsets.
  Grammar spans that overlap queried bytes are rejected; every completed
  candidate is then re-evaluated against the stored Query IR before entering
  the proposal manager. Hidden `.NAME.query.json` sidecars are metadata and are
  excluded from the query-candidate work queue.

- SYMCC_QUERY_GRAMMAR_HOLE_MAX=N (default 16, range 0--64): Maximum verified
  Query-IR/grammar hole proposals considered per semantic observation before
  the global proposal limit. Zero is an ablation. `symcc-query-grammar-hole-v1`
  certificates bind query ID, source candidate/manifest digests, exact queried
  offsets, hole interval and grammar rule ID. The certificate records only the
  Query IR gate; concrete target replay and authoritative AFL retention remain
  mandatory independent gates.

- SYMCC_HISTORY_ACQUISITION_PLATEAU=N (default 64, range 1--65536):
  Consecutive semantic observations with zero global coverage delta required
  before retained-seed acquisition is enabled. Any positive coverage delta
  resets the counter. This keeps history crossover off the hot path while
  ordinary execution is still productive.

- SYMCC_HISTORY_ACQUISITION_SEEDS=N (default 128, range 1--4096) and
  SYMCC_HISTORY_ACQUISITION_BYTES=N (default 4096, range 64--65536): Bound the
  persistent bank of inputs that previously survived authoritative AFL novelty
  triage and the bytes retained from each input. During a plateau, lexical
  tokens from high-yield/underexplored retained seeds may replace current
  comparison spans as `history_acquisition` proposals. Seed ID, attempts,
  target validations, subsequent retentions and coverage yield are persisted.
  Every acquired candidate remains untrusted until concrete target replay and
  AFL novelty validation; retained history never authorizes solver or parser
  claims.

- SYMCC_QUERY_SPOOL=PATH (default unset): Export each interesting branch query
  as an immutable `symcc-query-ir-v1` envelope below `PATH/incoming`. The
  envelope contains a versioned expression DAG, prefix and target roots,
  concrete witness, metadata, and full/split SMT-LIB artifacts. Export uses a
  temporary file plus atomic rename. Without this variable, query export is
  disabled.

- SYMCC_QUERY_DEFER=0/1 (default 0): When query export succeeds, skip the
  corresponding inline Z3 solve and leave it to the asynchronous query service.
  An export failure always falls back to the inline solver. Enable this only
  when `symcc_query_service.py` is running; leaving it at 0 permits shadow-mode
  comparison between inline and asynchronous solving.

- SYMCC_QUERY_OUTPUT_DIR=PATH (default `SYMCC_OUTPUT_DIR`): Directory into which
  SAT assignments from asynchronous queries are materialized as concrete input
  candidates. In the MPI integration these candidates re-enter the normal
  feedback queue and are retained only after authoritative AFL bitmap triage.

- SYMCC_QUERY_MAX_NODES=N (default 65536, maximum 250000): Maximum number of
  expression DAG nodes exported for one query. Queries exceeding the limit
  retain the inline fallback.

- SYMCC_ASYNC_QUERY_WORKERS=N (default 0): Start N persistent query-solver
  workers in the MPI master. This also configures a shared spool, query store,
  and candidate directory for SymCC workers. Set `SYMCC_QUERY_DEFER=1` for full
  tracer/solver separation. The semantic grammar-hole generator receives the
  shared QueryStore only after this service process starts successfully and
  only when `SYMCC_QUERY_GRAMMAR_HOLES=1`. Zero workers or a failed service
  launch fail closed to ordinary grammar generation with no QueryStore-backed
  holes; parser replay, target validation and AFL novelty remain mandatory.

- SYMCC_QUERY_STORE=PATH (default
  `$AFL_OUT/<symcc-name>/.query_store`): SQLite/WAL index and immutable
  content-addressed artifacts used by the asynchronous query service.

- SYMCC_QUERY_SOLVER=COMMAND (default auto-discovered
  `symcc-query-solver`): Solver helper command. Each service worker starts one
  long-running `--server` process.

- SYMCC_QUERY_SOLVER_PORTFOLIO=<json-or-path> (default empty): Configure a
  bounded exact-solver portfolio for `symcc_query_service.py`. The JSON format
  accepts two backend kinds:

    {"solvers":[
      {"kind":"symcc-json","name":"z3",
       "command":["symcc-query-solver"],"persistent":true},
      {"kind":"smtlib-qfbv","name":"cvc5",
       "command":["cvc5","--lang","smt2","--produce-models",
                  "--tlimit-per={timeout_ms}","{query}"],
       "capabilities":{"logic":"QF_BV","max_bits":4096,
                       "max_nodes":250000,"max_input_bytes":4096,
                       "accept_unsat":true}}
    ]}

  `symcc-json` is the existing helper JSON protocol; persistent entries use
  `--server`, while non-persistent entries receive `QUERY TIMEOUT_MS`.
  A non-persistent `smtlib-qfbv` entry lowers the content-addressed Query IR
  itself instead of replaying Z3's printed SMT text. `{query}` and
  `{timeout_ms}` placeholders may appear inside argv entries. If `{query}` is
  absent, the temporary SMT-LIB path is appended. F238 also supports:

    {"kind":"smtlib-qfbv","name":"cvc5-incremental",
     "command":["cvc5","--lang","smt2","--incremental",
                "--produce-models"],
     "persistent":true,"prefix_cache":4,
     "capabilities":{"incremental":true,"accept_unsat":true}}

  Persistent commands cannot contain `{query}` or `{timeout_ms}`. Each exact
  `prefix_key` owns one interactive solver process. Prefix roots are asserted
  once; each target uses `push -> assert -> check-sat/get-value -> pop`.
  Target-only input declarations may be added between requests. `prefix_cache`
  is an LRU process bound in `[1,64]`, default 4. Process closure, malformed
  output, timeout, or prefix-digest mismatch destroys that context; a later
  request rebuilds it cold. Request wall time is enforced externally even when
  the solver has no portable per-check timeout option. The service-level
  `--portfolio` option overrides this environment variable.

  An `smtlib-qfbv` capability contract has schema
  `symcc-qfbv-capability-v1`. `operators` defaults to the complete Query IR
  QF_BV set; `max_bits`, `max_nodes`, and `max_input_bytes` are hard lowering
  bounds. Unsupported operators, sort/width/arity mismatches, and bound
  violations return `unknown` before a solver process starts. `model_values`
  must be true. `incremental` defaults to false and must be true for a
  persistent entry. `accept_unsat` defaults to false: an external UNSAT is retained
  as raw telemetry but downgraded to `unknown` unless the experiment explicitly
  authorizes that backend as an exact UNSAT authority.

  Lowering emits `symcc-qfbv-lowering-v1` with canonical capability, input-set,
  SMT-LIB and certificate digests, exact operator counts, maximum width, and
  sort proof status. SAT uses standard SMT-LIB `get-value` for every 8-bit input
  offset. The adapter patches the concrete witness and checks all Query IR roots;
  `QueryStore.complete()` repeats that check against its independently loaded
  CAS expressions before persisting the result. Missing/malformed model values,
  a false model, certificate tampering, or a query-id mismatch therefore cannot
  enter the SAT cache. The current lowerer covers QF_BV only; arrays, floating
  point, strings, cross-worker clause transport, and proof-producing UNSAT
  require separate capability or evidence layers.

  Portfolio results include a `symcc-solver-portfolio-v1` object with every
  attempt's name, status, solver, elapsed time, prefix-cache hit,
  backend/capability status, context protocol, model/UNSAT authorization bits,
  certificate digests, and bounded reason. A SAT/UNSAT conflict across portfolio members is recorded as
  `disagreement=true` and conservatively returned as `unknown`, so a disputed
  result is not cached as a proof or model. Query-store stats expose
  `portfolio_results` and `portfolio_disagreements`.

- SYMCC_QUERY_SOLVER_PORTFOLIO_PARALLELISM=N (default number of configured
  portfolio solvers, maximum 64): Maximum number of solver backends run
  concurrently for one portfolio query. The service-level
  `--portfolio-parallelism` option overrides this default.

- SYMCC_QUERY_SOLVER_PORTFOLIO_CANCEL_GRACE_MS=N (default -1/disabled, range
  -1--60000): With -1, the portfolio waits for all launched attempts before
  choosing a winner, preserving complete SAT/UNSAT disagreement observation.
  A nonnegative value starts a bounded cross-check window only after a SAT
  result. At expiry, queued futures are cancelled and running helpers receive a
  query-scoped process-group interrupt. UNSAT never triggers cancellation.
  `--portfolio-cancel-grace-ms` overrides the environment; 0 requests immediate
  cancellation after processing results already completed in the same wait
  batch.

  Interrupted persistent JSON servers respawn on the next query. Interrupted
  prefix-persistent QF_BV contexts are removed and rebuilt cold. Every SAT
  winner still passes QueryStore's exact model validation; an invalid early SAT
  is rejected but may have cancelled a slower valid fallback. Portfolio
  telemetry exposes `cancellation_enabled`, `cancel_grace_ms`,
  `cancel_requested`, `cancelled_attempts`, and `consensus_complete`; attempts
  expose `cancelled/cancel_reason`. QueryStore stats expose
  `portfolio_cancel_requests`, `portfolio_cancelled_attempts`, and
  `portfolio_incomplete_consensus`. Elapsed time remains wall-clock time through
  cancellation and helper cleanup.

- SYMCC_QUERY_TRAVERSAL=dfs|bfs|priority (default dfs): Prefix-trie work
  ordering used by the MPI-launched service. The standalone service exposes the
  equivalent `--traversal` option. Prefix ownership is deterministically
  sharded across worker slots so repeated prefixes reach the same solver cache.

- SYMCC_QUERY_PREFIX_CACHE=N (default 128, maximum 65536): Number of parsed
  prefix solver contexts retained by each persistent helper. A query loads its
  target under `push`, checks it, and then `pop`s back to the immutable prefix.

- Query/schedule joint validation: `symcc_query_service.py` accepts
  `--schedule-constraints PATH`, `--schedule-validation-out PATH`,
  `--schedule-validation-max-artifacts N`, and `--schedule-validation-only`.
  It matches schedule artifacts to queries by explicit `query_id` when present,
  otherwise by `target_branch` against bounded Query IR metadata (`site`,
  `target_branch`, `target_site`, or `branch`). The query store persists
  validation rows in SQLite table `joint_schedule_validations` and immutable
  JSON files under `$SYMCC_QUERY_STORE/joint_schedule/<hash-prefix>/`.

- SYMCC_GENERATOR_SAMPLES=N (default 4, maximum 64): Number of
  solver-verified candidate models that `symcc-query-solver` attempts to embed
  in a reusable `symcc-solution-generator-v1` result after a SAT query. Set this
  to 0 to persist the generator IR, fixed assignments, computed byte ranges, and
  fields without spending time on additional checked samples.

- SYMCC_GENERATOR_MAX_VARS=N (default 4, maximum 64): Maximum number of input
  byte variables for which the persistent query solver computes exact
  per-byte feasible lower/upper bounds. Variables outside the budget stay fixed
  to the primary model in the emitted generator.

- SYMCC_GENERATOR_CHECK_TIMEOUT=N (default min(100, query timeout)): Per-check
  timeout in milliseconds for generator range probing and sample validation.
  Unknown results narrow or reject generator candidates; they are not emitted as
  verified models.

- SYMCC_GENERATOR_OPTIMISTIC=0|1 (default 1): In persistent prefix/target
  queries, compute generator ranges and proposals against the target assertions
  with prefix assertions removed. The emitted
  `symcc-optimistic-simplification-v1` certificate records the original query
  hash and complete kept/dropped assertion partition. Every proposal is still
  checked with all prefix and target assertions in the original solver;
  `unsat`/`unknown` candidates are rejected. Set this to 0 for exact full-PC
  ranges. One-shot queries and queries without a separable prefix stay exact.

- SYMCC_GENERATOR_TACTIC_CONVERTER=0|1 (default 1): Apply the native Z3
  `simplify` then `solve-eqs` tactic pipeline to the generator proposal goal,
  enumerate a bounded number of subgoal models, and use Z3's model converter to
  recover eliminated input variables. Converted assignments are accepted only
  after the original full-prefix solver returns SAT. Tactic failure is local
  and falls back to range sampling.

- SYMCC_GENERATOR_CONVERTER_SAMPLES=N (default 2, maximum 64): Maximum number
  of full-solver-accepted models requested from the native tactic converter.
  The value is also capped by `SYMCC_GENERATOR_SAMPLES`; subgoal enumeration
  attempts are bounded to four times this value.

- SYMCC_GENERATOR_REPLAY_SAMPLES=N (default 8, maximum 64, 0 disables):
  Maximum number of candidates materialized per witness by replaying a
  persisted solution generator in QueryStore. Query-IR converter recipes,
  ranges, and field samples are proposals only. Every replayed byte string
  must satisfy all persisted prefix and target roots in the bounded Query IR
  evaluator before materialization; concrete replay remains required.

- Solution generator artifacts: asynchronous query results may contain a
  `generator` object and `generator_hash`. The query store writes canonical
  generator JSON to
  `$SYMCC_QUERY_STORE/generators/<hash-prefix>/<hash>.json`, records the same
  generator in SQLite, and materializes every solver-verified model as a normal
  candidate manifest with `solver_verified=true` and `verified=false` until
  concrete replay. Offline generator replay candidates are separately marked
  `generator_replay_verified=true`, `query_ir_verified=true`, and
  `solver_verified=false`.

- SYMCC_PARTIAL_SOLUTION_CACHE=0|1 (default 1): Enable the
  PSCache-inspired partial-solution cache in the asynchronous query store. SAT
  primary assignments and solver-verified generator models are persisted as
  `symcc-partial-solution-v1` records. A later query only receives a candidate
  after bounded Query IR evaluation proves that the patched witness satisfies
  every prefix root and the target root. A partial hit never marks a query SAT
  or UNSAT; it only emits a candidate for ordinary concrete replay.

- SYMCC_PARTIAL_SOLUTION_LIMIT=N (default 8, maximum 256): Maximum number of
  Query-IR-verified partial candidates materialized for one query.

- SYMCC_PARTIAL_SOLUTION_SCAN=N (default 512, maximum 65536): Number of recent
  partial solutions considered when looking for reusable assignments.

- SYMCC_PARTIAL_SOLUTION_PENDING_QUERIES=N (default 64, maximum 4096): Number
  of pending queries rescanned after a SAT completion writes new partial
  solutions.

- SYMCC_SOLVER_PSCACHE=0|1 (default 1 in `symcc-query-solver --server`):
  Enable solver-helper-internal partial-solution probing. The persistent helper
  remembers recent SAT input-byte assignments and, before a normal Z3 check,
  briefly asserts a bounded number of cached assignments against the current
  prefix+target solver context. A hit returns SAT only after Z3 checks the
  current query under the cached assignment; a miss falls through to the normal
  solver and is not treated as UNSAT evidence.

- SYMCC_SOLVER_PSCACHE_SIZE=N (default 128, maximum 65536): Number of recent
  SAT assignment maps retained by the persistent helper.

- SYMCC_SOLVER_PSCACHE_ASSIGNMENTS=N (default 64, maximum 4096): Maximum input
  byte assignments retained from one SAT model for solver-internal probing.

- SYMCC_SOLVER_PSCACHE_PROBES=N (default 4, maximum 128): Maximum cached
  assignment maps probed before a full solve.

- SYMCC_SOLVER_PSCACHE_TIMEOUT=N (default min(25, query timeout) ms, maximum
  1000 ms): Timeout for each solver-internal partial-solution probe. Results
  expose `solver_pscache_hit` and `solver_pscache_probes`; QueryStore stats
  include `solver_pscache_hits`.

- SYMCC_SOLVER_PSCACHE_CONFLICTS=0|1 (default 1): Enable proof-carrying
  assumption-conflict collection in the persistent QF_BV helper. The helper
  projects the current concrete witness and failed cached probes to numeric
  input-byte equalities, calls Z3 with those equalities as assumptions, and
  retains a record only when Z3 returns UNSAT with a non-empty assumption
  core. A second check revalidates the retained core. If the formula is UNSAT
  without any byte assumption, minimization reaches the empty core and the
  record is discarded.

- SYMCC_SOLVER_PSCACHE_CONFLICT_ASSIGNMENTS=N (default 64, maximum 4096):
  Maximum input-byte equalities projected from one concrete witness for an
  assumption-conflict check.

- SYMCC_SOLVER_PSCACHE_CONFLICT_SOLUTIONS=N (default 16, maximum 64):
  Maximum distinct failed cached assignments exported from one helper request.
  The current witness may add one record; the serialized result has an
  unconditional hard bound of 64 records.

- SYMCC_SOLVER_PSCACHE_CONFLICT_CORE_CHECKS=N (default 8, range 0--4096):
  Deletion checks used to minimize each Z3 assumption core. Exhausting the
  budget or receiving unknown preserves a verified non-minimal core and sets
  `core_minimal=false`; it never upgrades an unproved core. Every retained
  core receives a final UNSAT recheck.

- SYMCC_SOLVER_PSCACHE_CONFLICT_TIMEOUT=N (default min(25, query timeout) ms,
  maximum 1000 ms): Per-check timeout for witness conflict extraction, core
  deletion, and final core verification. Timeout/unknown yields no conflict
  claim for the affected check.

  Helper results expose `solver_pscache_conflict_checks` and bounded
  `symcc-solver-conflict-solution-v1` records containing the full projected
  byte assignment, non-empty core assignment, source, proof kind, minimization
  status, and check count. QueryStore validates their types and subset
  relation, adds canonical certificate hashes, independently checks that the
  assignment fails the source Query IR, and persists only such records.
  SQLite `query_literals` and `partial_solution_literals` normalize nested
  logical negation into signed literal identities, so positive-prefix and
  off-path evidence participates in relevance ranking. Future candidates
  still require complete Query IR validation and ordinary concrete replay.

- SYMCC_SELECTIVE_QUERY=0|1 (default 1 in persistent
  `symcc-query-solver --server`): Before a full query solve, build an
  assertion-to-input-byte dependency hypergraph and close the target assertion's
  byte set through every connected prefix assertion. Bytes in disconnected
  components may be fixed to the QueryStore concrete witness for one short
  selective SAT probe. A selective SAT model is exact for the full query.
  Selective UNSAT, unknown, timeout, malformed/missing witness, or budget
  rejection always falls through to the ordinary full solver and can never
  populate an UNSAT proof.

- SYMCC_SELECTIVE_QUERY_MIN_FIXED=N (default 2, maximum 4096): Minimum number
  of disconnected witness bytes required before attempting a selective probe.

- SYMCC_SELECTIVE_QUERY_MAX_FIXED=N (default 64, maximum 4096): Maximum
  disconnected bytes fixed in one selective probe.

- SYMCC_SELECTIVE_QUERY_MAX_SYMBOLIC=N (default 16, maximum 4096): Maximum
  byte variables left symbolic after fixing. Queries above this bound go
  directly to the full solver.

- SYMCC_SELECTIVE_QUERY_TIMEOUT=N (default min(50, query timeout) ms, maximum
  1000 ms): Maximum total short-probe timeout. The learned policy may reduce
  this value from per-context selective/full-solve EWMA, but never increases
  it or the query timeout.

- SYMCC_SELECTIVE_QUERY_COMPLETIONS=N (default 1, range 0--8): Number of
  disconnected-component completions attempted inside the total short-probe
  timeout. The bounded sequence is concrete witness, all-zero, all-0xff, then
  deterministic query-seeded random assignments; duplicate assignments are
  skipped. Setting 0 is a mechanism ablation. Every completion retains the
  complete prefix+target query, so only SAT is authoritative.

- SYMCC_SELECTIVE_QUERY_LEARNING=0|1 (default 1): Enable contextual online
  selection of whether a structurally eligible query should receive the short
  probe. Context keys bucket assertion count, byte-variable count, target
  dependency ratio, fixed-byte count, AST size, and costly bit-vector
  operations. Value 0 keeps the F188 structural policy.

- SYMCC_SELECTIVE_QUERY_POLICY_EXPLORE=N (default 4, range 0--1024): Forced
  cold-start attempts per context before the cost-aware decision is used.

- SYMCC_SELECTIVE_QUERY_POLICY_MIN_SAVINGS_US=N (default 100, range
  0--3600000000): Minimum optimistic expected solver-time saving needed for a
  learned attempt after cold start.

- SYMCC_SELECTIVE_QUERY_POLICY_MIN_TIMEOUT=N (default 5 ms, range 1--1000):
  Lower bound when the learned EWMA predictor reduces the selective timeout.

- SYMCC_SELECTIVE_QUERY_POLICY_STATE=PATH (default: query service creates
  `STORE/policies/selective-worker-W-backend-B.state`): Versioned bounded
  per-worker/backend policy state. Explicit paths should not be shared by
  concurrently writing helpers. A corrupt or incompatible file is ignored.

- SYMCC_SELECTIVE_QUERY_POLICY_CONTEXTS=N (default 256, range 1--4096):
  Maximum learned structural contexts. Least-observed contexts are evicted.

- SYMCC_SELECTIVE_QUERY_POLICY_SAVE_INTERVAL=N (default 1, range 1--4096):
  Number of new observations between atomic state-file replacements.

  Result artifacts expose eligibility, decision/context, predicted savings,
  learned timeout, completion count/hit index, policy observations, full-solve
  EWMA, and the original attempted/hit/symbolic/fixed/elapsed fields.
  QueryStore stats additionally expose learned skips and non-witness completion
  hits. Tunable mechanism parameters are present in the conditional
  self-configuration schema; state paths and storage limits are operational
  controls and are not sampled.

- Partial-solution artifacts: cache rows live in SQLite tables
  `partial_solutions`, `partial_solution_clauses`,
  `partial_solution_literals`, `query_literals`, and
  `partial_solution_candidates`. Lookup prioritizes normalized signed-literal
  overlap, then source-clause overlap, before applying the mandatory Query IR
  verifier. Conflict-derived rows include `provenance`, a canonical proof JSON,
  and an independently checked source-verification bit. Candidate manifests
  use `symcc-query-candidate-v1` with
  `solver_verified=false`,
  `partial_solution_hash`, `partial_solution_source_query_id`,
  `partial_solution_verified=true`, `query_ir_verified=true`, and
  `verified=false`. External query-output directories receive
  `async-partial-*` files that flow through the same MPI/AFL feedback path as
  exact solver candidates.

- F241 schedule-level SMBO artifacts are trained from an already verified F240
  ensemble and can be passed through the existing
  `SYMCC_SMT_ALGORITHM_PRIOR=PATH` interface:

      python3 util/smt_schedule_smbo.py \
        .smt_sequence_ensemble.json --output .smt_schedule_smbo.json \
        --evaluation-budget 64 --initial-design 12 \
        --max-candidates 1024 --max-schedule-length 3 \
        --slice-fractions 0.25,0.5,1 \
        --bag-estimators 5 --boost-rounds 3 --tree-depth 3
      python3 util/smt_schedule_smbo.py --verify .smt_schedule_smbo.json

  `--evaluation-budget` is the maximum number of schedule objectives visible
  to acquisition (4--512). `--initial-design` is the requested deterministic
  initial size (4--128), and the actual design always includes every
  single-action/budget baseline. `--max-candidates` is 8--4096 and must also
  contain all such baselines. `--max-schedule-length` is 1--8.
  `--exploration` is EI xi (0--1), `--uncertainty-floor` is the minimum sigma,
  and `--action-uncertainty-z`, `--reward-weight`, and
  `--min-schedule-improvement` retain F240's conservative schedule semantics.
  Tree count/depth/leaf/threshold and learning-rate flags bound the
  schedule-level acquisition surrogate independently of F240's action models.

  Artifact schema `symcc-smt-schedule-smbo-policy-v1` records selection
  `evaluations` separately from `posthoc_oracle_evaluations`. The latter are
  computed only after selection to diagnose simple regret and must be charged
  equally or disabled conceptually in optimizer-cost comparisons. Loading
  fails closed on any F240 proof, digest, candidate, trace, or replay mismatch.
  Runtime state reports
  `prior_kind=smbo-expected-improvement-sequence`; the schedule remains a 90/10
  preference and does not grant additional solver-result authority.

- F244 fixed-version QF_BV backend conformance:

      # Reproducibly build the official Bitwuzla 0.9.1 tag/commit under
      # $HOME/.local/opt/bitwuzla-0.9.1.
      benchmark/install_bitwuzla_0_9_1.sh
      export PATH="$HOME/.local/opt/bitwuzla-0.9.1/bin:$PATH"

      # Run pinned Z3 4.8.12, cvc5 1.1.2, and Bitwuzla 0.9.1.
      python3 util/qf_bv_conformance.py --output qfbv-evidence.json
      python3 util/qf_bv_conformance.py --verify qfbv-evidence.json
      python3 util/qf_bv_conformance.py \
        --replay qfbv-evidence.json --output qfbv-replay.json

  Default evidence requires exact versions Z3 4.8.12, cvc5 1.1.2, and
  Bitwuzla 0.9.1.
  `--backend-config` accepts a JSON file or inline list of objects with
  `name`, `command`, `version_command`, and exact `expected_version`.
  Commands use the same `{query}` and `{timeout_ms}` placeholders as the
  one-shot QF_BV query-service adapter. Missing executables, version mismatch,
  malformed models, incomplete operator coverage, untrusted UNSAT acceptance,
  certificate mismatch, or digest mismatch fail closed.

  Schema `symcc-qfbv-backend-conformance-v1` binds the canonical 38-operator
  SAT matrix, contradictory UNSAT probe, absolute executable identity and
  SHA-256, exact version output, capabilities, lowering certificates, and
  QueryStore completion. `artifact_sha256` seals the complete run.
  `semantic_sha256` excludes timestamp, elapsed time, and host-specific binary
  path/hash so `--replay` can compare solver semantics across runs. Offline
  `--verify` reconstructs Query IR identities and lowering certificates without
  executing a solver. The checked result is
  `benchmark/evidence/qfbv_conformance_f244.json`.

- F245 sealed paired QF_BV holdout campaigns:

      python3 util/qf_bv_campaign.py \
        --corpus /path/to/frozen/query-spool \
        --conformance benchmark/evidence/qfbv_conformance_f244.json \
        --split-seed frozen-study-seed --split-parts 5 --holdout-parts 1 \
        --timeout-ms 5000 --repetitions 20 --confirmatory \
        --output qfbv-holdout.json
      python3 util/qf_bv_campaign.py --verify qfbv-holdout.json
      python3 util/qf_bv_campaign.py \
        --replay qfbv-holdout.json --output qfbv-holdout-replay.json

  `--corpus` accepts a Query IR envelope JSON, list/`queries` bundle, JSONL,
  or directory (`*.query.json` preferred), bounded to 4096 unique queries and
  256 MiB. `SHA256(split_seed:query_id) mod split_parts` assigns the first
  `holdout_parts` buckets to holdout. Only holdout tasks execute. `--backends`
  optionally selects comma-separated names already certified by the embedded
  conformance artifact. Every current executable version and file SHA must
  still match before execution.

  Repetitions run one-shot tasks in a stable hash-randomized order with equal
  query count and wall timeout. The artifact records elapsed time, child
  user+system CPU, censored PAR-2, model/trust evidence, backend totals, and
  pairwise solved quadrants/disagreements/PAR-2 deltas. `--verify` reconstructs
  the corpus split, task set, lowering, SAT witnesses, PAR-2, and aggregates
  without running a solver. `--confirmatory` requires at least 20 repetitions,
  a non-synthetic corpus, and a non-empty disjoint training split.

  `--smoke-corpus` exists only for functional validation and is rejected by
  confirmatory mode. The checked non-performance smoke artifact is
  `benchmark/evidence/qfbv_holdout_f245_smoke.json`.

- F246 train-sealed QF_BV strategy campaigns:

      python3 util/qf_bv_strategy_campaign.py \
        --base-campaign qfbv-holdout.json \
        --training-trajectory train-trajectory.jsonl \
        --beam-policy .smt_sequence_ensemble.json \
        --smbo-policy .smt_schedule_smbo.json \
        --timeout-ms 5000 --cancel-grace-ms 50 \
        --repetitions 20 --confirmatory \
        --output qfbv-strategies.json
      python3 util/qf_bv_strategy_campaign.py \
        --verify qfbv-strategies.json
      python3 util/qf_bv_strategy_campaign.py \
        --replay qfbv-strategies.json \
        --output qfbv-strategies-replay.json

  Every JSONL training event must contain `context.query_id` naming a query in
  the embedded F245 train split. The tool normalizes the events, retrains F240
  from them, retrains F241 from F240, and requires exact artifact equality.
  Modeled action names must exactly equal the selected F244-certified backend
  names. The F240/F241 timeout must equal `--timeout-ms`, and every sequence's
  stage budgets must sum to at most that value.

  The task matrix includes one individual arm per backend, `f240-beam`,
  `f241-smbo`, and `f242-parallel-grace-Nms`. `--cancel-grace-ms` is 0--60000;
  only a validated SAT result starts cancellation, while UNSAT collects all
  attempts. The artifact stores full internal attempts, child CPU, wall,
  PAR-2, cancel/incomplete-consensus counters, structural feature decisions,
  and paired strategy aggregates. Equal logical query count/shared declared
  wall budget does not make parallel CPU equal; use CPU quotas or
  coverage/CPU-hour for confirmatory interpretation.

  `--smoke-policy` deterministically builds a synthetic train-only F240/F241
  bundle for functional testing and is rejected by confirmatory mode. The
  checked non-performance artifact is
  `benchmark/evidence/qfbv_strategy_f246_smoke.json`.

- F247 sealed AFL edge/data coverage join:

      cc -O2 -shared -fPIC util/afl_data_coverage_rt.c \
        -o build/libafl_data_coverage_rt.so -ldl
      afl-clang-fast -O0 -g -fno-builtin \
        benchmark/qfbv_coverage_smoke.c \
        -o build/qfbv_coverage_smoke_afl
      python3 util/qf_bv_coverage_join.py \
        --strategy-campaign qfbv-strategies.json \
        --target-command-json \
          '["/absolute/path/to/afl-target","@@"]' \
        --data-preload /absolute/path/to/libafl_data_coverage_rt.so \
        --showmap afl-showmap --timeout-ms 1000 \
        --map-repetitions 2 \
        --output qfbv-coverage.json
      python3 util/qf_bv_coverage_join.py --verify qfbv-coverage.json
      python3 util/qf_bv_coverage_join.py --replay qfbv-coverage.json \
        --output qfbv-coverage-replay.json

  The command must contain exactly one `@@`. The target, `afl-showmap`, and
  preload absolute paths, file SHA-256 values, showmap version, and timeout are
  sealed. Every SAT assignment in the verified F246 source is materialized;
  candidates and original witnesses are deduplicated by content SHA-256 and
  replayed through persistent `afl-showmap -S -e` edge/data oracles.

  Both oracles load the same preload so PCGUARD edge IDs have the same layout.
  The edge oracle sets `AFL_DATA_COVERAGE=0` and
  `SYMCC_AFL_DATA_COVERAGE=0`; the combined oracle sets both to `1`.
  The preload reserves IDs `0..65535` as its data namespace before AFL++
  forkserver map negotiation, while PCGUARD edge IDs are allocated above it.
  The verifier requires identical status, `edge_ids subset combined_ids`, and
  every extra data ID below 65536. Do not compare a no-preload edge map with a
  preload combined map because their PCGUARD IDs are not comparable.

  `SYMCC_AFL_DATA_MAP_SIZE=N` optionally narrows data hashing to the first
  `N` slots, where `1 <= N <= 65536`; invalid or larger values retain 65536.
  It does not resize the AFL shared memory and must not be confused with
  AFL++'s internal `__AFL_MAP_SIZE` allocation limit. The normal public switch
  remains `SYMCC_AFL_DATA_COVERAGE=0/1`; `AFL_DATA_COVERAGE=0/1` is the
  emergency runtime alias.

  `--map-repetitions` is 1--100. Each input must produce an identical status
  and sparse bitmap in every repetition. `--confirmatory` additionally
  requires at least two map repetitions and a verified confirmatory F246
  source, which itself requires a non-synthetic corpus and at least 20
  repetitions. The artifact reports candidate-vs-witness edge/data novelty,
  per-strategy union gain, coverage per solver child CPU second, pairwise
  complementarity, and F243 feature-schema v1/v2 Brier/log-loss/ECE
  calibration. Showmap replay CPU is reported separately.

  `benchmark/evidence/qfbv_coverage_f247_smoke.json` and
  `benchmark/qfbv_coverage_smoke.c` are functional evidence only. They contain
  four synthetic holdout queries and must not be used to rank strategies or
  make coverage-performance claims.

- F248/F268/F272/F273/F287/F288 Hydra profile/transform/original-replay pipeline:

      # Build and run this exact baseline to produce telemetry first.
      symcc -O0 target.c -o build/target.original

      python3 util/hydra_transform.py profile telemetry/*.json \
        --profiled-command-json '["/abs/build/target.original"]' \
        --profile-output build/hydra.profile \
        --artifact-output results/hydra-profile.json

      # Build one transformed site. Use a fresh manifest.
      SYMCC_HYDRA=1 \
      SYMCC_HYDRA_PROFILE=build/hydra.profile \
      SYMCC_HYDRA_MODE=aggressive \
      SYMCC_HYDRA_MANIFEST_OUT=build/hydra-manifest.jsonl \
        symcc -O0 target.c -o build/target.hydra
      python3 util/verify_hydra_transform_manifest.py \
        build/hydra-manifest.jsonl

      # Run the transformed target through the normal SymCC exploration, then
      # replay every generated input on both binaries.
      python3 util/hydra_transform.py campaign \
        --original-command-json '["/abs/build/target.original"]' \
        --transformed-command-json '["/abs/build/target.hydra"]' \
        --input-dir /abs/transformed-output \
        --site <manifest-site> \
        --manifest build/hydra-manifest.jsonl \
        --profile-artifact results/hydra-profile.json \
        --denylist-output build/hydra-denylist.txt \
        --output results/hydra-replay.json
      python3 util/hydra_transform.py verify results/hydra-replay.json
      python3 util/hydra_transform.py replay results/hydra-replay.json \
        --output results/hydra-replay-check.json

  Commands may contain one `@@` file placeholder; otherwise input bytes are
  provided on stdin. Campaign bounds are 16,384 inputs, 16 MiB per input,
  256 MiB total and 1--3,600,000 ms timeout. Exit 0 means the artifact verifies
  and no failure-preservation violation was observed; exit 2 means at least one
  input failed only on the original, so the transformed build is rejected.
  A transformed-only failure is not an error in aggressive mode: it is omitted
  from `accepted_failure_inputs` and its unique selected site is emitted to the
  denylist. The checked mechanism-only evidence is
  `benchmark/evidence/hydra_f248_smoke.json`. F268's compiler regression checks
  an equal 2x2 region on all 256 byte values, structure-manifest tampering and
  symbolized LLVM verification. F272 additionally checks a 2x1 region with a
  one-sided edit and a 1x4 cross-block def-use region on all 256 byte values,
  v2 block-ordinal/edit-distance tampering through both the direct verifier and
  campaign gate, and rejection of a fifth pure-linear arm block. F273 checks
  3x1 and maximal 7x7 internal trees plus an aggressive matched-store tree on
  all 256 byte values, validates symbolized IR, rejects parent/leaf/successor
  tampering, and keeps a fourth internal branch, empty alignment and
  tree-local reconvergence unchanged under v3. F287 upgrades the supported
  reconvergence case to v4: a maximum test has two left and one right local
  merge, three local PHIs and two output PHIs; a separate aggressive-memory
  test predicates a matched readback store. Both compare all 256 byte inputs.
  Predecessor/local-PHI/lowered-IR tampering is rejected, while external
  predecessors, cycles and a fourth local merge remain unchanged. A
  branch-only chain with no local merge and a 1x5 linear region also remain
  rejected instead of bypassing the older schema bounds.
  F288 additionally checks v1 compatibility, strict v2 fail-closed parsing,
  profile/manifest/original-command identity, command replacement rejection
  and 24 concurrent `opt` processes appending 24 independently verified JSONL
  records. The historical smoke artifact remains replay-v1 evidence and does
  not carry the v2 binary-identity claim.

- F274 unified continuation/loop/Hydra transformation seal and independent
  replay:

      # Continuation. The manifest determines memory-on versus structural-only.
      python3 util/seal_transform_artifact.py seal \
        --pipeline continuation \
        --manifest continuation=continuations.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --output transformation.seal.json

      # A loop may carry recurrence evidence, exit evidence, or both.
      python3 util/seal_transform_artifact.py seal \
        --pipeline loop \
        --manifest loop-recurrence=loops.jsonl \
        --manifest loop-exit=loop-exits.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --output transformation.seal.json

      # Hydra requires exactly one record and restores its site and mode.
      python3 util/seal_transform_artifact.py seal \
        --pipeline hydra --manifest hydra=hydra.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --output transformation.seal.json

      python3 util/seal_transform_artifact.py verify \
        --pipeline hydra --manifest hydra=hydra.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --seal transformation.seal.json

      python3 util/replay_transform_artifact.py \
        --pipeline hydra --manifest hydra=hydra.jsonl \
        --input-ir input.ll --lowered-ir lowered.ll \
        --compiler build/libsymcc.so --llvm-tool /path/to/opt \
        --seal transformation.seal.json

  Repeat `--manifest KIND=PATH` for each loop proof kind. Pipeline/kind
  mismatches and duplicate kinds are rejected. Seal creation independently
  verifies every manifest, binds ordered proof identities, input/lowered IR,
  compiler, LLVM tool and LLVM version, refuses an existing output and commits
  through lock/fsync/atomic rename. Replay clears inherited transformation
  variables and independently reruns the exact pass pipeline from `input.ll`;
  regenerated manifests must be record-identical, regenerated textual IR must
  be SHA-256-identical and LLVM-verifier clean, and the seal is checked again
  after replay. Generate `lowered.ll` with the same deterministic `opt -S`
  invocation. This is local exact artifact replay, not a signature, remote
  attestation, transparency log or cross-version semantic equivalence proof.

- F289 signed, transparency-logged cross-host transformation bundle:

      # Provision artifact and log keys separately. Private outputs are 0600.
      python3 util/transform_artifact_bundle.py keygen \
        --private-key keys/artifact-private.pem \
        --public-key keys/artifact-public.pem
      python3 util/transform_artifact_bundle.py keygen \
        --private-key keys/log-private.pem \
        --public-key keys/log-public.pem

      # The roles must exactly match the F274 seal.
      python3 util/transform_artifact_bundle.py publish \
        --seal transformation.seal.json \
        --artifact input-ir=input.ll \
        --artifact lowered-ir=lowered.ll \
        --artifact compiler=build/libsymcc.so \
        --artifact llvm-tool=/path/to/opt \
        --artifact manifest:hydra=hydra.jsonl \
        --private-key keys/artifact-private.pem \
        --public-key keys/artifact-public.pem \
        --log results/transformation-transparency.jsonl \
        --log-private-key keys/log-private.pem \
        --log-public-key keys/log-public.pem \
        --output results/transformation.bundle.zip

      # On another host, provision trusted public keys out of band. `--log` is
      # optional: the bundle carries an offline inclusion proof.
      python3 util/transform_artifact_bundle.py verify \
        results/transformation.bundle.zip \
        --public-key trusted/artifact-public.pem \
        --log-public-key trusted/log-public.pem \
        --extract-dir imported/transformation

      # A monitor with the log can also audit every historical signed head.
      python3 util/transform_artifact_bundle.py audit-log \
        results/transformation-transparency.jsonl \
        --log-public-key trusted/log-public.pem

  Loop bundles use `manifest:loop-recurrence` and/or `manifest:loop-exit`;
  continuation uses `manifest:continuation`. The Ed25519 signature covers a
  canonical descriptor in a domain separate from signed Merkle tree heads.
  Leaves and internal nodes use the RFC 9162-style `0x00`/`0x01` SHA-256
  separation. Verification requires externally trusted artifact/log public
  keys, recomputes the inclusion root, rejects extra/duplicate ZIP members,
  verifies every content-addressed blob and the embedded F274 seal, then
  atomically imports to a fresh directory with a receipt.

  Bounds are 32 roles, 512 MiB per file, 2 GiB total, 2 MiB metadata and
  4096/64 MiB log entries/bytes. This is a self-contained copyable transport,
  not an HTTP service. Key protection, passphrases/HSM, rotation/revocation,
  timestamps and public-log operation are external. A valid historical-prefix
  rollback cannot be detected without checkpoint witnesses or gossip; use
  independently replicated signed tree heads for hostile storage.

- F290 explicit LLVM semantics and cross-major exact transformation replay:

      # Build ABI-matched plugins. The project currently declares LLVM 8--18;
      # this checked configuration exercises 18.1.3 and 17.0.6.
      PATH=/usr/lib/llvm-18/bin:$PATH cmake -S . -B build -G Ninja \
        -DSYMCC_RT_BACKEND=qsym -DZ3_TRUST_SYSTEM_VERSION=ON
      PATH=/usr/lib/llvm-18/bin:$PATH cmake --build build -j8
      PATH=/usr/lib/llvm-17/bin:$PATH cmake -S . -B build-llvm17 -G Ninja \
        -DLLVM_DIR=/usr/lib/llvm-17/lib/cmake/llvm \
        -DSYMCC_RT_BACKEND=qsym -DZ3_TRUST_SYSTEM_VERSION=ON
      PATH=/usr/lib/llvm-17/bin:$PATH cmake --build build-llvm17 -j8

      # Produce the LLVM 18 baseline manifest/IR and its F274 seal first.
      env SYMCC_HYDRA=1 SYMCC_HYDRA_MODE=safe \
        SYMCC_HYDRA_SITE=801 \
        SYMCC_HYDRA_MANIFEST_OUT=hydra.jsonl \
        /usr/lib/llvm-18/bin/opt \
        -load-pass-plugin="$PWD/build/libsymcc.so" \
        -passes=hydra-transform -S input.ll -o lowered.ll
      python3 util/seal_transform_artifact.py seal \
        --pipeline hydra --manifest hydra=hydra.jsonl \
        --input-ir "$PWD/input.ll" --lowered-ir lowered.ll \
        --compiler "$PWD/build/libsymcc.so" \
        --llvm-tool /usr/lib/llvm-18/bin/opt \
        --output transformation.seal.json

      cat > cross-llvm-candidates.json <<EOF
      {"schema":"symcc-cross-llvm-candidates-v1","candidates":[{
        "label":"llvm17",
        "opt":"/usr/lib/llvm-17/bin/opt",
        "compiler":"$PWD/build-llvm17/libsymcc.so",
        "llvm_diff":"/usr/lib/llvm-17/bin/llvm-diff"
      }]}
      EOF

      python3 util/cross_llvm_transform_replay.py audit \
        --pipeline hydra --manifest hydra=hydra.jsonl \
        --input-ir "$PWD/input.ll" --lowered-ir lowered.ll \
        --compiler "$PWD/build/libsymcc.so" \
        --llvm-tool /usr/lib/llvm-18/bin/opt \
        --seal transformation.seal.json \
        --candidates cross-llvm-candidates.json \
        --output cross-llvm-certificate.json
      python3 util/cross_llvm_transform_replay.py verify \
        --certificate cross-llvm-certificate.json

  Hydra records now state
  `llvm_ir_semantics=llvm-poison-undef-freeze-refinement-v1`, the actual LLVM
  version/major, inactive-operand/freeze/exception policies, and left/right/
  paired/extra freeze counts. The independent manifest verifier recomputes the
  counts. The cross-major audit first reruns the sealed baseline, then requires
  every candidate to pass its LLVM verifier and `llvm-diff`, preserve ordered
  proof identities and normalized manifests, and emit byte-identical textual
  IR. Only `llvm_version` and `llvm_major` are normalized away. The recorded
  major must match the actual tool; candidate binaries are hashed before and
  after replay and the baseline seal is checked again after all candidates.

  Use absolute `--input-ir` paths consistently: LLVM module identifiers and
  stable site identities can otherwise differ between the baseline and replay.
  Candidate `opt`, `llvm-diff` and pass plugin must be ABI-matched. At least
  two distinct majors are required; a same-major candidate is rejected.
  `invoke`, EH pads and other non-branch terminators are not modeled and keep
  the original CFG.

  `benchmark/evidence/hydra_f290_cross_llvm_certificate.json` is checked
  LLVM 17/18 mechanism evidence. Its canonical digest detects accidental
  modification but is not a signature; wrap it in an F289 bundle when an
  external trust root is required. Exact IR equality applies only to the
  sealed input/pass/configuration and is not a universal semantic-equivalence
  proof or a public-target performance result.

- F291 symbolic-index fixed heap-region continuation writers:

      # No new switch is required. F291 is a fail-closed extension of the
      # existing compile-time continuation-memory gate.
      export SYMCC_IFSS_CONTINUATION_STATE=1
      export SYMCC_IFSS_CONTINUATION_MEMORY=1
      export SYMCC_IFSS_CONTINUATION_MANIFEST_OUT=continuations.jsonl

      opt -load-pass-plugin="$PWD/build/libsymcc.so" \
        -passes=ifss-continuation-lowering,ifss-continuation-memory \
        -S input.ll -o lowered.ll
      python3 util/verify_ifss_continuation_manifest.py continuations.jsonl

  F291 emits
  `symbolic-region-writer-graph-continuation-memory-tuple-v16` and analysis
  `llvm-memoryssa-aa-symbolic-region-writer-graph-revalidated-v16`. It is
  selected when a writer layer uses a symbolic byte index, or when the ordered
  graph exceeds the v15 limit of four total layers/two pointer partitions/two
  guards. V16 permits at most eight total layers. Existing shapes inside the
  v15 budget retain v15; this is a schema extension, not a global migration.

  A symbolic region layer records:

      kind=symbolic-region-write
      store_site, store_width
      region_base_site, region_extent
      index_site, index_bits, base_offset
      lane_cases[].ordinal
      lane_cases[].cases[].{ordinal,index_value,source_byte}

  `region_extent`, sites and fingerprints are canonical unsigned decimal text;
  `base_offset` and `index_value` are signed JSON integers. The verifier checks
  their signed bit-width bounds and mixes negative values as uint64 two's
  complement, matching LLVM metadata. Do not normalize them to unsigned text.

  Accepted allocations are external declarations of standard address-space-0
  `malloc`/`calloc` with constant nonzero extent no larger than 2^32. The load
  must be a fixed 2--8-byte integer window inside that region. The dynamic
  writer is a simple 1--8-byte integer store through an `inbounds gep i8` with
  one instruction-valued index whose width equals the DataLayout pointer-index
  width and is at most 64. Unknown/dynamic extent, argument base, user-defined
  allocator, symbolic base, non-byte or strided GEP, pointer PHI, realloc,
  volatile/atomic memory, unknown ModRef and cyclic MemoryPhi keep the original
  load.

  The checked LLVM 17/18 continuation certificate is
  `benchmark/evidence/ifss_f291_cross_llvm_certificate.json`. Verify it with:

      python3 util/cross_llvm_transform_replay.py verify \
        --certificate \
        benchmark/evidence/ifss_f291_cross_llvm_certificate.json

  The certificate applies to the sealed F291 fixture only. It does not prove
  arbitrary heap semantics or public-target performance.

  The post-F291 full gates pass 195/195 LLVM 18 lit tests, 194 LLVM 17 lit
  tests with one unsupported cross-major driver, and 471/471 Python tests.

- F292 symbolic-region cyclic byte fixed point:

      # F292 uses the existing continuation-memory switches.
      export SYMCC_IFSS_CONTINUATION_STATE=1
      export SYMCC_IFSS_CONTINUATION_MEMORY=1
      export SYMCC_IFSS_CONTINUATION_MANIFEST_OUT=continuations.jsonl

  F292 emits
  `symbolic-region-cyclic-byte-lane-continuation-memory-tuple-v17` and
  `llvm-memoryssa-aa-symbolic-region-cyclic-byte-lane-revalidated-v17`.
  It scalarizes only the fixed 2--8-byte window read after a loop. Each
  backedge lane carries the previous integer PHI byte and replaces it when
  the current pointer-width index equals one of at most eight overlap cases.
  The generated state is bounded by load width times store width, not by the
  concrete trip count.

  Accepted cycles have one entry, one unconditional backedge and exactly one
  simple 1--8-byte symbolic-index writer. The region must meet the F291 fixed
  `malloc/calloc` rules. Allocator declarations must additionally be
  non-variadic, have the standard argument count, and use the DataLayout
  pointer-index integer width for every size argument. Entry bytes must have
  an existing exact linear proof. Argument/symbolic bases, dynamic extents,
  wrong allocator prototypes, fixed-plus-dynamic or multiple dynamic writers,
  conditional/multi-latch transfers under the v17 proof, pointer PHIs,
  volatile/atomic accesses and unknown ModRef retain the original load.
  F294 below adds a separate v18 proof for a bounded conditional/multi-latch
  subset; it does not relax the v17 artifact contract.

  The manifest places the F291 region record under
  `backedge_state.symbolic_region_writer`; the ordinary backedge lanes must
  all be canonical `carry` lanes. Signed `index_value` and `base_offset`
  retain their v16 encoding. Verify the checked LLVM 17/18 certificate with:

      python3 util/cross_llvm_transform_replay.py verify \
        --certificate \
        benchmark/evidence/ifss_f292_cross_llvm_certificate.json

  The certificate binds proof identity `11600885392756402730`, lowered IR
  SHA-256 `6e5e4c5c8fbc76d79a603a874dd78161803f5b54aeedf9c30ee05365efe91189`,
  and normalized-manifest SHA-256
  `2eb7bf054afdbc666c0fa9929c1c429bb80dce6dcb63fbf1dc6b29353c1c1901`.
  It is fixture-specific structural evidence, not general array semantics or
  a public-target performance result.

  The post-F292 full gates pass 198/198 LLVM 18 lit tests, 197 LLVM 17 lit
  tests with one unsupported cross-major driver, and 471/471 Python tests.

- F294 conditional multi-latch symbolic-region transfer:

      # F294 uses the same opt-in continuation-memory switches.
      export SYMCC_IFSS_CONTINUATION_STATE=1
      export SYMCC_IFSS_CONTINUATION_MEMORY=1
      export SYMCC_IFSS_CONTINUATION_MANIFEST_OUT=continuations.jsonl

  F294 emits
  `symbolic-region-multi-latch-cyclic-byte-lane-continuation-memory-tuple-v18`
  and
  `llvm-memoryssa-aa-symbolic-region-multi-latch-cyclic-byte-lane-revalidated-v18`.
  It accepts 2--4 mutually exclusive MemoryPhi latch transfers. Each latch may
  contain at most one F291-compatible fixed-region symbolic-index writer,
  either unconditional or protected by one branch guard. Different latches
  are alternative incoming states; their writers are never composed in latch
  ordinal order.

  For each address-order lane, the inner equality/select chain applies the
  current latch's symbolic writer when its pointer-width index matches a
  canonical signed overlap case. A conditional transfer then wraps that
  region result in an outer guard/select and carries the previous PHI byte
  when the store arm was not taken. The ordinary per-transfer lane state is
  therefore canonical all-carry whenever `symbolic_region_writer` is present.

  The manifest records a writer-presence bit and the complete allocator,
  extent, store/index, signed offset/case, guard-site and polarity proof for
  every transfer. Compiler replay re-runs MemorySSA/AA and peels the actual
  PHI, outer guard and inner equality/select expressions. The independent
  verifier checks 2--4 latches, all-carry symbolic bases, field exclusivity,
  signed canonical order and the same presence-aware fingerprint.

  Same-latch multiple dynamic writers, nested predicate guards, five or more
  latches, dynamic extent, symbolic allocator base, pointer PHI, typed/strided
  multi-dimensional GEP, unknown ModRef, volatile/atomic accesses and general
  array/heap state retain the original load. Existing v17 and constant-offset
  multi-latch shapes keep their old schema.

  Verify the checked LLVM 17/18 certificate with:

      python3 util/cross_llvm_transform_replay.py verify \
        --certificate \
        benchmark/evidence/ifss_f294_cross_llvm_certificate.json

  The certificate binds proof identity `2389278380394154034`, lowered IR
  SHA-256 `c2802fe2c1015fc0117954e0f74c3edcf19d6cac2d67cabd400825ebe87f3769`,
  and normalized-manifest SHA-256
  `296583a8c561d62aa2abaecca7e844a7c5edb1aa4c5dcecca7ef51638e0ca409`.
  It is fixture-specific exact structural evidence, not a public-target
  profitability result or a proof of arbitrary array semantics.

  The post-F294 full gates pass 202/202 LLVM 18 lit tests at `-j16`,
  201 LLVM 17 lit tests at `-j16` with one unsupported cross-major driver,
  and 471/471 Python tests. The measured wall times were 134.31, 134.07,
  and 79.584 seconds respectively.

- F296 same-latch ordered symbolic-region multiwriter:

      # F296 uses the existing opt-in continuation-memory switches.
      export SYMCC_IFSS_CONTINUATION_STATE=1
      export SYMCC_IFSS_CONTINUATION_MEMORY=1
      export SYMCC_IFSS_CONTINUATION_MANIFEST_OUT=continuations.jsonl

  No new runtime switch is required. When a single unconditional latch has a
  MemorySSA chain of two through four relevant F291-compatible writers to one
  fixed heap allocation/window, the pass emits
  `ordered-symbolic-region-cyclic-byte-lane-continuation-memory-tuple-v19` and
  analysis
  `llvm-memoryssa-aa-ordered-symbolic-region-cyclic-byte-lane-revalidated-v19`.
  One writer retains v17; multiple mutually exclusive latches retain v18.

  `symbolic_region_writers` is ordered newest first. Ordinal zero is the latest
  MemorySSA definition and therefore has the highest last-writer priority.
  Lowering starts from the carry byte, wraps older writers first, and places
  newer writers outside them. Compiler replay must peel the actual equality/
  select chain in newest-first order and end at the matching cycle-PHI byte.
  The independent verifier requires 2--4 canonical ordinals, distinct store
  sites, one allocation identity/extent, all-carry base lanes, signed canonical
  cases, and v17/v19 field exclusion.

  A fifth relevant writer, unknown ModRef between writers, conditional writer
  tree, static/dynamic relevant-write mixture, dynamic extent, symbolic base,
  pointer PHI, volatile/atomic access, typed/strided multidimensional GEP, or
  general heap/array state retains the original continuation load.

  Verify the checked LLVM 17/18 certificate with:

      python3 util/cross_llvm_transform_replay.py verify \
        --certificate \
        benchmark/evidence/ifss_f296_cross_llvm_certificate.json

  The certificate binds proof identity `3118488025292340061`, lowered IR
  SHA-256 `cd776afe464d40533caae83d942d1eded06b5174652585128feae7ad313e03c5`,
  and normalized-manifest SHA-256
  `d83e318f2ec82a93aab8894eab29c278b5a91a9254a1470cb35221c4f7fabe55`.
  This is exact fixture evidence, not a public-target performance result.

  The post-F296 full gates pass 206/206 LLVM 18 lit tests in 135.31 seconds,
  205 LLVM 17 lit tests with one expected unsupported cross-major driver in
  139.22 seconds, and 471/471 Python tests in 80.736 seconds. The suites were
  run sequentially.

- F293 shared-predicate DAG guard hash-consing:

      # F293 uses the existing opt-in Hydra controls.
      export SYMCC_HYDRA=1
      export SYMCC_HYDRA_MODE=safe
      export SYMCC_HYDRA_MANIFEST_OUT=hydra.jsonl

  Hydra still tries the v3 tree and v4 DAG proof before v5. Therefore an
  existing region inside the v4 10-block/4-branch/8-leaf/3-local-merge/
  8-local-PHI/64-instruction domain keeps
  `bounded-acyclic-sese-dag-hydra-v4` and its original lowering. V5 emits
  `bounded-shared-predicate-sese-dag-hydra-v5` only after v4 fails and accepts
  at most 14 blocks, 5 internal branches, 10 external-merge leaf edges,
  4 local merges, 12 local PHIs, and 96 flattened instructions per arm.

  V5 retains the F287 single-entry, nearest-common-post-dominator, arm
  disjointness, predecessor-closure and acyclic topological requirements.
  Every CFG edge guard is interned by `(predecessor ordinal, successor index)`
  inside its arm. Predicate negations are interned across both arms by the
  lowered predicate identity. The manifest reports
  `guard_reuse_policy=per-arm-edge-and-global-negation-hash-cons-v1`,
  `canonical_guard_edges`, ordered left/right predicate sites, unique/reused
  predicate counts, and observed edge/negation reuse. These values are
  verified and included in `structure_fingerprint`.

  Cycles, a fifth local merge, more than 14 blocks, external arm predecessors,
  overlapping arms, switch/invoke/EH, address-taken blocks, escaping SSA,
  unsupported instructions and unsafe effects retain the original CFG. The
  hash-consing scope is one selected Hydra region; it is not cross-function or
  cross-module common-subexpression elimination.

  Verify the checked LLVM 17/18 certificate with:

      python3 util/cross_llvm_transform_replay.py verify \
        --certificate \
        benchmark/evidence/hydra_f293_cross_llvm_certificate.json

  The certificate binds proof identity `3502535688576112958`, lowered IR
  SHA-256 `cd12b34975f22a06c2c8de323509511dc576b94693ed38f1f767df7dc0e6d700`,
  and normalized-manifest SHA-256
  `409fe0b27aaf5699d4f86f3e30f14322fad721e730f6dcbd5e13754ed17f3e9f`.
  It is fixture-specific structural evidence, not arbitrary-CFG semantics or
  a public-target performance claim.

  The post-F293 full gates pass 199/199 LLVM 18 lit tests at `-j16`,
  198 LLVM 17 lit tests at `-j16` with one unsupported cross-major driver,
  and 471/471 Python tests. Run the three suites sequentially: launching both
  default 192-worker lit suites together can exhaust resources needed by the
  exact-polyhedral and persistent-helper stress tests.

- SYMCC_HYDRA_SITES=<site0,site1[,site2,site3]> (compile time, default
  unset): Enable the F295 bounded cross-region Hydra transaction. This option
  is mutually exclusive in intent with the legacy single-site selector
  `SYMCC_HYDRA_SITE`; when present, the ordered multi-site list is authoritative.
  It requires `SYMCC_HYDRA=1`, two through four distinct nonzero decimal site
  IDs, and the existing safe/aggressive mode:

      export SYMCC_HYDRA=1
      export SYMCC_HYDRA_MODE=safe
      export SYMCC_HYDRA_SITES=7001,7002
      export SYMCC_HYDRA_MANIFEST_OUT=hydra-transaction.jsonl

  Every selected candidate must already satisfy the F293 v5 shared-predicate
  DAG proof. All sites must be in one function, their owned arm blocks must be
  pairwise disjoint, the listed entry blocks must form a strict dominance
  chain, and their internal conditional predicates must have a nonempty common
  original-SSA identity set. The compiler validates the complete batch before
  editing IR. Reverse order, duplicates, missing sites, cross-function sites,
  overlapping ownership, or no common predicate fail closed.

  A function-scoped cache stores `{predicate Value*, negation instruction,
  producer site}`. A cached negation is reused in a later region only when a
  freshly built LLVM DominatorTree proves that instruction dominates the later
  outer branch. The per-arm edge cache remains region-local. F295 therefore
  does not perform textual expression matching, arbitrary ALU/ITE CSE, or
  cross-function/module reuse.

  Multi-site records emit
  `bounded-cross-region-shared-predicate-sese-dag-hydra-v6`,
  `compatible-lcs-cross-region-shared-dag-topological-left-tie-v6`, and
  `per-arm-edge-and-function-dominating-negation-hash-cons-v2`. Every JSONL
  record binds the same ordered site/common-predicate transaction fingerprint,
  its ordinal, actual cross-region reuse count, and preceding producer sites.
  Verify the whole JSONL transaction and its checked LLVM 17/18 certificate:

      python3 util/verify_hydra_transform_manifest.py \
        hydra-transaction.jsonl
      python3 util/cross_llvm_transform_replay.py verify \
        --certificate \
        benchmark/evidence/hydra_f295_cross_llvm_certificate.json

  The checked certificate binds two structure identities
  `8175852705754774924` and `1889164356607597381`, lowered IR SHA-256
  `a0df2ebd9b22a950a6301330cdbdc421fbc6bf35cc3b4eab0a458c2cf957a937`,
  and normalized-manifest SHA-256
  `31a953eeb4e74106e7bbadb2e66af29fa725db8e8745cc4c43827cbf5942d4c8`.

  Unified `seal_transform_artifact.py` and
  `replay_transform_artifact.py` accept one legacy Hydra record or one complete
  v6 transaction and replay the exact ordered site list. The higher-level
  `util/hydra_transform.py` failure/coverage campaign remains intentionally
  single-site; public multi-site profitability evidence is not yet claimed.

  The post-F295 full gates pass 203/203 LLVM 18 lit tests in 134.10 seconds,
  202 LLVM 17 lit tests with one expected unsupported cross-major driver in
  133.26 seconds, and 471/471 Python tests in 79.599 seconds. The suites were
  run sequentially.

See sota_hybrid_execution_2026.md for the feedback model and evaluation plan.

(Most people should stop reading here.)


                                Advanced options


There is actually a third category of options: when compiling with SymCC, you
can specify the location of its various components via environment variables.
This is not necessary in most cases because the build system makes sure that all
components know about each other; however, in some advanced setups you may need
to move files around after building them, and in that case, you can use the
variables documented below to communicate the new locations:

- SYMCC_RUNTIME_DIR and SYMCC_RUNTIME32_DIR: The directory that contains the
  run-time support library (i.e., libSymRuntime.so).

- SYMCC_PASS_DIR: The directory containing the compiler pass (i.e.,
  libSymbolize.so).

- SYMCC_CLANG and SYMCC_CLANGPP: The clang and clang++ binaries to use during
  compilation. Be very careful with this one: if the version of the compiler you
  specify here doesn't match the one you built SymCC against, you'll most likely
  get linker errors.