Skip to content

fix(agda): repair EchoSearchExample against current axis-8 API and wire it in - #353

Merged
hyperpolymath merged 3 commits into
mainfrom
claude/kind-clarke-aqpe7a
Oct 26, 2026
Merged

fix(agda): repair EchoSearchExample against current axis-8 API and wire it in#353
hyperpolymath merged 3 commits into
mainfrom
claude/kind-clarke-aqpe7a

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Oct 26, 2026

Copy link
Copy Markdown
Owner

Summary

proofs/agda/EchoSearchExample.agda did not compile on main. It imported an API that never landed: BoundedSearch, bounded-search, bounded-search-to-{echo,cost,dec,access-feasible} from EchoSearch, EchoCost as a type, and EchoA from EchoAccess. It was not in All.agda, so CI never checked it.

I repaired it rather than deleting it. EchoSearchInstance only pins proof-of-life terms at the trivial-on-⊤ instance. This module is the one non-trivial operational exhibit that chains the axis-8 refinements together on a concrete witness.

Changes

EchoSearchExample.agda is rewritten against the current exports:

Headline Type Content
double ℕ → ℕ the map
search-double-6 EchoS id double 6 4 hit at step 3
search-double-6-decided bounded-search-is-decidable _≟_ id double 6 4 ≡ yes search-double-6 proved by refl: the decision procedure already in EchoSearch finds the witness itself
search-as-echo Echo double 6 echo-search-forget
search-as-cost EchoC search-steps 4 double 6 uses a real ℕ step-cost CostAlgebra; under the identity enumerator k < n is definitionally suc k ≤ n
search-as-dec EchoDec double 6 yes from the search hit
search-as-feasible CEcho feasible double 6 degrade-access free≤feasible. The carrier is the Lift ⊤ placeholder by design (see decisions/echo-access-trivial-carrier.adoc), so this records the grade only; the module comments say so
  • The module stays --safe --without-K with no postulates.
  • It is wired into All.agda after EchoSearchInstance.
  • All seven headlines are pinned in Smoke.agda.

Verification

Run locally with Agda 2.6.3 and stdlib 2.3, after bash scripts/provision-agda.sh with absolute-zero checked out as a sibling:

  • On main, agda -i proofs/agda proofs/agda/EchoSearchExample.agda fails with a scope error. On this branch it passes.
  • agda -i proofs/agda proofs/agda/All.agda exits 0.
  • agda -i proofs/agda proofs/agda/Smoke.agda exits 0.
  • sh scripts/kernel-guard.sh passes.
  • bash tools/check-guardrails.sh passes for all 137 modules.

Generated by Claude Code

@claude
fix(agda): repair EchoSearchExample against current axis-8 API and wi…
cd00bf8 
…re it in

EchoSearchExample imported a `BoundedSearch` / `bounded-search-to-*`
API from EchoSearch (and `EchoCost`/`EchoA` names) that never landed,
so the module failed scope checking. It was not in All.agda, so CI
never saw it.

Re-express the exhibit against the current exports:

* search-double-6 : EchoS id double 6 4 (hit at step 3)
* search-double-6-decided : the landed bounded-search-is-decidable
  computes to `yes search-double-6` by refl
* search-as-cost : EchoC over a real ℕ step-cost CostAlgebra; under
  the identity enumerator `k < n` is definitionally `suc k ≤ n`
* search-as-dec : EchoDec from the search hit
* search-as-feasible : degrade-access free≤feasible (grade-only
  Lift ⊤ carrier, per the echo-access-trivial-carrier decision)

Still --safe --without-K, no postulates. Wired into All.agda and the
headlines pinned in Smoke.agda.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01P4yFkxW5Heb8p2YW7ZYs9F
@coderabbitai

coderabbitai Bot commented Oct 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 59 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration
  • Source mode: Auto
  • Repository: Unavailable
  • Branch: Unavailable
  • File: No configuration file from this repository applied
  • Commit: Unavailable
  • Layers: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: 062f401d-172a-4165-bfce-c12060495fb6
Commits

Reviewing files that changed from the base of the PR and between cb1eaa3 and fb2cf86.

Files selected for processing: 3
  • proofs/agda/All.agda
  • proofs/agda/EchoSearchExample.agda
  • proofs/agda/Smoke.agda
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@github-actions

github-actions Bot commented Oct 26, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 38 issues detected

Severity Count
🔴 Critical 0
🟠 High 12
🟡 Medium 26
View findings 
[
  {
    "reason": "Required file missing",
    "type": "missing",
    "file": "0-AI-MANIFEST.a2ml",
    "level": "epi",
    "action": "create",
    "rule_module": "root_hygiene",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": "0-AI-MANIFEST.a2ml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "root_hygiene/missing",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 39,
          "start_line": 39
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 53,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 53,
          "start_line": 53
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 87,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 87,
          "start_line": 87
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/push-email-notify.yml",
          "end_line": 46,
          "start_line": 46
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 34,
    "reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 34,
          "start_line": 34
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 48,
    "reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 48,
          "start_line": 48
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": null,
    "reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
    "type": "WH014",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_hardening/WH014",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath
hyperpolymath marked this pull request as ready for review October 26, 2026 18:21
@hyperpolymath
hyperpolymath enabled auto-merge (squash) October 26, 2026 18:21
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Oct 26, 2026 •
edited
Loading

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-10-26T19:39:46.847730Z fb2cf86 New commits
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

chatgpt-codex-connector[bot]
chatgpt-codex-connector Bot reviewed Oct 26, 2026
View reviewed changes

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: cd00bf8871

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread proofs/agda/EchoSearchExample.agda Resolved
@claude
docs(agda): correct EchoSearchExample's claims about the decider's se…
8ae2bb0 
…arch order

bounded-search-is-decidable tests indices from the top of the budget
downwards, so on this instance it hits index 3 on its first comparison;
it does not walk 0, 1, 2, 3. Reword the comments so search-double-6-decided
is described as a one-comparison hit, and so search-steps is described
as the enumeration position (the cost the bound k < n certifies), not
the decider's executed work. Comment-only; no proof terms change.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01P4yFkxW5Heb8p2YW7ZYs9F
@github-actions

github-actions Bot commented Oct 26, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 38 issues detected

Severity Count
🔴 Critical 0
🟠 High 12
🟡 Medium 26
View findings 
[
  {
    "reason": "Required file missing",
    "type": "missing",
    "file": "0-AI-MANIFEST.a2ml",
    "level": "epi",
    "action": "create",
    "rule_module": "root_hygiene",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": "0-AI-MANIFEST.a2ml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "root_hygiene/missing",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 39,
          "start_line": 39
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 53,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 53,
          "start_line": 53
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 87,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 87,
          "start_line": 87
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/push-email-notify.yml",
          "end_line": 46,
          "start_line": 46
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 34,
    "reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 34,
          "start_line": 34
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 48,
    "reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 48,
          "start_line": 48
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": null,
    "reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
    "type": "WH014",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_hardening/WH014",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath
hyperpolymath merged commit 7f1778c into main Oct 26, 2026
6 of 7 checks passed
@hyperpolymath
hyperpolymath deleted the claude/kind-clarke-aqpe7a branch October 26, 2026 19:38
@github-actions

github-actions Bot commented Oct 26, 2026

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 38 issues detected

Severity Count
🔴 Critical 0
🟠 High 12
🟡 Medium 26
View findings 
[
  {
    "reason": "Required file missing",
    "type": "missing",
    "file": "0-AI-MANIFEST.a2ml",
    "level": "epi",
    "action": "create",
    "rule_module": "root_hygiene",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": "0-AI-MANIFEST.a2ml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "root_hygiene/missing",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_audit/missing_timeout_minutes",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 39,
          "start_line": 39
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 53,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 53,
          "start_line": 53
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 87,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 87,
          "start_line": 87
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/push-email-notify.yml",
          "end_line": 46,
          "start_line": 46
        },
        "rule": "research_extensions/RE001",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 34,
    "reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/labels.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/labels.yml",
          "end_line": 34,
          "start_line": 34
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": 48,
    "reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/label-triage.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "medium",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/label-triage.yml",
          "end_line": 48,
          "start_line": 48
        },
        "rule": "workflow_hardening/WH006",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  },
  {
    "line": null,
    "reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
    "type": "WH014",
    "file": ".github/workflows/hypatia-scan.yml",
    "level": "epi",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "high",
    "evidence": [
      {
        "span": {
          "file": ".github/workflows/hypatia-scan.yml",
          "end_line": 0,
          "start_line": 0
        },
        "rule": "workflow_hardening/WH014",
        "observations": 1,
        "rule_version": "0.1.0"
      }
    ],
    "support": {
      "kind": "pattern"
    }
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath mentioned this pull request Nov 9, 2026
Merged
hyperpolymath added a commit that referenced this pull request Nov 9, 2026
@hyperpolymath @claude
proofs: EchoSearchExample PWG-2ii (Agda receipt + Rocq and Lean legs,…
9abd8a5 
… reconciled) (#368)

## Summary

This PR takes `EchoSearchExample` (#353), a theory theorem, through the
estate proof policy (PROOF-POLICY §2, §5, §8 at standards `9bdf864`). It
adds an Agda receipt, hand re-proofs in **Rocq** and **Lean 4** (core
only, no Mathlib) that are kernel-checked with no axioms, and a full
§2.2 correspondence record.

**Computed grade: `PWG-2ii`, with no axioms.**
- Agda leg: `PROVEN`.
- Rocq and Lean legs: route `re-proved`, `PROVEN`, `RECONCILED`.

**How the legs were reconciled.** An agent wrote the statement
comparison, and the owner accepted it on 2026-11-09 without a separate
line-by-line review. The record says so explicitly, in commit `4147da7`.
Grade `PWG-1` additionally needs current receipts from the pinned CI
lanes for every witness; the lanes added here produce them on every
push.

## Changes

| File | What |
|---|---|
| `proofs/rocq/EchoSearchExample.v` | Rocq re-proof of every headline.
It restates `Echo`, `EchoS`, the downward-scanning
`bounded-search-is-decidable`, `EchoC` at the step-cost instance,
`EchoDec`, and the access lattice (`CEcho` / `degrade-access`, all 15
pairs). `decided = yes search_double_6` holds by `reflexivity`. |
| `proofs/lean4/EchoSearchExample.lean` | The same in Lean 4 core, with
no imports. |
| `proofs/RECHECK-EchoSearchExample.adoc` | The §2.2 record: statements
side by side, residual differences, receipts, the §6 toolchain deviation
(state `open`), and revalidation triggers. |
| `scripts/setup-recheck.sh`, `scripts/check-recheck.sh` | Toolchains
with asserted versions: Coq 8.18.0 from Ubuntu, and Lean 4.30.0 from a
release archive pinned by checksum. The check fails on any axiom,
`sorry`, warning or error. |
| `.github/workflows/agda.yml` | New `rocq-recheck` and `lean-recheck`
jobs. They reuse the existing pinned checkout line, so `actions.lock` is
unchanged. |
| `PROOF-STATUS.adoc` | Per-theorem PWG table with a census line, and
the 2026-11-09 cold-check record. Bare "Grade 3" becomes `PWG-3` (§8
prefix rule). |
| `docs/proof-witness-audit.adoc` | Note that §8 supersedes the brief's
scale. The dated audit text is otherwise unchanged. |
| `docs/receipts/agda-cold-2026-11-09.log.gz` | Full Agda log;
uncompressed sha256 `7f9de4d1…`. |

## Residual differences

These are recorded in full in the correspondence record; none of them
changes what the headlines state.
- **Identity type:** Lean's `Eq` has definitional proof irrelevance, so
K holds in Lean, whereas Agda is checked `--without-K`. No proof here
uses K: every one is a closed computation or a re-pairing.
- **`Prop`-valued order and decision types:** `_<_` and `Dec` live in
`Prop` in the targets.
- **Universes:** handled differently in each prover.
- **Scope:** the cost-algebra laws are not restated, because no headline
depends on them.

## Verification

- **Agda:** I ran the cold check at `ccec4d7` with
`scripts/setup-agda.sh` (Agda 2.7.0.1, stdlib `8326c74`, absolute-zero
`f486c29`). These exited 0:
  - the 5 static guards;
- all 7 `--safe --without-K --cubical-compatible` roots, with
`--ignore-interfaces`;
  - the `--safe --cubical` island.

The only warnings were the known `UnsupportedIndexedMatch` ones. No Agda
source changed in this PR.
- **Recheck legs:** `bash scripts/check-recheck.sh all` gives Rocq 5/5
`Print Assumptions` closed and Lean 5/5 `#print axioms` with no axioms.
- **Mutants:** changing `double`, or setting the decided budget to 3,
makes both legs fail.
- **Static guards after the change:** `kernel-guard`, `check-guardrails`
and the invocation lint all pass.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01P4yFkxW5Heb8p2YW7ZYs9F

---------

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chatgpt-codex-connector chatgpt-codex-connector[bot] chatgpt-codex-connector[bot] left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hyperpolymath @claude