diff --git a/docs/echos/BOT-PROMPT.adoc b/docs/echos/BOT-PROMPT.adoc new file mode 100644 index 0000000..2a7839c --- /dev/null +++ b/docs/echos/BOT-PROMPT.adoc @@ -0,0 +1,80 @@ +// SPDX-License-Identifier: MPL-2.0 += Investigation brief: echo-based fidelity for autoformalisation + +Paste the section below into a bot tied to the `echo-types` repository on +branch `arena/93ae4ce1-echo-types`. Work only on that branch. + +== Prompt + +____ +You are investigating whether echo types (fibres with witnesses) can help +assure fidelity of autoformalisation: the step where an informal or source +statement is translated into a formal statement that a proof checker accepts. + +Context you must read first: + +* `docs/echos/README.adoc` (scope, status, ground truth) +* `docs/echos/FIDELITY-FIBRE-DESIGN.adoc` (design and what is not claimed) +* `proofs/agda/EchoFidelity.agda` (draft model, NOT yet type-checked) +* `proofs/agda/EchoEpistemic.agda` (existing knowledge/observation model) +* `docs/CLAIMS_AUDIT.adoc` (how this repo audits its own claims) + +Core question: if the fibre of each target atom is traceable to its source +atoms, does that help assure that the translation preserved what matters? + +Tasks, in order: + +1. *Type-check the draft.* Attempt to type-check `EchoFidelity.agda` with the + same Agda version and standard library the repo uses (see + `echo-types.agda-lib` and the version noted in `EXPLAINME.adoc`). Fix only + errors that are syntactic or type-level. Do not change claims. Report the + exact errors and fixes. If Agda is unavailable, say so and stop this task. + +2. *Test the claims in the design note.* For each claim in + `FIDELITY-FIBRE-DESIGN.adoc` section "What the types buy", state whether + it is (a) enforced by the type, (b) a definitional consequence, or + (c) only a convention. Give evidence for each. + +3. *Check the direction example.* Confirm that `cmp 4 5 ≡ weaker` reflects the + stated convention (smaller parameter = stronger claim). Then construct one + more example of your own from a different domain (for example, a hypothesis + that is added, or a bound that is tightened) and encode it. Say whether the + convention generalises or needs more structure. + +4. *Stress-test the checker/auditor split.* Write down a concrete pair of + translations with identical target atoms and different fibres. Show that a + checker's observation is identical, and that the auditor can tell them + apart. Then describe one case where the auditor's view is still not enough. + +5. *Survey the surrounding tools (read-only).* In the sibling repositories + `echidna`, `echidnabot`, and `proof-burrower`, identify any place where a + source-to-target mapping could be recorded. Use the existing content-ID + scheme (`echidna/src/rust/ids.rs`) as a candidate. Do not modify those + repositories. Report file paths and line references. + +6. *Propose, do not implement, a persistence format.* Sketch the minimal record + needed to store a fibre alongside a proof receipt. Keep it to fields and + invariants. Put it in `docs/echos/FIBRE-RECORD-PROPOSAL.adoc`. + +Rules: + +* Label every statement as VERIFIED (you ran it), READ (you read the code), or + INFERRED (reasoning only). Do not present inferred results as verified. +* Do not claim fidelity is established. The output is about structure and + assurance layers, not about whether any particular theorem is correct. +* Do not wire `EchoFidelity.agda` into `All.agda` or `Smoke.agda` unless every + check passes and the user asks for it. +* Keep changes to `docs/echos/` and `proofs/agda/EchoFidelity.agda` unless a + task requires otherwise. Explain any other file you touch. +* Commit to `arena/93ae4ce1-echo-types` only. + +Deliverable: a short report at `docs/echos/INVESTIGATION-REPORT.adoc` with one +section per task, the labels above, and a list of open questions. +____ + +== Notes for the person running the bot + +* The bot's output is a structured exploration, not a verdict on any + autoformalisation result. +* If the bot reports that Agda cannot be run, treat task 1 as open, and do not + let later tasks rely on the draft compiling. diff --git a/docs/echos/FIDELITY-FIBRE-DESIGN.adoc b/docs/echos/FIDELITY-FIBRE-DESIGN.adoc new file mode 100644 index 0000000..d77f929 --- /dev/null +++ b/docs/echos/FIDELITY-FIBRE-DESIGN.adoc @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: MPL-2.0 += Fibre accounting for autoformalisation: design note +:toc: preamble + +== The object + +For one translation step, let `SA` be the source atoms (hypotheses, constants, +bounds, quantifier structure, conclusion) and `TA` the target atoms of the +formal statement. A translation is a total map + +[source] +---- +account : SA -> Verdict TA +Verdict TA = mapped t | dropped reason +---- + +The fibre of a target atom `t` is the set of source atoms whose verdict is +`mapped t`. This is the echo-type reading: `Fibre t = Σ s. account s ≡ mapped t`. + +== What the types buy + +* *No silent loss.* `account` is total, so every source atom has a verdict. + An atom that vanishes from the translation is a type error, not an + oversight. +* *Fabrication is a fibre question.* A target atom with an empty fibre has no + source in this step. It may be a helpful lemma or an invented one. The + record makes that visible; it does not decide which. +* *Checker blindness is explicit.* Two translations with the same target atoms + look identical to a checker, whatever their fibres say. The auditor needs the + fibre to tell them apart. + +== Direction, not just equality + +Equality of atoms is too coarse. The video's case is a numeric parameter: the +paper needs four, the formal version needs five. Both are "a bound", but the +formal one is a weaker claim. `EchoFidelity.agda` encodes this as a direction +check: `cmp 4 5 ≡ weaker`. + +The same idea extends to hypotheses (a target with an extra hypothesis is +weaker) and to conclusions (a target with a stronger conclusion is stronger +and needs proof, not just a check). + +== What is not claimed + +* The fibre does not show that matched atoms have the same meaning. A `Nat` + standing in for `ℝ` maps cleanly and is still wrong. +* The fibre cannot see what the source left implicit. Unstated assumptions + need a reader. +* A trace produced by the translating process can be wrong in the same way as + the translation. Its independence is what gives it value. +* Round-trip back-translation is a useful heuristic, not a proof of equivalence. + +== Layers of assurance + +[cols="1,2,2"] +|=== +|Layer |What it checks |Decidable? + +|1. Accounting |Every source atom has a verdict; drops carry reasons |Yes +|2. Structural diff |Hypothesis set, quantifier order, numeric parameters, + direction of each change |Yes, for the syntactic fragment +|3. Back-translation |Target re-read as informal text, compared with source |No; + needs review +|4. Axiom audit |No postulates or assumptions added on the target side |Yes +|5. Human reading |Implicit assumptions and meaning |No +|=== + +Layers 1, 2, and 4 are cheap and should run on every step. Layers 3 and 5 are +where judgement is needed. The design aim is that judgement is spent on the +few atoms the structural layers flag, not on the whole statement. + +== Open questions + +* Which fragment of statements admits a complete structural diff? Derivative + counts and bounds are plausible; full first-order equivalence is not. +* How should a fibre be persisted alongside a proof receipt so the link from + source to check is durable? Candidate: content IDs from `echidna/src/rust/ids.rs`. +* Who writes the trace? Options: the translator (cheap, weak), a separate + model (medium), code that diffs both sides (strong for structure only). diff --git a/docs/echos/README.adoc b/docs/echos/README.adoc new file mode 100644 index 0000000..ee0f561 --- /dev/null +++ b/docs/echos/README.adoc @@ -0,0 +1,65 @@ +// SPDX-License-Identifier: MPL-2.0 += Echos: fidelity exploration for autoformalisation +:toc: preamble + +== Scope + +This directory is the exploration space for using echo types (fibres with +witnesses) to reason about fidelity of translation steps, in particular +autoformalisation: informal or source statement → formal statement → checked +proof. + +It is exploratory. Nothing here is a claimed result. The question is: + +____ +If the fibre of each target atom is traceable back to its source atoms, does +that help assure that the translation preserved what matters? +____ + +== Status + +[cols="2,1,3"] +|=== +|Item |Status |Where + +|Fibre accounting model (Agda) |DRAFT, unverified |`proofs/agda/EchoFidelity.agda` +|Design note (what fibres do and do not give) |Draft |`FIDELITY-FIBRE-DESIGN.adoc` +|Investigation brief for a repo-tied bot |Ready to use |`BOT-PROMPT.adoc` +|Wired into `All.agda` / `Smoke.agda` |No |Deliberately not wired until checked +|=== + +== Ground truth from the surrounding tools + +Checked on 2026-10-11 against the sibling repositories (read-only): + +* `echidna`: proof identity and goal identity hash the submitted goal text + (`src/rust/proof_encoding.rs`). Nothing in the trust path records a + source-to-target mapping. Axiom detection is pattern-based + (`src/rust/corpus/agda.rs`). +* `echidna`: `src/rust/ids.rs` provides a stable content-ID scheme (UUIDv8 over + canonical JSON) that could hold atom identifiers. +* `proof-burrower`: goal matching is Jaccard over signature tokens, described + in the code as crude (`crates/burrower-core/src/ranking.rs`). + +So the fibre trace described here does not exist in those tools yet. + +== Principles + +1. *Accounting is decidable; fidelity is not.* Every source atom must end up + mapped or explicitly dropped with a reason. That is a structural check. It + is not evidence that the meanings agree. +2. *The checker sees only the target.* A proof checker cannot observe + fidelity. Fidelity needs an observer that sees both sides. +3. *Traces need an independent author.* A trace written by the same process + that translated can share its errors. Prefer a structural diff run by code. +4. *Record, don't assume.* A dropped or strengthened atom is information, not + an error to hide. + +== Files + +* `proofs/agda/EchoFidelity.agda`: fibre accounting, checker vs auditor + observation, and a direction check for a numeric parameter (the 4-vs-5 case). +* `FIDELITY-FIBRE-DESIGN.adoc`: the design note, with what is and is not + claimed. +* `BOT-PROMPT.adoc`: a prompt for a bot tied to this repository to carry out + the investigation. diff --git a/proofs/agda/EchoFidelity.agda b/proofs/agda/EchoFidelity.agda new file mode 100644 index 0000000..c6bd9b6 --- /dev/null +++ b/proofs/agda/EchoFidelity.agda @@ -0,0 +1,106 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- +-- STATUS: DRAFT, NOT YET TYPE-CHECKED. Agda was not available in the +-- authoring environment. Before relying on this module, run +-- agda proofs/agda/EchoFidelity.agda +-- and fix any errors. It is deliberately NOT imported from All.agda or +-- Smoke.agda until it has been checked. +-- +-- Purpose: a small model of an autoformalisation step as a fibre record. +-- Every source atom (hypothesis, constant, bound, conclusion) receives a +-- verdict: mapped to a target atom, or dropped with a recorded reason. +-- The types enforce that nothing is silently lost. They do NOT establish +-- semantic fidelity; see docs/echos/FIDELITY-FIBRE-DESIGN.adoc. + +module EchoFidelity where + +open import Agda.Builtin.String using (String) +open import Data.Empty using (⊥) +open import Data.List.Base using (List) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Product.Base using (Σ; _,_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +------------------------------------------------------------------------ +-- Verdicts for a single source atom. +------------------------------------------------------------------------ + +data Verdict (TA : Set) : Set where + mapped : TA → Verdict TA + dropped : String → Verdict TA -- reason must be recorded + +------------------------------------------------------------------------ +-- A translation step: a total accounting of source atoms. +------------------------------------------------------------------------ + +record Translation (SA TA : Set) : Set where + field + source-atoms : List SA + target-atoms : List TA + -- Totality: every source atom gets a verdict. This is the + -- "nothing silently lost" constraint, enforced by the type. + account : SA → Verdict TA + +open Translation public + +------------------------------------------------------------------------ +-- Fibres: the source atoms that a given target atom traces back to. +-- A fibre is a Σ-type of source atoms together with a proof that the +-- source atom is mapped to that target atom. +------------------------------------------------------------------------ + +Fibre : {SA TA : Set} → Translation SA TA → TA → Set +Fibre T t = Σ _ (λ s → account T s ≡ mapped t) + +-- A target atom with an empty fibre has no source: it is fabricated +-- relative to this step. Stated here as the definition of "fabricated"; +-- deciding it for an arbitrary translation needs decidable equality. +Fabricated : {SA TA : Set} → Translation SA TA → TA → Set +Fabricated T t = Fibre T t → ⊥ + +------------------------------------------------------------------------ +-- Checker observation vs auditor observation. +-- The proof checker (Lean, Agda, Coq) sees only the target side. The +-- auditor sees the whole translation, including the fibre. +------------------------------------------------------------------------ + +checker-obs : {SA TA : Set} → Translation SA TA → List TA +checker-obs T = target-atoms T + +-- Two translations that agree on the target side are indistinguishable +-- to the checker, whatever their fibres say. +same-target-same-checker-obs : + {SA TA : Set} (T T' : Translation SA TA) → + target-atoms T ≡ target-atoms T' → + checker-obs T ≡ checker-obs T' +same-target-same-checker-obs T T' eq = eq + +------------------------------------------------------------------------ +-- Direction check for a numeric parameter, using the 4-vs-5 example. +-- Convention: the parameter k means "to control the output, you need +-- k more derivatives on the input". A smaller k is a stronger claim. +------------------------------------------------------------------------ + +data Direction : Set where + same stronger weaker : Direction + +-- cmp paper target: `stronger` means the target claims more than the +-- paper, `weaker` means it claims less. +cmp : ℕ → ℕ → Direction +cmp zero zero = same +cmp zero (suc _) = weaker +cmp (suc _) zero = stronger +cmp (suc m) (suc n) = cmp m n + +-- The video's case: paper says 4, Lean needs 5. The Lean statement is +-- weaker, so the composed result is not the paper's result. +lemma-8-6-check : cmp 4 5 ≡ weaker +lemma-8-6-check = refl + +-- Sanity cases. +cmp-same : cmp 4 4 ≡ same +cmp-same = refl + +cmp-stronger : cmp 5 4 ≡ stronger +cmp-stronger = refl