Skip to content

AUDIT.adoc

Latest commit

 

History

History
107 lines (87 loc) · 3.98 KB

AUDIT.adoc

File metadata and controls

107 lines (87 loc) · 3.98 KB
Raw

Absolute Zero — Audit Trail

Table of Contents

1. Purpose

Estate-wide audit log for absolute-zero. Records all axiom/postulate discharges, unsoundness findings, deletions of dead code, license audits, and other trust-boundary events.

For architectural decisions (which are forward-looking design choices rather than backward-looking audit events), see .machine_readable/descriptiles/META.a2ml architecture-decisions.

2. Open Audit Items

None open. AUDIT-2026-05-20-A (Idris Types.idr errors) was resolved in PR #100 — see Resolved Audit Items below.

3. Resolved Audit Items

ID Date resolved Description Resolution commit

AUDIT-2026-07-06-A

2026-07-06

Unsoundness finding — 3 axioms. During the two-pillar discharge, three Coq axioms were found to be UNSOUND and removed/corrected: no_cloning (provably false in the flat 1-qubit model — witnessed by I_gate), Cconj_Cexp (false for a genuine phase: (e^{iθ})* ≠ e^{iθ}), and eta_equivalence (false as stated — counterexample f = LVar 5; root cause: subst does not re-index under binders). eta_equivalence was replaced by a no_lambda-guarded theorem; the other two were dead code and deleted.

PR #100 (6b591f12)

AUDIT-2026-05-20-A

2026-07-06

src/abi/Types.idr 5 pre-existing errors (missing Decidable.Equality import; %runElab without ElabReflection; MkStateHandle/MkProgramHandle nonNull auto-proof via choose; No absurd DecEq instances removed as unused). ABI packaging restructured (module paths ↔ sourcedir); Idris ABI now builds clean.

PR #100 (6b591f12)

AUDIT-2026-07-06-B

2026-07-06

CNO axiom base reduced 98 → small classified remainder and both pillars (CNO + OND) machine-checked across six provers + Idris. Remaining axioms are tagged METAL-BOUNDARY physical postulates or openly-labelled class-A items; Print Assumptions on every headline theorem shows only Coq stdlib axioms
tagged postulates. Reproduce: proofs/verify-all-provers.sh.

PR #100 (6b591f12)

AUDIT-2026-05-20-B

2026-05-26

.github/workflows/cflite_pr.yml missing actions/checkout before build_fuzzers. Added explicit checkout step pinned to v6.0.2 SHA.

PR #41 follow-up

AUDIT-2026-05-20-#27

2026-05-25

Unsound alignmentMatchesPlatformWord postulate (Idris2). The universal-quantification claim could derive So (1 mod 8 == 0) from the file’s own CNOResultLayout.alignment since HasAlignment t n carries no evidence about n. Companion alignedSizeCorrect postulate isolated into shared Proofs/DivMod.idr for cross-estate incremental discharge.

aac48b7, f0f9b8f, d2853ca (PR #41 / merged via #40)

AUDIT-2026-05-20-#24

2026-05-20

eval_deterministic discharged from Axiom → Theorem via step_deterministic_strong helper. First post-T0 axiom audit win.

PR #24 (see descriptiles/META.a2ml ADR-007)

AUDIT-2026-05-20-#32

2026-05-20

Deleted unsound eval_respects_state_eq_{left,right} axioms; weakened logically_reversible to observational reversibility (=st=); re-proved cno_eval_on_equal_states
cno_logically_reversible via cno_terminates
cno_preserves_state.

PR #32 (see descriptiles/META.a2ml ADR-008)

AUDIT-2026-02-05

2026-02-05

License canonicalisation across the estate to PMPL-1.0-or-later (79 files updated). Pre-existing AGPL references reconciled.

see docs/archive/LICENSE-AUDIT-2026-02-05.adoc

4. Audit categorisation

Audit IDs follow AUDIT-<YYYY-MM-DD>-<seq-or-PR>:

  • PR-numbered IDs map directly to GitHub PRs that close the item.

  • Seq-numbered IDs (A, B, C…) are pre-PR findings that still need a tracking issue or PR.

5. See also

  • .machine_readable/descriptiles/META.a2ml — forward-looking architecture decisions (ADR-001…N)

  • docs/archive/ — historical session / audit artefacts (dated)

  • RSR_COMPLIANCE.adoc — Rhodium Standard Repository compliance status