saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-04 20:03:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: 'You hold the ruler' - customer-facing requirements-card box on the LTL page + WALLET.md

Browse source 
The lecture-11 framing where customers actually land: the allowed-axioms
list as a card the customer owns and can rewrite; verdicts re-derived
against THEIR copy; stricter card => itemized gap => relax / walk away /
grow the supply. Links to lecture 11 for the executable walk-through.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-07 22:32:27 +02:00
parent ea80c99244
commit 2f67f14054
2 changed files with 37 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
WALLET.md
View file

@ -98,6 +98,22 @@ custody wallet that cannot show its evidence has no business existing.
`--trusted-provider` is **required**: you must name whose *observations*
you are consuming. You are never asked to trust their verdicts.
### You hold the ruler
The allowed-axioms lists the gate checks against are a **requirements
card** that ships in *your* tooling ([the ed25519
profile](src/pacta/profiles/ed25519.py)) — small enough to read over
coffee, re-derivable from the attested repos' own docs and check
scripts, and replaceable with a card you write yourself from first
principles. Verdicts are re-derived against *your* copy, name by name;
the provider's labels are ignored. If your card is stricter than
today's supply (e.g. "SHA-512 itself proven"), the gap is itemized and
your options are honest: accept a named line item, walk away, or prove
the missing piece and enter it into the log — *if your ruler is
stricter than our supply, your ruler is our roadmap.* The full
walk-through is
[lecture 11](notebooks/11_the_customers_eye_view.ipynb).
---
## Quickstart

21
provider/src/pacta_provider/webdocs.py
View file

@ -249,6 +249,27 @@ the content hash) and build it yourself — compiler and build are declared trus
until the reproducible-builds program (R5) lands. Every attestation carries its full
residual-risk list. Honesty about the boundary is the product.</div>
<h2>You hold the ruler</h2>
<div class="card">The list of assumptions a certificate is <em>allowed</em> to rest on
is not something this site hands you at verification time — it is a
<strong>requirements card</strong> that lives in <em>your</em> tooling, on
<em>your</em> disk, and that you can read in five minutes or rewrite from first
principles: Lean's three foundational axioms, plus — for the signature tiers only —
named placeholders for SHA-512 and the wire format. Your tooling ignores this
operator's pass/fail labels entirely and re-derives every verdict by comparing the
attestation's <em>observed</em> axiom list against <em>your</em> card, name by name.
The operator is trusted to copy down what the proof kernel printed — never to
interpret it.</div>
<div class="card">A card you write yourself will match this log's supply
<strong>exactly</strong> — and that is engineered, not coincidence: the corpus was
shrunk until every remaining axiom justifies its existence. If your card is
<em>stricter</em> (say: "SHA-512 itself must be proven"), there is nothing here to
negotiate — the gap is itemized, never blurred, and you have three honest options:
accept a <em>named</em> line item, walk away, or prove the missing piece and enter it
into this same log. <strong>If your ruler is stricter than our supply, your ruler is
our roadmap.</strong> (The full walk-through is lecture&nbsp;11 in the
<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">course</a>.)</div>
<h2>The paper</h2>
<div class="card"><a href="{base}/paper"><strong>LTL: Lean Transparency Log</strong></a>
(PDF, 4 pages) — the design in full: the trust model (observations, never verdicts),