Observed-run dossiers and example index

Run a new CM1-in-3 input through the four engines and keep the checked results, figures, and PDF in one dossier. From the repository root, after installing the system prerequisites:

make demo-setup
make demo-check
make demo INPUT='path/to/new formula.cm13' TIMEOUT=300

Setup downloads the locked dependencies and checks the compiler, renderer, and PDF tools. The short suite checks known cases. The demo then accepts your own input without an expected result and prints the PDF path after the complete dossier succeeds. Both commands run offline after setup; each invocation keeps its own diagnostics.

For SAT, the dossier includes checked witnesses. For UNSAT, it records engine agreement without an independent UNSAT certificate. Timeout, UNKNOWN, errors, and incomplete traces are failures, never substitutes for UNSAT.

Continue with the input format and output files, the six narrated checks, or the named v2 cases. The older single-solver diagnostic cases remain available below.

Suite breve commentata

Dopo make demo-setup, eseguire offline:

make demo-check

La suite annuncia in italiano sei controlli, spiegando cosa verificano:

1. Input valido: il parser C legge le tre variabili e le tre clausole del caso tests/instances/pipeline_sat.cm13.
2. Input fuori dominio: il parser rifiuta una variabile non dichiarata; un errore I/O non conta come il rifiuto atteso.
3. SAT noto: il solver reference produce un tiling verificato e un assegnamento booleano estratto, controllati anche dai checker indipendenti.
4. UNSAT noto: tests/instances/pipeline_unsat_search.cm13 contiene la clausola (x4,x4,x4), che richiede 3*x4=1; il risultato non ha witness.
5. Accordo: optimized, Boolean Z3 e Wang Z3 confermano entrambi gli esiti noti; ogni motore gira una volta per caso e ogni witness SAT viene verificato. I risultati reference dei punti precedenti vengono riusati.
6. Witness alterato: una sola tessera viene sostituita con un’altra del tileset, incompatibile con un colore di bordo. Il checker Python deve rifiutare la copia e accettare ancora l’originale. Le coordinate stampate partono da zero.

Questi sono casi fissi con esito noto; make demo INPUT=..., descritto sotto, accetta invece un input nuovo senza presumere SAT o UNSAT. La suite breve non genera PDF, figure o trace e non sostituisce l’intera suite di test del progetto. Richiede solo l’ambiente Python principale e la libreria nativa già installati; non avvia build, installazioni o download.

Ogni invocazione conserva worker.log in una directory distinta build/demo-check/run-*, stampata come diagnostics=.... Si ferma al primo fallimento. Solo dopo tutti i controlli compare Superati 6/6 controlli, con la durata effettiva: l’obiettivo indicativo di 30–60 secondi dopo il setup non è una soglia CI e non introduce attese artificiali. La durata del dossier si misura separatamente.

Per impostazione predefinita non c’è un limite di tempo (TIMEOUT=none); si può imporlo con make demo-check TIMEOUT=60. Ctrl+C interrompe anche un’esecuzione senza limite. Per scegliere una directory di diagnostica nuova:

python3 tools/demo_check.py --output build/my-check --timeout 60

Directory, file o link già presenti non vengono sovrascritti. Timeout, interruzione, UNKNOWN, discordanza, errori e output incompleti sono fallimenti, mai risultati UNSAT. La CLI restituisce 124 per timeout, 130/143 per SIGINT/SIGTERM, 1 per errori e 2 per argomenti invalidi; GNU Make restituisce il proprio esito nonzero quando la ricetta fallisce. Timeout e interruzioni fermano anche i processi figli. Il log resta disponibile; se un terminale lento perde messaggi, contiene comunque l’output completo del worker.

Full-pipeline v2 capture

New CM1-in-3 input

Run make demo-setup once, then use the installed environments offline:

make demo INPUT='path/to/new formula.cm13' TIMEOUT=300

The input needs a p cm13 n n header, followed by n clauses. Each clause has three positive variable indices in 1..n and ends in 0. Every variable must occur exactly three times across all clauses, counting repeated occurrences within one clause. Lines beginning with c are comments. For example:

c Three variables, each with three occurrences
p cm13 3 3
1 1 2 0
1 2 3 0
2 3 3 0

No expected result is supplied. The demo copies the original bytes before parsing, reduces once, and runs reference, optimized, Boolean Z3 and Wang Z3 once each. The dossier and PDF consume that same validated capture. Named cases below use the same capture producer and retain their configured metadata.

Each invocation creates a separate build/demo/run-* directory containing input.cm13, diagnostic input.json (original path/name and SHA-256), worker.log, and the completed dossier/ with run.json, source/trace assets, figures, report.tex and report.pdf. Input names with spaces or shell/Make metacharacters are passed literally; quote the command argument as above. The portable name inside a new dossier is always input.cm13.

The command prints real operations as they start. worker.log keeps the full worker output even if a slow terminal or pipe cannot display every message. TIMEOUT defaults to none (no time limit). An explicit numeric limit must be finite and positive, in seconds. It covers the worker’s preflight, input copy, native/Z3 capture, checks, figures and LaTeX. Timeout or Ctrl-C stops the worker and its child processes; SIGTERM is also handled. The log and copied input survive failures, while any staging artifacts remain diagnostic only. The command prints dossier= and pdf= only after successful completion.

For explicit output and trace capacity, use the same supervised Python entry:

python3 tools/demo.py 'path/to/new formula.cm13' \
  --output build/my-demo --timeout 300 --event-capacity 100000

The output directory must be new, including when a symlink already occupies that path. Trace capacity is an integer from 2 to 100000 per native solver; the default is 100000 and checkpoints are disabled. Exhaustion fails without rerunning either solver. Missing dependencies require make demo-setup; the demo never builds, installs or downloads them itself.

Malformed input, missing dependencies, UNKNOWN, engine disagreement, incomplete trace and failed checks produce distinct diagnostic messages. Timeout exits with 124; handled SIGINT/SIGTERM exits with 130/143. These are process outcomes, not UNSAT results. GNU Make reports a failed recipe with its own nonzero exit. UNSAT succeeds only when all four engines agree on that terminal result, and still carries no independent UNSAT certificate. Arbitrary inputs may exceed the time or trace limits; neither option promises completion.

Wide regions appear as overview figures in the PDF. Use the PDF viewer’s zoom or the full-resolution PNG frames under dossier/assets/narrative/ to inspect individual cells and trace labels; a whole-page view cannot show every detail.

Named cases

wang-run-case-v2 deliberately has no initial-domain override field. Its canonical case follows tests/instances/pipeline_sat.cm13 through the four named engines and one shared native reduction:

make shared
uv run --frozen python tools/generate_run_dossier.py \
  examples/run-cases-v2/pipeline-sat.json \
  build/run-dossiers/pipeline-sat-v2

The v2 implementation parses and reduces once, then runs the traced reference and optimized solvers exactly once while the same native formula and reduction are alive. It invokes the existing Boolean Z3 and Wang Z3 summary producers once each. SAT assignments and tilings are checked with the existing pure Python checkers; native tilings also retain the assignment extracted by the existing Yang–Zhang witness bridge.

The v2 directory contains run.json, the copied CM1-in-3 input, two existing trace-v3 manifests, their content-addressed snapshots, and the two existing Z3 summary documents. Both native manifests bind the same formula, tileset, region, and construction-provenance hashes. Agreement means equal SAT/UNSAT status plus independently valid SAT witnesses; different valid witnesses are not required to be byte-equal. UNKNOWN, mismatch, a truncated trace, or a failed checker aborts the capture before installation.

Result expectation and recorded outcome

The v2 case and run contracts keep expected_status required and accept "sat", "unsat", or null. A null value means no expected result was supplied; it is never filled from a solver result and does not mean UNKNOWN. All four named engines must first report the same terminal result. A supplied expectation is then checked as an additional assertion. Witness checks, presentation applicability, and PDF status follow the observed agreement. For an absent expectation the PDF says so explicitly.

The standalone narrative manifest adds case.observed_status exactly when case.expected_status is null. Known cases retain the existing three-field case shape. Verification receipts preserve the nullable expectation and use their four recorded agreement statuses; they need no extra status field. Bundle loading also binds each native source identity and trace status/completeness, and each Z3 summary status, to its run record.

Updated readers continue to accept earlier v2 dossiers, and known-case output and canonical asset identities stay unchanged. Earlier strict readers reject the new nullable variant. V1 retains its existing contracts. This is an extension of the existing v2 and narrative contracts, with no new pipeline or independent UNSAT certificate.

The downstream shared-asset pass then consumes only that validated capture. Its closed wang-narrative-assets-v1 manifest names fixed component assets, not generic stages: Boolean and Wang Z3 encoding order, canonical region construction, observed reference and optimized traces, the six checker records, the checked square/generalized/hex witness sequence, the six retained optimized mechanisms, and the complete pipeline overview. Every GIF record contains one reduced-motion PNG, contact sheet, caption, alt text, semantic label, source identity, completeness/selection scope, and all static frame hashes.

Trace frames use semantic-milestones-v1, which selects event and phase transitions before deterministic gap filling; it is distinct from uniform sampling and reuses the same single replay as PNG, contact-sheet, and GIF encoding. For SAT, run.json binds the three reserved static presentation artifacts and their hashes. For UNSAT they remain null, while the asset bundle records an explicit not-applicable panel and never fabricates a witness or certificate. The separate example is versioned at examples/run-cases-v2/pipeline-unsat-search.json.

The default v2 command stops after the validated capture and shared assets. It does not import the LaTeX formatter, invoke a TeX compiler, or produce report.tex and report.pdf. With pdfLaTeX available, add --pdf when a static report is wanted:

make shared
uv run --frozen python tools/generate_run_dossier.py \
  examples/run-cases-v2/pipeline-sat.json \
  build/run-dossiers/pipeline-sat-v2-pdf \
  --pdf

The v2 formatter consumes only the validated run.json and static PNGs already named by the asset manifest. It does not solve, invoke Z3, verify, replay, or render again. SAT reports include the checked witness presentations; search-UNSAT reports mark witness-only sections not applicable and do not invent a certificate.

The opt-in compiler uses the same isolated, no-shell-escape execution and private TeX state as v1. TeX and PDF files are staged with the complete dossier and installed atomically; compilation failure leaves no partial destination. The v1 command, formatter, output shape, and --tex-engine behavior remain unchanged.

All v2 durations use one monotonic nanosecond clock and are labelled run-specific-observation-not-a-benchmark. They are raw facts about that capture, never a performance comparison. SAT-only checker timings are null for UNSAT rather than fabricated as zero.

Example index

The v1 reports describe one configured native run. Each completed directory contains run.json, report.tex, report.pdf, and assets/. The four cases below retain their existing schemas, initial-domain behavior, and output shape.

run.json records the source and Git identity, environment, solver options and result, complete trace counters, initial-domain overrides, raw stage durations, replay scope, and SHA-256 for each referenced JSON or raster asset. The PDF uses that recorded data; it does not recalculate events, witness state, timing, or provenance.

Four strict case documents are versioned. Their classification is checked against the observed trace rather than trusted as prose.

The first three cases use the same small formula so the observed boundary is easy to compare. The two constrained UNSAT cases deliberately exercise the public initial-domain option: their UNSAT status describes that configured Wang solve, not the unconstrained source formula. The search case uses a separate cubic monotone input whose unconstrained optimized run reaches depth two before exhausting all branches.

The solver trace contract remains the canonical explanation of event semantics, truncation, and replay. The reference solver component owns the public reference animation. The static snapshot contract defines formula and region views, while the square-to-hex reference defines the presentation-only port.

Reproduce one dossier

Build the shared native library, provide pdfLaTeX, and run the sole generator:

make shared
uv run --frozen python tools/generate_run_dossier.py \
  examples/run-cases/sat-end-to-end.json \
  build/run-dossiers/sat-end-to-end \
  --tex-engine pdflatex

The destination must not exist. Every intermediate is written below a sibling staging directory, the trace bundle is validated before rendering, and the completed directory is installed with one rename. A failed render or TeX compile leaves no partial destination.

The generator calls the isolated renderer through its locked environment. A single replay composes the selected frames used for individual PNGs, the contact sheet, and the optional GIF. The PDF embeds the already-produced contact sheet and static square/hex PNGs; it never embeds viewer-dependent GIF or video content. UNSAT reports contain region views rather than inventing a solution.

pdfLaTeX is invoked directly, never through a shell, with -no-shell-escape, restricted input/output policy, a private TeX home, UTC, and SOURCE_DATE_EPOCH derived from the recorded run time. The CI smoke installs TeX only inside its disposable runner. TeX is not a runtime or root Python dependency.

Timing and evidence boundary

The monotonic durations for parse, region build, solve, export, render, and SAT witness verification are raw evidence from one environment. They are excluded from snapshot identity and are not performance gates. The native solver has no Z3-style encoding stage, so encoding is explicitly recorded as not applicable rather than reported as a fabricated zero-duration operation. Verification is also explicitly not applicable to UNSAT runs because the trace is diagnostic, not an independently checked certificate.

Every example requires a complete trace. Selected frames remain a presentation subset of that trace. For UNSAT, unsat_certificate is always false: conflicts and trail history diagnose what the run observed but do not constitute a standalone mathematical proof of unsatisfiability.