1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
;;; Copyright (c) 2026 Nicholas Vermeulen
;;; SPDX-License-Identifier: AGPL-3.0-or-later
;; cert.lisp — verifiable certificate exchange (pure Lisp library).
;;
;; mingjian proves a log by REPLAYING it; cert.lisp generalizes that to
;; proof EXCHANGE across hosts. An issuer bundles a claim — a function's
;; SOURCE, a property's SOURCE, and the finite DOMAINS it was checked over —
;; runs the gates locally, and SIGNS the canonical serialization (Ed25519). A
;; receiver on another machine does TWO independent things:
;; 1. verifies the signature — the bundle came UNCHANGED from a trusted
;; issuer (the serialization is INJECTIVE, so mutating any claim field
;; changes the signed bytes and the signature fails);
;; 2. RE-CHECKS the claim's HONESTY itself — check-effects (pure?) then
;; check-exhaustive over the declared domains. The issuer's signature is
;; NOT taken as evidence that the claim holds; the receiver re-runs it.
;;
;; THE LOAD-BEARING DISTINCTION: a validly-signed bundle from a trusted issuer
;; is STILL refused if the receiver's own re-run finds a counterexample or an
;; effect. The signature proves PROVENANCE (this exact claim came from this
;; key); the re-run proves HONESTY (the claim actually holds); they are
;; separate, and honesty is delegated to no one. (Negative control in the
;; golden: a correctly-signed WRONG bundle is refused by the re-run.)
;;
;; WHAT A CERT DOES *NOT* GIVE YOU: the receiver still accepts the issuer's
;; CHOICE of subject, sources, and DOMAINS. A trusted key can sign a true-but-
;; trivial claim (a tiny domain, a weak invariant); the re-run confirms only
;; that the stated claim holds on the stated domain, never that it is a strong
;; or meaningful claim. `certified` = "the receiver independently re-verified
;; THIS claim over THIS declared finite domain, and the signature proves it
;; arrived unchanged from a trusted issuer" — never "trusted"/"safe"/"correct".
;; The mingjian anchor limit holds: a private-key holder can sign a false
;; claim, and only the receiver's re-run — never the signature — catches it.
;;
;; No new interpreter code: check-effects + check-exhaustive are the gates,
;; ed25519-keygen/sign/verify are the anchor, eval-string turns SOURCE (text,
;; because a bundle crosses hosts as text) into a callable.
;; ── Canonical serialization = the exact bytes that get signed ──────────────
;; INJECTIVE by construction: every atom is TYPE-TAGGED and LENGTH-PREFIXED
;; (s/y/n = string/symbol/number then <char-count>:<chars>; L<count>: for a
;; list; bt/bf for a boolean). No content — embedded quotes, spaces, digits,
;; ":" — can forge a field boundary, and no two data of different type collide
;; (the tag separates them). Distinct data always encode to distinct strings,
;; so there is no fragile "subset" to remember. (We never parse this back;
;; injectivity of the ENCODER is all a signature preimage needs.)
;; The signed message = a DOMAIN-SEPARATION tag + the canonical claim. The tag
;; ("cert-v1") means a cert signature can never be replayed as an evolve
;; receipt (a different tag) even under the same key. Nothing about the issuer
;; or signature is inside it (a signature can't cover itself).
;; ── The gates (run by BOTH issuer and receiver — identical, so they can't
;; drift): the candidate must be pure, then satisfy the invariant on every
;; declared domain point. 'ok, or (refused <tag> <detail>). A malformed or
;; unparseable source RAISES inside eval-string / apply — caught here and
;; normalized to (refused error ...) so a garbage bundle can never crash the
;; receiver, only be refused. ───────────────────────────────────────────────
;; ── Issue: gate locally, then sign. The issuer VOUCHES ONLY for what passed
;; its own gates — cert-make refuses to sign a bundle that doesn't verify. ───
;; secret-hex is the Ed25519 private seed (32 bytes hex); it never leaves the
;; issuer. Returns a bundle (data) or the gate refusal.
;; ── Bundle accessors ───────────────────────────────────────────────────────
;; ── Verify: the receiver's job. `trusted` is a list of issuer public keys
;; (they arrive out-of-band, over a channel you already trust). Returns
;; (certified subject domain-size N) or (refused <tag> ...). ─────────────────
;; Static-first order: a malformed / untrusted / bad-signature bundle is
;; refused BEFORE its source is ever eval'd by the re-run. A missing field
;; (cert-field → #f) or empty domains is (refused malformed) — an empty domain
;; product is a vacuous claim, so it is rejected rather than "verified" over
;; nothing.
; a valid signature does NOT save a
; bundle whose re-run fails.