Skip to content

GCC v0.30.0

Latest
Latest

Choose a tag to compare

View all tags
@github-actions github-actions released this 22 Jul 11:43
v0.30.0
122bff8
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Guarded Continuation Checker v0.30.0

GCC 0.30.0 adds proof-carrying bounded revision-impact analysis for firmware
and RTL research workflows. GCC remains an evaluation-ready research prototype,
not a production-qualified or certified verification product.

Release highlights

  • Adds a deterministic revision-impact certificate that binds a complete
    admitted old/new counterfactual table to independently checkable
    revision-local evidence.
  • Distinguishes source changes that invalidate evidence from inclusion-minimal
    changes that actually alter a bounded SAFE or UNSAFE answer.
  • Adds bounded Rust, strict file CLI and typed subprocess interfaces with exact
    no-fallback verification, resource policy and logical-work observability.
  • Qualifies a connected two-change OpenTitan PWM cohort with 20 observations,
    separate core-only and channel-only effects, and a combination-only
    regression.
  • Reproduces the exact public artifact and nine hostile drift rejections in a
    hosted Linux release build.
  • Records agreement with maintained Yosys, rIC3 and Certifaiger evidence for
    all 9 SAFE and 11 UNSAFE observations.
  • Retains both sides of the measured result: GCC is about 53.78 times faster
    from source through answer for the matched shared-model orchestration run and
    uses about 20.0 percent less producer-path peak RSS, while its artifact is
    about 8.32 times larger.
  • Adopts QatQ 0.1.4's upstream exact-byte container API while preserving the
    frozen GCC transport bytes and keeping QatQ outside the production profile.
  • Adds a crates.io-backed public Rust API compatibility gate using pinned
    cargo-semver-checks 0.49.0. The gate explicitly admits additive operation
    telemetry variants as a pre-1.0 minor change while retaining every other
    default major-change check.

The timing result compares one shared GCC workflow with 20 isolated maintained
jobs. It is not a universal solver-performance claim.

Installation

Install the complete research build:

cargo install guarded-continuation-checker --version 0.30.0 --locked

Install the frozen firmware and RTL profile:

cargo install guarded-continuation-checker --version 0.30.0 --locked \
  --features production-firmware
guarded-continuation-checker production-profile-version

The production-profile capability remains:

production_support_profile=firmware-rtl-v1 firmware_cli_version=2 artifact_schema_version=4

Revision impact and QatQ transport are research surfaces. They are not included
in firmware-rtl-v1.

Claim boundary

Incremental proof reuse, mutation impact, compositional verification and
multi-property checking have substantial prior art. This release demonstrates
a narrow source-bound certificate and self-service workflow, not a proven novel
algorithm. A systematic closest-implementation search, external expert review,
broader public subsystems, warm and parallel baseline comparisons, and external
product evaluation remain open.

Assets 6
Loading