proof(idris2/abi): delete unsound alignmentMatchesPlatformWord, isola…

[hyperpolymath]

…te alignedSizeCorrect into shared DivMod module (#27)

The alignmentMatchesPlatformWord postulate in src/abi/Layout.idr was not merely unproven but unsound. HasAlignment t n has a single information-free constructor AlignProof, so the universal claim HasAlignment t n -> So (n mod (word/8) == 0) could derive So (1 mod 8 == 0) from CNOResultLayout.alignment : HasAlignment CNOVerificationResult 1. The unsoundness was hidden by the postulate's single consumer only ever instantiating n at 8.

Replace it with a per-Platform decidable proof of the only specific claim that was actually used (programStateAlignmentValid). The verifyAlignment helper, whose only purpose was to call the postulate, is removed (no other callers).

The remaining alignedSizeCorrect postulate is moved to a new AbsoluteZero.ABI.Proofs.DivMod module that consolidates the estate-wide trusted div/mod base. Each lemma is named separately so discharge can be incremental, and civic-connect's alignUpDivides / mkFieldsAligned / offsetInBoundsPrf deferrals are intended to migrate onto the same surface.

Tracked as ADR-009.

[github-actions]

🔍 Hypatia Security Scan

Findings: 167 issues detected

Severity	Count
🔴 Critical	7
🟠 High	55
🟡 Medium	105

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Superseded by 0-AI-MANIFEST.a2ml",
    "type": "banned",
    "file": "AI.djot",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/absolute-zero/absolute-zero",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6.0.2 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/configure-pages@v6 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/jekyll-build-pages@v1 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/upload-pages-artifact@v5 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence