INDEPENDENCE v0.8.0 — Deterministic Property Generation & Counterexample Minimisation

Release Notes

INDEPENDENCE v0.8.0 — Deterministic Property Generation & Counterexample Minimisation

Release date: 31 October 2026
Project: QSOL-IMC — Software Declaration of Independence
Release: v0.8.0

Overview

INDEPENDENCE v0.8.0 introduces a fully executable, dependency-free Property Laboratory for deterministic property generation, reproducible fault injection, counterexample minimisation, and typed-array ownership testing.

Building on the v0.7 proof contracts and formally checked reference-model evidence, this release advances the project from checking predefined fixtures to systematically generating inputs, detecting behavioural violations, and reducing failing cases to smaller reproducible witnesses.

Correctness outranks speed. Evidence outranks slogans.

What's New

1. Deterministic Property Generation

• Introduced PROPERTY-LAB/1 with the existing first-party xorshift32 generator.
• Supports reproducible seeds and configurable runs of 1–512 generated cases.
• Tests the real JavaScript cellular automaton against an independently implemented transition oracle.
• Covers bounded binary rows, elementary cellular automaton rules, and fixed-zero boundary semantics.
• Detects incorrect outputs and mutation of input typed arrays.
• Produces identical generated vectors for identical configurations.

2. Counterexample Minimisation

Introduced a deterministic, bounded counterexample shrinker.

The laboratory uses a deliberately injected wraparound-boundary defect to demonstrate how a larger failing input can be reduced to a canonical minimal witness.

Original counterexample:

• Width: 8
• Rule: 110
• Mask: 255

Minimised counterexample:

• Width: 1
• Rule: 4
• Mask: 1

The shrinker uses a documented width-first, rule-then-mask ordering and rechecks the failure predicate during minimisation.

The injected defect is an educational test fixture, not a vulnerability discovered in the deployed automaton.

3. Typed-Array Ownership Protection

Reproduces the existing public-API counterexample in which Object.freeze() protects an enclosing object but does not prevent mutation of its contained Uint8Array.

Added the opt-in guardedSnapshot() interface:

• Validates automaton dimensions, cell values, and fingerprint consistency.
• Rejects stale or corrupted input snapshots.
• Creates independent private copies of cell data.
• Returns fresh typed-array copies to callers.
• Preserves fingerprint consistency against external mutations.

The original buildAutomaton() behaviour is retained for compatibility and historical reproducibility.

4. Interactive Browser Property Lab

Added a new interactive section to the INDEPENDENCE website.

Users can generate deterministic trials, inspect failure classifications, examine minimised counterexamples, and export evidence receipts.

The interface operates entirely in the browser using first-party HTML, CSS and JavaScript, without additional runtime packages, remote services, telemetry or backend infrastructure.

5. Reproducible Evidence Receipts

Introduced PROPERTY-LAB-RECEIPT/1 with SHA-256 fingerprints over exact UTF-8 JSON payloads.

Receipts contain the generator configuration, generated cases, counterexample witnesses, minimisation metadata, ownership observations, and explicit verification limitations.

The new Python standard-library verifier, scripts/verify_property_receipt.py, independently reconstructs expected data and rejects malformed, tampered or internally contradictory reports.

Receipt integrity establishes consistency, not independent authentication of browser execution.

6. Expanded Regression and Security Testing

• Added 16 native JavaScript property assertions.
• Added 16 Python standard-library regression tests.
• Added tests for deterministic replay, invalid configurations, forged receipts, false formal-proof claims and counterexample manipulation.
• Addressed Codex's P2 finding concerning mutation of the actual Uint8Array supplied to evolve().
• Confirmed that correct output cannot conceal source-input corruption.
• Integrated the new Property Lab into the existing GitHub Pages deployment workflow and first-party asset audit.

Verification Results

Local verification against PR #17 HEAD:

Check	Result
Python regression suite	260/260 passed
Repository dependency audit	PASS
Files inspected	160
Dependency/remote asset findings	0
Codex review finding	Fixed and resolved
Historical Lean/SPARK/Ada evidence	Preserved unchanged

Scope and Limitations

Generated property checks are finite behavioural tests, not mathematical proofs of arbitrary JavaScript execution.

Counterexample minimisation is canonical within the explicitly defined bounded search space, not a general-purpose global minimisation guarantee.

The injected wraparound defect is separate from the genuine legacy typed-array ownership counterexample.

This release does not alter or promote the previously recorded Lean 4, SPARK/Ada or Ada/Python verification claims.

Deployment

The Property Lab is integrated into the existing first-party GitHub Pages website.

Live site: https://qsolkcb.github.io/INDEPENDENCE/#property-lab

Run the repository tests and audit:

python3 -m unittest discover -s tests -v
python3 scripts/audit.py --json

Verify an exported Property Lab receipt:

python3 scripts/verify_property_receipt.py property-lab-<hash>.json

No Node.js, npm, Docker, Kubernetes, third-party Python packages or new browser runtime dependencies are required.

Source and Provenance

Merged pull request: #17

Verified PR HEAD: 70177db2c01beb77ae2c7fe19bc11f1776600a1a

Merge commit: b8888deacd8ae72e8812848faafce82047cd9755

License: Apache-2.0

---

THE SOFTWARE DECLARATION OF INDEPENDENCE

This Is Not War, This Is a Divorce.

This Isn't War, This Is Pest Control.

Now with a deterministic shrink ray for catching Gremlins. 👹

QSOL-IMC — Independent Software Sovereignty Initiative

What's Changed

• draft: v0.7.3 Lean 4 Mathematical Foundation — kernel check required by @EmergentMonk in #10
• fix(lean): discharge CRT right-inverse without undecidable product quantifier by @EmergentMonk in #11
• archive: preserve v0.7.3 Lean kernel evidence and exact provenance for Zenodo v1.1.0 by @EmergentMonk in #12
• fix(spark): correct scalar GPR directory attributes before GNATprove by @EmergentMonk in #13
• feat: Pest Control declaration + preserve 21-check SPARK evidence by @EmergentMonk in #14
• feat(v0.7.4): build real Ada CLI and verify Python differential execution by @EmergentMonk in #15
• archive(v0.7.4): preserve original 150/8,903 Ada runtime receipts with exact byte provenance by @EmergentMonk in #16
• feat(v0.8): deterministic property generation, bounded shrinking and ownership guard by @EmergentMonk in #17

Full Changelog: v0.7.2...v0.8.0