refactor(proofs/coq): consolidate trusted-base dups (Follow-ups 1+2+3)#67
Merged
Merged
Conversation
…stants (Follow-up 1) Replaces three triplicated `Parameter kB / Axiom kB_positive` + `Parameter temperature / Axiom temperature_positive` declarations across QuantumCNO.v, StatMech.v, and LandauerDerivation.v with a single canonical source at `proofs/coq/common/PhysicsConstants.v`. Each caller now does `Require Import CNO.PhysicsConstants` instead of redeclaring. Net escape-hatch count: 129 → 125 (−4: removed 6 sites, added 2 canonical sites). `check-trusted-base.sh` undocumented count unchanged at 4 (Idris2 BoJ markers; out of Phase 2 scope). Verification: - `coqc -R common CNO common/PhysicsConstants.v` — OK - `coqc -R common CNO physics/StatMech.v` — OK - `coqc -R common CNO physics/LandauerDerivation.v` — OK - `coqc -R common CNO quantum/QuantumCNO.v` — OK - `check-trusted-base.sh` — 4/125 undocumented (unchanged) Refs: docs/proof-debt-triage.md (Phase 1, #58); Follow-up 1 listed in "Follow-ups surfaced by triage", now marked DONE in the same file. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,39 @@ | |||
| (** * Physical Constants — Shared Across CNO Theory | |||
🔍 Hypatia Security ScanFindings: 67 issues detected
View findings[
{
"reason": "Ada pragma Suppress disables runtime checks (1 occurrences, CWE-704)",
"type": "ada_pragma_suppress",
"file": "/home/runner/work/absolute-zero/absolute-zero/examples/ada/balanced_ops.adb",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/lambda/LambdaCNO.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (8 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/StatMech.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "Coq admit tactic leaves goal unproven (1 occurrences, CWE-704)",
"type": "coq_admit_tactic",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (12 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/category/CNOCategory.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (13 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/filesystem/FilesystemCNO.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (3 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumMechanicsExact.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (27 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumCNO.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/common/PhysicsConstants.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
… + statmech basis
Builds on Follow-up 1 (PhysicsConstants.v) with the remaining two
mechanical dedupes from docs/proof-debt-triage.md.
Follow-up 2 — dead duplicate axioms removed from QuantumMechanicsExact.v:
- `unitary_preserves_entropy` (line 323) — was dead code; canonical lives
in QuantumCNO.v (which uses an unindexed `QuantumGate`, the only form
with downstream callers).
- `no_cloning` (line 404) — was dead code AND its statement `forall ψ,
False` was trivially `True`-equivalent. Canonical in QuantumCNO.v.
Follow-up 3 — statmech basis consolidated:
- New file `proofs/coq/common/StatMechBasis.v` declares once:
`StateDistribution`, `prob_nonneg`, `prob_normalized`, `state_dec`,
`point_dist`, `shannon_entropy` (parameter), `shannon_entropy_nonneg`,
`shannon_entropy_point_zero`.
- `StatMech.v` and `LandauerDerivation.v` import via
`Require Import CNO.StatMechBasis` and drop their local copies.
- `state_eq_dec` aliased into canonical `state_dec` (LandauerDerivation
only used the local name internally; no external callers).
Cleanup + machine-readable:
- `.gitignore`: adds Coq build artefact patterns (*.vo, *.vok, *.vos,
*.glob, .*.aux, .lia.cache, .nia.cache) so future builds don't pollute
status output.
- `_CoqProject`: adds `common/StatMechBasis.v` to the build manifest
(alongside PhysicsConstants.v from Follow-up 1).
- `.machine_readable/META.scm`: ADR-011 (Phase 2a–2e Lean triage) and
ADR-012 (Follow-ups 1–3 consolidation) recorded.
- `docs/proof-debt-triage.md`: Follow-ups 2 + 3 marked DONE.
Verification:
- `coqc -R common CNO common/{PhysicsConstants,Complex,CNO,StatMechBasis}.v`
— OK
- `coqc -R common CNO physics/{StatMech,LandauerDerivation}.v` — OK
- `coqc -R common CNO quantum/{QuantumCNO,QuantumMechanicsExact}.v` — OK
- `check-trusted-base.sh` — 4/118 undocumented (remaining 4 are Idris2
`src/abi/Proofs/DivMod.idr`; out of Phase 2 scope). Net change since
Phase 2e closeout (#66): 129 → 118 markers, −11.
Refs: docs/proof-debt-triage.md (Phase 1 #58); Phase 2a (#60),
Phase 2b (#61), Phase 2c (#62), Phase 2d (#63), Phase 2e (#66).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
changed the title
| @@ -0,0 +1,75 @@ | |||
| (** * Statistical Mechanics Basis — Shared Probability + Entropy Axioms | |||
🔍 Hypatia Security ScanFindings: 68 issues detected
View findings[
{
"reason": "Ada pragma Suppress disables runtime checks (1 occurrences, CWE-704)",
"type": "ada_pragma_suppress",
"file": "/home/runner/work/absolute-zero/absolute-zero/examples/ada/balanced_ops.adb",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumMechanicsExact.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (27 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/quantum/QuantumCNO.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/lambda/LambdaCNO.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/category/CNOCategory.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/common/PhysicsConstants.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (5 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/common/StatMechBasis.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (13 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/filesystem/FilesystemCNO.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "Coq admit tactic leaves goal unproven (1 occurrences, CWE-704)",
"type": "coq_admit_tactic",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (7 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/absolute-zero/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Mechanical follow-ups 1, 2, 3 from the Phase 1 proof-debt triage (#58). Consolidates triplicated / duplicated trusted-base axioms into shared modules and removes dead duplicate copies, reducing the estate trust base by 11 markers (129 → 118) without changing semantics.
Follow-up 1 — physics constants (
PhysicsConstants.v)proofs/coq/common/PhysicsConstants.v— single declaration ofkB,kB_positive,temperature,temperature_positive.QuantumCNO.v,StatMech.v,LandauerDerivation.v— drop local declarations,Require Import CNO.PhysicsConstants.Follow-up 2 — quantum laws (dead-code removal in
QuantumMechanicsExact.v)Axiom unitary_preserves_entropy(line 323) andAxiom no_cloning(line 404) fromQuantumMechanicsExact.v. Both were dead code (no in-file callers). Theno_cloningbodyforall ψ, Falsewas triviallyTrue-equivalent, so removal also strengthens the trust base.QuantumCNO.vdeclarations remain (used byquantum_cno_preserves_informationand friends).Follow-up 3 — statmech basis (
StatMechBasis.v)proofs/coq/common/StatMechBasis.v— single declaration ofStateDistribution,prob_nonneg,prob_normalized,state_dec(canonical name; subsumesstate_eq_dec),point_dist,shannon_entropy,shannon_entropy_nonneg,shannon_entropy_point_zero.StatMech.vandLandauerDerivation.v— drop local declarations,Require Import CNO.StatMechBasis.Cleanup + machine-readable
.gitignore: adds Coq build artefact patterns (*.vo,*.vok,*.vos,*.glob,.*.aux,.lia.cache,.nia.cache) so future builds don't pollute status._CoqProject: registerscommon/PhysicsConstants.vandcommon/StatMechBasis.vin the build manifest..machine_readable/META.scm: ADR-011 (Phase 2a–2e Lean triage campaign) and ADR-012 (Follow-ups 1–3 consolidation) added to the architecture-decisions ledger.docs/proof-debt-triage.md: Follow-ups 1, 2, 3 marked✅ DONE 2026-05-27with the consolidation summaries.Verification
bash ~/developer/repos/standards/scripts/check-trusted-base.sh .:The 4 remaining undocumented markers are in
src/abi/Proofs/DivMod.idr(BoJ vendored proofs) — explicitly out of Phase 2 scope and tracked at #27.Why this is low-risk
The consolidated axioms are opaque
Parameters andAxioms (no executable definitions). Consolidating means all callers now reference the same symbol instead of nominally-distinct copies — strictly an improvement for soundness. The dead-code removal in Follow-up 2 is verified bycoqcbuilding all downstream files unchanged.Refs
docs/proof-debt-triage.md§"Follow-ups surfaced by triage" (1, 2, 3 of 5; 4 + 5 require real proof work, deferred)Test plan
coqc -R common CNO ...(verified locally)check-trusted-base.sh— 129 → 118 markers, undocumented count unchanged at 4.gitignorecovers Coq build artefacts🤖 Generated with Claude Code