theory: EchoSearch — Axis 8 witness-search machine (thin slice)

[hyperpolymath]

Adds proofs/agda/EchoSearch.agda (+ EchoSearchInstance.agda for
smoke pins), the enumerator-bounded witness-search refinement of
Echo named in docs/echo-types/taxonomy.md §Axis 8 / refinement
(4) "witness-search abstract machine".

What lands

• SearchStrategy A := ℕ → A (a total enumeration; partiality is a separate axis-8(2) refinement)
• EchoS enum f y n := Σ ℕ λ k → (k < n) × (f (enum k) ≡ y) — the bound-indexed witness, using stdlib Data.Nat._<_ so <-≤-trans / ≤-<-trans apply without conversion glue
• Headlines echo-search-intro, echo-search-relax (bound monotonicity via <-≤-trans), echo-search-forget (project to plain Echo), echo-search-bound-zero (vacuity at budget 0), echo-search-postcompose (post-compose with g, same index, same bound)
• EchoSearchInstance.agda pins each headline at the trivial A = B = ⊤ enumerator (mirrors the EchoApproxInstance pattern so Smoke.agda can enumerate the parameterised lemmas in a using clause)
• Wired into All.agda + Smoke.agda

Design notes

The roadmap term "abstract machine" admits several honest readings; the smallest is enumerator-bounded witness — a search strategy enum : ℕ → A paired with a step budget n : ℕ. The ℕ-bound is the step budget; a heavier machine (Turing-bounded, polynomial-time, configurations + step relation) projects onto this thin slice by forgetting everything except the index queried and the bound queried under. This sits at the bottom of the axis-8(4) lattice in the same sense EchoDecidable sits at the bottom of axis-8(3).

On composition. The brief asked for "a sensible compositional rule" and flagged that a full product-strategy compose may be awkward without more machinery. I shipped echo-search-postcompose — the genuinely-honest compositional content available without further machinery: a bound-n search witnessing f at y also witnesses g ∘ f at g y, at the same step index and the same bound (the enumerator and queried step have not changed; only the answer has). Sequential / product-strategy composition EchoS enum f b n₁ → EchoS enum' g y n₂ → EchoS (paired) (g ∘ f) y (n₁ * n₂) needs a ℕ × ℕ ↔ ℕ pairing bijection and is deferred to a separate slice; this and a real abstract-machine refinement + a bridge to EchoDecidable are documented in the module's "where next" section.

Invariants

• --safe --without-K on every new module
• No postulates, no funext, no escape pragmas, no believe_me-equivalents
• Clean-worktree Agda build green: agda --safe --without-K All.agda exits 0 (Smoke pins all resolve)

Refs Axis 8(4) — docs/echo-types/taxonomy.md.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "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": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "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": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence