CQ-SAT/GCC v0.28.0

CQ-SAT/GCC v0.28.0 adds a bounded experimental dense predicate quotient for state-dependent firmware and robotics models with 9–16 relevant inputs and 1–4 latches.

Highlights:

• exact BDD predicate compilation without enumerating all input patterns
• powered temporal relation composition and concrete trace reconstruction
• dual-direction agreement with persistent CDCL and maintained Yosys
• three separately authored interrupt, actuator, and sensor-fusion controllers
• reproducible 120-row evidence matrix and timing-free static admission boundary
• fail-closed support, latch, horizon, BDD-node, and cache limits

Admitted controlled rows show median end-to-end ratios of 1.21x–2.35x against persistent CDCL. Negative short-horizon rows are retained and rejected by the static gate.

Claim boundary: this is an experimental research backend, not default portfolio integration, a general SAT/model-checking speedup, a production-grade claim, or evidence of scholarly novelty.

v0.27.0 — Exact Symbolic Input Projection

CQ-SAT/GCC v0.27.0 adds the first exact symbolic-input projection stage for CIQ.

The compiler now propagates input-support masks through AIG transition and property cones, allowing firmware and robotics models to declare up to 64 inputs when no more than eight affect the combined interface. Proven-irrelevant causal observations are removed without training or timing calibration. Recovered projected traces are lifted into complete input vectors and checked by re-evaluating the original AIG.

On a 16-input mobile-robot obstacle-stop regression projected exactly to two inputs, ten trials per horizon produced median end-to-end speedups of 2.46x, 4.00x, 6.76x, and 10.74x at horizons 8, 16, 32, and 64. All 1,240 target rows were independently replayed with fresh CDCL and every full-input witness validated.

The boundary remains explicit: this result applies to wide declared buses with narrow semantic support. Genuinely dense wide-input predicate projection remains open.

Full details: https://github.com/kabudu/continuation-quotient-sat/blob/v0.27.0/docs/SYMBOLIC_INPUT_PROJECTION.md

v0.26.0 — Counterfactual Interface Quotient

CQ-SAT/GCC v0.26.0 introduces the Counterfactual Interface Quotient (CIQ), an exact bounded experiment for small firmware controllers with repeated input phases.

CIQ preserves constant phases as cached powered state relations instead of expanding every frame, suppresses semantically irrelevant repairs, and reconstructs concrete avoiding traces on demand. An independent verifier re-enumerates causal queries with fresh CDCL, validates witnesses, checks source identity and coverage, and rejects altered or incomplete reports.

On the bounded infusion-pump door-interlock regression, ten trials per horizon produced median end-to-end speedups of 1.42x, 2.38x, 4.15x, and 7.00x at horizons 8, 16, 32, and 64. Every query agreed with CDCL and every recovered witness validated.

This is a robust result for one narrow product-shaped controller class. It is not a claim of general superiority, production readiness, or established scholarly novelty.

Full details: https://github.com/kabudu/continuation-quotient-sat/blob/v0.26.0/docs/COUNTERFACTUAL_INTERFACE_QUOTIENT.md

CQ-SAT/GCC v0.25.0

CQ-SAT/GCC v0.25.0 broadens the evaluation surface and tests whether causal explanation can finally amortise continuation-quotient preparation.

The release adds strict original-format binary AIGER support across every AIGER command. Checked little-endian base-128 delta decoding reconstructs implicit inputs, latches, and AND gates, then passes the result through the same topology and semantic validation used for ASCII. Malformed, truncated, overflowing, extended, or oversized inputs fail closed. The binary fixture is semantically compared with ASCII and independently accepted by Yosys on Linux and macOS.

The new compile-once causal batch builds one maximum-horizon transition CNF and at most one continuation quotient, then explains every reachable frame/output failure. It tests maximal segments, individual points, and dyadic constant intervals; uses an exact bounded subset map to enumerate distinct 1-minimal causes; replays the identical transcript through persistent CDCL and CQ; reports workload-wide measured/projected break-even; and ships an independent verifier that rejects missing, duplicate, altered, non-sufficient, or non-minimal rows.

The first infusion-pump run is deliberately reported as a negative performance result: eight reachable targets produced 24 complete rows, 35 minimal causes, and 619 discovery queries. All causes verified, but CQ showed neither a measured nor projected crossover after 100 transcript repetitions. Persistent CDCL remains the practical default for this workload.

Validation includes 79 Rust tests, clean RustSec audit and package verification, Yosys interoperability, Rust 1.97 Bookworm tests, the public RTL differential corpus, and all required GitHub checks.

CQ-SAT/GCC remains an evaluation-ready research prototype—not a production-grade product and not evidence of a novel causal algorithm. Independent scholarly review and representative design-partner evidence remain open gates.

CQ-SAT/GCC v0.24.0

CQ-SAT/GCC v0.24.0 adds an exact closest-method experiment for causal counterexample analysis.

The release compares ordered deletion and QuickXplain over the same temporal waveform-intervention vocabulary. Every fresh-CDCL discovery and validation query is recorded and replayed through persistent CDCL and, when statically admitted, a continuation quotient. Publication fails on disagreement, overwrite, or invalid minimality evidence.

The result is deliberately mixed:

• QuickXplain reduces discovery queries on the sparse 2-of-16 control.
• Deletion wins on the dense control, infusion-pump example, and SPI fixture.
• Persistent CDCL beats rebuilding a fresh solver on all eight rows.
• CQ accelerates query replay when admitted but does not amortise preparation on this cohort.

This negative result is part of the release: v0.24.0 does not claim a new minimisation algorithm or a production performance advantage. Deletion, QuickXplain, incremental SAT, causal counterexample explanation, and compiled Boolean explanations are established work. The maximal-constant waveform vocabulary, identical cross-backend transcript replay, and digest-bound evidence integration remain potentially distinctive but scholarly novelty is unproven.

Validation includes exhaustive monotone-oracle checks through four choices, deterministic regeneration of eight result rows, Rust 1.97 Linux and macOS tests, public RTL differential checks, production-evaluation smoke tests, and a clean RustSec audit.

CQ-SAT/GCC remains an evaluation-ready research prototype. Independent security review, technical review, and design-partner RTL evidence are still required before any production-grade claim.

CQ-SAT/GCC v0.23.0

Certified causal counterexample analysis

CQ-SAT/GCC v0.23.0 adds a bounded, evidence-producing way to explain input-driven AIGER failures.

• segments the earliest counterexample into maximal constant primary-input waveform events
• computes a replay-checked 1-minimal set that forces the named bad output at the original counterexample frame
• compares the same intervention sequence across fresh CDCL, persistent CDCL, and continuation quotients when statically admitted
• aborts publication on any solver disagreement and uses exact CDCL when CQ is rejected
• publishes a durable, atomic, no-clobber v1 evidence directory with SHA-256-bound certificate, metrics, and manifest
• provides a strict verifier that rederives the earliest counterexample and re-solves sufficiency and every single-event minimality obligation
• includes checked-in verified SPI and infusion-pump evidence bundles, adversarial tests, CI coverage, schema documentation, and a self-contained runner

On the infusion-pump example, four candidate segments reduce to a verified two-segment cause. CQ is 1.30x faster per intervention query in the recorded run, but only 0.031x after compilation; this release therefore does not claim an amortised speed improvement. The SPI example exercises the exact CDCL fallback.

This release combines established counterexample-minimisation, minimal-UNSAT, incremental-SAT, and causal-explanation ideas with continuation-quotient reuse and a strict evidence contract. It is a potentially novel synthesis, not a claim of proven scholarly novelty, a general SAT breakthrough, physical-world causation, or production certification. CQ-SAT/GCC remains an evaluation-ready research prototype pending external design-partner and security assessment.

Validation: 72 Rust tests passed on macOS and Rust 1.97 Linux/arm64; GitHub test, public RTL corpus, and dependency-audit jobs passed; RustSec reported no vulnerable dependencies; both checked-in bundles replay-verified.

CQ-SAT/GCC v0.22.0

First-person, self-service external evaluations

CQ-SAT/GCC v0.22.0 corrects the external engagement model for an individual maintainer.

• all sendable partner and assessor communication now uses “I”, not “we”
• partners and independent reviewers operate the evaluation themselves using repository resources
• the maintainer does not participate in setup or execution and does not access RTL, properties, traces, workers, credentials, private registers, meetings, or intermediate findings
• the repository makes no engineering-support, consultancy, legal, certification, or partner-specific operational commitment
• private data agreements, execution, oracle comparison, review, and production-gate checking remain entirely within the partner/assessor boundary
• a new non-confidential outcome template reports only suitability, aggregate outcome, material limitations, gate status, recommendation, and authorised references

All CI, 67 Rust tests, 25,000 deterministic parser mutations, current/historical RTL corpus, independent oracle, hostile-input isolation, evidence-gate adversarial tests, operations qualification, and RustSec audit checks passed. No external evidence has been invented; CQ-SAT/GCC remains a research preview pending partner-operated assessment.

CQ-SAT/GCC v0.21.0

External evaluation engagement kit

CQ-SAT/GCC v0.21.0 makes controlled external assessment and design-partner outreach ready to begin.

The release adds:

• a sendable design-partner introduction with the exact bounded SAFE/UNSAFE claim and explicit non-certification language
• partner suitability criteria, a ten-step engagement sequence, project/partner responsibilities, and a pre-transfer go/no-go call
• a private pilot intake covering authority, confidential-data handling, immutable environments, project/property records, operator exercises, closeout, and public-redaction approval
• a copyable 15-key independent aggregate attestation and exact production-gate invocation
• an independent security and formal-verification assessment statement of work with hands-on attack scope, adversarial models, attributable deliverables, finding remediation, and retesting

The templates explicitly prohibit confidential source transfer through public GitHub, are not legal agreements, and cannot close a readiness gate by themselves.

All CI, 67 Rust tests, 25,000 deterministic parser mutations, current/historical RTL corpus, independent oracle, hostile-input isolation, evidence-gate adversarial tests, operations qualification, and RustSec audit checks passed. The canonical external register remains empty, so CQ-SAT/GCC remains a research preview pending real independent and partner evidence.

CQ-SAT/GCC v0.20.0

Machine-enforced external production gate

CQ-SAT/GCC v0.20.0 turns the fixed v0.19 external-evidence protocol into a fail-closed executable check.

The checker enforces:

• canonical injection-resistant register syntax and SHA-256 evidence fields
• at least seven security-review and three technical-review cases
• at least two organisations, three real projects, two domains, two workers, and 30 partner configurations
• minimum SAFE, UNSAFE, and expected-failure coverage
• expected/CQ/oracle agreement and exact result/exit semantics
• positive runtime/memory evidence, repeatability, validated bundles, witness replay, and partner triage
• zero open high/critical findings and complete independent attestations
• annotated release tags that peel to the exact attested Git commit

CI exercises a complete synthetic passing package and rejects disagreement, exit mismatch, missing replay, unresolved rows, spreadsheet injection, failed security assessment, invalid date, undersized cohorts, symlinks, lightweight tags, and tag/commit mismatch. Synthetic fixtures never enter the canonical register.

All product, Linux portability, RTL corpus, isolation, independent oracle, mutation, operations, and RustSec checks passed. The public register remains header-only, so CQ-SAT/GCC remains a research preview until real independent and partner evidence satisfies this gate.

CQ-SAT/GCC v0.19.0

Fixed external production-evidence gates

CQ-SAT/GCC v0.19.0 makes the remaining route to a production claim measurable and resistant to moving the goalposts.

It defines:

• independence and competency requirements for security and technical reviewers
• minimum adversarial attack reproduction and semantic-review scope
• a cohort of at least two embedded-product organisations, three real RTL projects, two domains, and 30 reviewed configurations
• minimum SAFE, UNSAFE, and expected-failure coverage
• independent oracle comparison, zero unresolved result disagreements, complete failure accounting, replay, repeatability, operator exercises, and independent sign-off
• a canonical UTF-8 CSV evidence-register contract with digest, enum, unit, empty-field, denominator, confidentiality, and spreadsheet-injection rules

The evidence register remains deliberately header-only: no customer, assessor, or pilot result has been invented.

All CI, 67 Rust tests, 25,000 deterministic parser mutations, current/historical RTL corpus, independent oracle, isolation profile, operations qualification, and RustSec audit checks passed. CQ-SAT/GCC remains a research preview until the external protocol is actually satisfied.