Skip to content

OPT v1.1.0 — Lean 4 Formal Verification Layer

Choose a tag to compare

View all tags
@EmergentMonk EmergentMonk released this 03 Sep 11:39
Immutable release. Only release title and notes can be modified.
v1.1.0
10c2e27
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

#RELEASE NOTES#

OPT v1.1.0 adds a dependency-free Lean 4 formal verification layer for the immutable OPT v1.0.0 optimization catalog.

This release does not rewrite the frozen optimization records. Instead, it adds machine-checkable contracts for their core invariants, evidence boundaries, trust assumptions, and admissibility rules.

Highlights

Lean 4 formalization

The release formalizes key OPT principles including:

  • Correctness outranks speed

    • A faster implementation that changes required semantics is not an optimization.

  • Adaptation boundaries

    • Admissible optimizations must preserve:

      • semantics
      • named invariants
      • determinism
      • validation
      • provenance
      • evidence boundaries
      • public API behaviour

  • OPT-INV-001

    • Cached or reused computation is valid only under an explicit equivalence witness.

  • OPT-PAR-001

    • Parallel execution must preserve the scalar/reference result when the deterministic equivalence contract applies.

  • OPT-LEAN-001

    • Verified dependency reuse does not constitute evidence of a cold reconstruction.

  • DSP approximation contracts

    • Approximate implementations require an explicit error bound, validated tolerance, and reference comparison.

  • Resource composition

    • Composed optimizations are modeled against combined CPU, memory, and I/O requirements.

Evidence and benchmark semantics

v1.1.0 formally separates:

  • historical observations;
  • environment-specific measurements;
  • transferable performance targets.

No evidence status, including verified, is sufficient by itself to authorize a transferable benchmark target.

Promotion to a transferable target requires explicit target-context evidence covering:

  • target-environment measurement;
  • correctness validation;
  • provenance binding.

This prevents source-project benchmark numbers from silently becoming universal performance claims.

Frozen v1.0.0 catalog model

The formal model represents the five records frozen in OPT v1.0.0:

  • OPT-PY-001
  • OPT-INV-001
  • OPT-LEAN-001
  • OPT-PAR-001
  • OPT-DSP-001

Lean proves that the formal catalog contains exactly five distinct records.

suxen.zip remains explicitly classified as source-candidate material. Keyword inventory results are not promoted into measured-performance evidence.

Trust boundary hardening

The Lean layer was subjected to repeated adversarial review and hardened against multiple proof-surface and CI escape paths.

Source-purity gate

Lean source scanning rejects executable uses of:

  • sorry
  • sorryAx
  • admit
  • axiom
  • constant
  • unsafe

The scanner distinguishes executable syntax from inert content including:

  • line and nested block comments;
  • ordinary strings;
  • hash-delimited raw strings;
  • interpolated strings;
  • nested interpolation;
  • character literals;
  • guillemet-quoted identifiers.

Regression cases cover bypass attempts involving comment markers, interpolation braces, raw strings, quoted identifiers, and direct sorryAx use.

Full declaration-level axiom audit

The trust audit is no longer limited to a hand-maintained theorem list or even proposition-valued declarations.

Every declaration originating from the formal module set is inspected.

The audited module boundary includes:

  • OPTFormal
  • every OPTFormal.* module
  • OPTFormalAll

The audit:

  1. identifies declarations by their originating module rather than namespace;
  2. rejects project-originating primitive .axiomInfo declarations;
  3. runs Lean.collectAxioms across every formal declaration;
  4. permits only Lean core propext;
  5. classifies proposition-valued declarations only after the complete declaration audit succeeds.

On the final reviewed PR head, the audit covered:

  • 354 formal declarations
  • 101 logical exports

This also prevents generated or data-valued declarations from creating an unaudited proof channel.

Multi-version formal audit root

Lean/OPTFormalAll.lean provides an unpinned audit root for current and future formal modules.

CI recursively enumerates every module under:

Lean/OPTFormal/

and requires the audit root to import the complete set.

Future modules such as a hypothetical OPTFormal.FrozenV200 therefore cannot silently exist outside the formal audit graph.

Declarations are tracked by originating module, so placing a theorem in the root namespace or an unrelated namespace does not evade the trust boundary.

Frozen v1 formal-model integrity

The constructed v1 formal model is permanently bound to Git history.

Protected files include:

  • Lean/OPTFormal/Core.lean
  • Lean/OPTFormal/FrozenV100.lean
  • Lean/OPTFormal.lean

Rather than storing editable expected blob hashes beside the CI check, the workflow derives the baseline from the historical commit that established the three-file blob gate on the canonical first-parent lineage.

For the merged PR #2 history, that anchor is:

a6fc797ef5759a5f0005b18630748ba68b5c7631

First-parent traversal prevents merged side history from substituting an alternative earlier baseline.

Future releases may add separately versioned formal modules, but the v1 formal model cannot be silently rewritten.

Reproducible Lean environment

The formal package intentionally has no mathlib or third-party Lean dependencies.

CI pins:

  • Lean 4.33.1
  • the exact lean-toolchain declaration
  • the official Lean Linux distribution SHA-256
  • the checkout action by commit SHA

The Lean archive is downloaded from the official release and authenticated before extraction.

Validation

The final PR #2 head passed both required validation lanes:

Lean formalization

  • frozen v1.0.0 identity verified
  • canonical first-parent model anchor verified
  • source scanner self-tests passed
  • source-purity scan passed
  • complete formal-module coverage verified
  • OPTFormal built successfully
  • OPTFormalAll built successfully
  • 354 formal declarations audited
  • 101 logical exports classified
  • axiom allowlist verified
  • only core propext permitted

Existing OPT regression suite

  • ZIP inventory regression tests passed
  • bundled SUXEN archive audit passed
  • existing OPT behavior remained green

Provenance

Frozen OPT v1.0.0 release commit:

41e2fc3677469839fb298dedefd0ce72caebcc68

Final reviewed PR #2 head:

530287344756f0a3444bcf419d81fe3e6339e7e2

PR #2 merge commit:

10c2e27075b9174ef2f2d586c281dc1da45588b5

Pull request:

QSOLKCB/OPT#2

Release principle

Correctness outranks speed.

OPT v1.1.0 turns that principle from repository doctrine into an executable formal contract.

Optimization remains optimization only when the required semantics, evidence boundaries, determinism, provenance, and validation survive the transformation.

Assets 3
Loading