Integrate skeleton evidence into human review and authenticated trust records #49

Problem

PR #12 adds autoform skeleton, and the agent-review skill explicitly regenerates its evidence from the exact built candidate. Standalone #12 stops at a terminal report, JSON report, proof-free packets, and optional cited passages. Current main does not expose those artifacts through the Obsidian-oriented human-review workflow or rendered site.

The unmerged review stack partly fills that gap:

• Implement skeleton read-backs #39 added read-back cards and rendered review disclosures, but is superseded by Add verified statement-review bundles #40.
• Add verified statement-review bundles #40 adds versioned review bundles, review prepare/record/check, Obsidian-compatible read-back cards, and review-aware rendering.
• Fix #40's review blockers 4 to 6, and the record half of 1 #42 hardens Add verified statement-review bundles #40, but coherent review check snapshots, filesystem races, and authenticated reviewer identity remain incomplete.
• Report semantic PR conflicts and bind reviews to exact candidates #23 separately tracks exact-candidate attestations and semantic PR conflicts.
• render: Lean source links point at the wrong repository in GitHub Codespaces (GITHUB_REPOSITORY trusted outside Actions) #47 notes the related absence of embedded Lean statements on rendered pages.

We should land and complete that work without inventing a second review protocol, while evaluating whether the existing chrisflav/trust ecosystem can supply the dependency UI and portable signed-review layer.

Current implementation direction

#75 now carries the durable review-bundle and policy-marker architecture and supersedes draft #141's removable opt-in statement_hash. It is not yet merge-ready: land #165, rebuild #90 on the combined publication contract, then restack #75. The final design must retain #141's valid requirement that statement approval bind a proof-invariant statement-meaning closure under mandatory versioned policy; deleting an authored field must not disable verification. That closure remains distinct from proof/evidence hashes and from Trust certificates.

Goal

Give an agent and a human reviewer the same exact evidence object:

• the article's Lean declarations;
• the proof-free skeleton packet;
• the cited source passage and locator;
• assumptions and axioms;
• the exact candidate commit, toolchain, schemas, skeleton hash, evidence hash, and review hash;
• an independent read-back and verdict.

The human must be able to reach this from the owning article in Obsidian and the rendered preview. An agent must be able to consume and validate the same bytes. Stale or incomplete evidence must fail closed.

Existing Trust ecosystem to evaluate

• chrisflav/trust: Lean dependency graph/exporter, rendered declarations, marks, and semantic hashes.
• chrisflav/trust-action: toolchain-selected CI export and publication of a static Trust index.
• chrisflav/trust-web: human dependency-graph UI with declaration deep links, marks, and certificate display.
• chrisflav/trust-cli: local issue/sign/verify/publish/fetch/revoke workflow for GPG-backed certificates.
• chrisflav/trust-server: certificate storage, sessions, trust lists, revocation, and federation.

The cheapest useful integration appears to be a static one: publish a Trust index in CI, then add an “Explore dependencies in Trust” link from an Autoform article or review disclosure. Autoform should continue to present its own skeleton packet and cited passage, since those encode the statement-faithfulness question that a declaration graph alone does not answer. This path requires no hosted certificate server.

Signed approvals are a later interoperability step, not a field rename:

• Autoform's declaration hash is SHA-256 over canonical elaborated meaning and an explicit trust boundary. Its evidence_hash binds the exact packet, and its review_hash also binds the article's cited passage.
• Trust's current semantic-v1 is a 16-hex UInt64 hash over a definitional cone and is explicitly proof-relevant. Re-proving a theorem rotates it.
• A Trust Claim has decl, hash, hasher, repo, commit, toolchain, asserted, and note. It does not structurally encode an article, packet digest, source passage, rubric, rejection, or review scope.

Therefore the two hashes must never be treated as equivalent, and an ordinary Trust certificate must not be interpreted as approval that a Lean statement faithfully formalizes an article. Durable certificate integration likely needs a versioned claim extension or a separate Autoform attestation type. A free-form note is not a protocol.

The Trust repositories are young. The core and web READMEs explicitly describe them as experimental, LLM-generated, and not human-reviewed. Toolchain compatibility also needs design: current core targets Lean 4.33.1, while trust-cli and trust-server target Lean 4.32.0. The server README and current route implementation are out of sync, so released/deployed API behavior must be verified before Autoform depends on it.

Proposed delivery

1. Rebase and consolidate Add verified statement-review bundles #40/Fix #40's review blockers 4 to 6, and the record half of 1 #42 onto the final Add autoform skeleton: the trusted surface of a formalized statement #12 contract. Close their remaining snapshot, storage-race, and stale-evidence blockers rather than reimplementing the review bundle.
2. Make each reviewed article link to its exact packet, cited passage, read-back, hashes, and current/stale status in both Obsidian and the rendered site. Generated artifacts remain derived state; the Markdown blueprint remains authoritative.
3. Add an optional Trust-index adapter:
   • publish the exact candidate's index with trust-action or an equivalent pinned invocation;
   • record its revision, schema, toolchain, and URL in the review bundle;
   • deep-link each Lean declaration into trust-web;
   • keep local/offline Autoform review functional when no index or service exists.
4. Write a compatibility note and fixture that compare Autoform's closure/hash semantics with Trust's. Define mismatch behavior explicitly.
5. Design authenticated approval separately. The signed object must bind the exact candidate and Autoform review_hash, identify its rubric and verdict, and be verifiable client-side. If trust-cli/trust-server are reused, the server remains transport and storage rather than the authority.

Implementation may be split after the compatibility decision, but the data model and end-to-end review contract should stay in this tracker.

Acceptance criteria

• From a blueprint article, a human can reach the exact proof-free packet, cited passage, independent read-back, and current review status in Obsidian and the rendered preview.
• The agent-review workflow consumes the same packet bytes and records the same review_hash; there is no agent-only parallel format.
• Review generation validates a fresh Lean build and one coherent candidate snapshot.
• Any change to the candidate commit, article mapping, packet, cited passage, or review testimony invalidates the recorded approval.
• Review cards and generated outputs are published atomically and safely under concurrent edits.
• The native workflow works offline and without trust-server.
• An optional Trust integration can publish or select an exact-revision index and deep-link every mapped declaration in trust-web.
• A documented mapping keeps Autoform hashes, Trust hashes, hashers, schemas, toolchains, and claim scopes distinct.
• Signed approvals are verified locally and bind Autoform's exact review evidence; an unsigned server assertion cannot satisfy the approval gate.
• The bundled example has an end-to-end test covering agent generation, human navigation, drift invalidation, and the optional Trust link.

Non-goals

• Making Trust or a hosted server mandatory for local Autoform use.
• Treating a Trust declaration certificate as source-faithfulness approval without a new explicit claim contract.
• Replacing the Markdown blueprint as the source of truth.
• Reimplementing Trust's dependency graph or certificate federation inside Autoform without a documented incompatibility that requires it.