From 479a2b9482ea283f9811cb8dd95fd216ead9f64a Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 30 May 2026 10:12:39 +0100
Subject: [PATCH] fix(hypatia): scope-narrow code_safety/agda_postulate alert
 on Exploratory module via inline allow directive
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds a file-level `-- hypatia: allow code_safety/agda_postulate --` directive
in the first 20 lines of `EchoImageFactorizationPropPostulated.agda` so the
Hypatia scanner stops re-raising alert #101 ("Agda postulate assumes without
proof -- potential soundness hole") on the module.

Rationale
=========

The flagged postulates (`Trunc-pos`, `∣_∣-pos`, `is-prop-pos`, `rec-pos`) are
the deliberate scoped TruncInterface DEMONSTRATION shipped by PR #153 / #155:

  * Propositional truncation `∥_∥` cannot be constructed in `--safe --without-K`
    without HITs (Cubical Agda) or `--rewriting`. The repo's flake pins
    `agda-stdlib v2.3` only — no cubical lib. The four postulates are the
    standard (-1)-truncation laws asserted-not-proved, which is the SAME
    discipline the in-file docstring describes ("the postulates assert that
    propositional truncation exists and satisfies its standard laws — they
    do not prove the existence; they assume it").
  * Classification: Exploratory (per `docs/echo-types/echo-kernel-note.adoc`).
    The module lives OUTSIDE the kernel cone, outside `proofs/agda/All.agda`,
    and is already exempt from `tools/check-guardrails.sh` via the
    `EXPLORATORY_EXEMPT` allowlist landed in `ea46e09` (PR #155).
  * The load-bearing `EchoImageFactorizationProp` (base) remains
    `--safe --without-K` with zero postulates; this consumer is the
    demonstration that the parametric `TruncInterface` slot is plug-in usable.

Preferred over `.hypatia-ignore`
================================

Per Hypatia's own scanner-hygiene guidance (`lib/hypatia/scanner_suppression.ex`
+ hypatia/CLAUDE.md §"When you need to suppress a real finding"), the preference
order is: fix > inline directive > `.hypatia-ignore` > baseline. An inline
directive scoped to this single file is the right knob:

  * Lives next to the postulates it justifies — the rationale is self-documenting.
  * Does not introduce a new repo-level `.hypatia-ignore` for one entry.
  * File-level scope per the directive matcher's `:max_header_lines = 20`
    default; covers every postulate in this file but no others elsewhere.

Verification
============

`agda -i proofs/agda proofs/agda/EchoImageFactorizationPropPostulated.agda`
typechecks clean (the directive is an Agda line comment); upstream modules
(`EchoImageFactorizationProp`, `EchoTotalCompletion`,
`EchoOrthogonalFactorizationSystem`, `EchoFiberBridge`, `Echo`) check
through unchanged.

The full `--safe --without-K` kernel suite (`proofs/agda/All.agda` +
`proofs/agda/Smoke.agda`) is unaffected — this file is already outside
both.

Honest scope (what this PR does NOT do)
=======================================

This PR does not discharge the postulates. Discharging requires either
adding Cubical Agda to the flake + a sibling `--cubical` module that
realises `Trunc` as a HIT, or moving to an axiom-permitting profile — both
substantial design decisions flagged in `CLAUDE.md` §"Plan for the next
Claude" item 3 (image-factorisation earn-back) and explicitly out of scope
for the alert-management cleanup.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 proofs/agda/EchoImageFactorizationPropPostulated.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/proofs/agda/EchoImageFactorizationPropPostulated.agda b/proofs/agda/EchoImageFactorizationPropPostulated.agda
index 90f8dab..74c4890 100644
--- a/proofs/agda/EchoImageFactorizationPropPostulated.agda
+++ b/proofs/agda/EchoImageFactorizationPropPostulated.agda
@@ -1,5 +1,7 @@
 {-# OPTIONS --without-K #-}
 
+-- hypatia: allow code_safety/agda_postulate -- ∥_∥ cannot be constructed in --safe --without-K without HITs / Cubical; the four postulates below are the scoped, documented TruncInterface demonstration. Exploratory per docs/echo-types/echo-kernel-note.adoc; guardrail-exempted in tools/check-guardrails.sh; base EchoImageFactorizationProp remains --safe --without-K with zero postulates.
+
 -- Postulated-truncation consumer for `EchoImageFactorizationProp`.
 --
 -- ## Purpose