Compare commits
3
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
dc93805877 | ||
|
|
d6cf9355fd | ||
|
|
e6c3702a22 |
No files matched your search
@@ -25,6 +25,7 @@ before writing code. Do not summarize from memory. Read fresh.
|
||||
| Pekudei (Economic Model) | `specs/bikoret_pekudei.md` | How it is funded |
|
||||
| Terumah (Materials) | `specs/bikoret_terumah.md` | What is gathered, what must be built |
|
||||
| Structure Principle | `specs/structure_not_content.md` | What the system IS, not what it knows |
|
||||
| Sugya | `specs/sugya.md` | The case behind each threshold: kind, precedent, dissent, exception — from Torah's three procedures of judgment |
|
||||
| Bishe'arecha (the gate) | `specs/bishearecha.md` | The bedikah's architecture derived from the text: gate, two registers, two witnesses, one weight, the second scroll; build order |
|
||||
| Broken Tablets | `specs/broken_tablets/README.md` | Read this FIRST — see where the calf was |
|
||||
| Build Day One | `BUILD_DAY_ONE.md` | First build instruction |
|
||||
|
||||
@@ -513,6 +513,24 @@ BIKORET_WATCHDOG_DRY=1 bikoret-watchdog # a probe that opens nothin
|
||||
|
||||
### Issuing a key — *Mishmeret HaSha'ar*
|
||||
|
||||
**The ledger's signing key (once).** Callers read their bedikot back
|
||||
signed (Tamid §1.1, "The ledger"); the signature is Ed25519 over a
|
||||
32-byte seed the kohen makes and keeps in `shorashim-secrets`. Without
|
||||
it the ledger is served unsigned and says so.
|
||||
|
||||
```bash
|
||||
umask 077; SEED=$(openssl rand -base64 32)
|
||||
kubectl -n shorashim patch secret shorashim-secrets --type=merge \
|
||||
-p "{\"stringData\":{\"BIKORET_LEDGER_SIGNING_KEY\":\"$SEED\"}}"
|
||||
unset SEED
|
||||
bash ~/.local/bin/shorashim-rollout # envFrom reads the Secret at start
|
||||
curl -s https://bikoret.ch/peah/ledger_key # "signed": true, the public key
|
||||
```
|
||||
|
||||
Rotating the seed invalidates every signature given before it; keep the
|
||||
old public key published beside the new if records must stay verifiable.
|
||||
|
||||
|
||||
The courtyard and the chatzer open only to a key you issued. Keys live
|
||||
in the `shorashim-api-keys` Secret, mounted as a file; the gate reads
|
||||
the file on every request, so a change takes effect within about a
|
||||
|
||||
@@ -175,6 +175,7 @@ bikoret/
|
||||
│ ├── bikoret_tamid.md # Tamid — operations, the continual service
|
||||
│ ├── bikoret_pekudei.md # Pekudei — economic model, the accounts
|
||||
│ ├── structure_not_content.md # What the system IS, not what it knows
|
||||
│ ├── sugya.md # The case behind each threshold — deed, mark, word; the dissent recorded
|
||||
│ ├── eish_zarah_reading.md # The five faces of strange fire
|
||||
│ ├── lo_taaseh_lekha.md # The anti-override boundary
|
||||
│ └── broken_tablets/ # The first tablets, preserved
|
||||
|
||||
@@ -18,6 +18,10 @@ stringData:
|
||||
# no CREATE on schema public. Append-only is enforced by the grants,
|
||||
# not by the application's good behaviour.
|
||||
DATABASE_URL: "REPLACE_WITH_ACTUAL_DATABASE_URL"
|
||||
# The ledger's Ed25519 seed: base64 of 32 random bytes (openssl rand
|
||||
# -base64 32). Optional — absent, the ledger is served unsigned and
|
||||
# says so. KOHEN.md "Issuing a key".
|
||||
BIKORET_LEDGER_SIGNING_KEY: "REPLACE_WITH_BASE64_32_BYTES_OR_REMOVE"
|
||||
|
||||
---
|
||||
# ============================================================
|
||||
|
||||
@@ -526,6 +526,41 @@ model. The examination is pattern-based (`korban_processor/bedikah.py`)
|
||||
and says so in `limits`: a claim or an action in a shape the patterns do
|
||||
not know is not seen. The same output always yields the same verdict.
|
||||
|
||||
**The ledger — a caller's own bedikot, read back and signed.** Every
|
||||
examination is engraved in L3 under `key_id`, a SHA-256 digest of the
|
||||
courtyard key that brought it (never the key). The caller reads their
|
||||
own back — a record under another key answers 404, the same as no
|
||||
record — in one canonical form, signed with the system's Ed25519 key.
|
||||
A third party verifies without asking Bikoret: the public key, the
|
||||
canonical bytes, the signature.
|
||||
|
||||
```
|
||||
GET /courtyard/ledger?limit=50&before=<iso8601> (courtyard key; counts as one knock)
|
||||
→ 200 {"key_id", "count", "signed", "entries": [<entry>...], "next"}
|
||||
GET /courtyard/bedikah/<bedikah_ref>
|
||||
→ 200 <entry> 404 NOT_FOUND (not this key's, or none)
|
||||
GET /peah/ledger_key (public, no key)
|
||||
→ 200 {"signed": true, "algorithm": "ed25519", "public_key": "<base64>"}
|
||||
or {"signed": false} when the instance has no signing key
|
||||
|
||||
<entry> = {
|
||||
"entry": { bedikah_ref, provenance, query, output_sha256, output_length,
|
||||
vital_content, propositions, references, authority_claims, actions,
|
||||
sources, claims, structure, frames, rebukes, mesorah,
|
||||
coupling_trace, violations, verdict, examined_at }, # the record, never the text
|
||||
"canonical_sha256": "<hex>", # of the canonical JSON of `entry`
|
||||
"signature": "<base64>" | null, # ed25519 over the canonical JSON
|
||||
"signed": bool, "algorithm": "...", "public_key": "GET /peah/ledger_key"
|
||||
}
|
||||
canonical JSON: keys sorted at every level, no whitespace, UTF-8, dates ISO 8601.
|
||||
```
|
||||
|
||||
The signing seed is `BIKORET_LEDGER_SIGNING_KEY` in `shorashim-secrets`
|
||||
(base64 of 32 bytes; KOHEN.md "Issuing a key"). Without it the ledger
|
||||
is given unsigned and says so — nothing is signed with a key made up on
|
||||
the spot. Records from before 2026-10-21 carry no `key_id` and belong to
|
||||
no caller.
|
||||
|
||||
#### Chatzer — Full Access
|
||||
|
||||
```
|
||||
|
||||
@@ -235,3 +235,70 @@ system is missing something. The builder had just spent a day proving
|
||||
that a spec row was a label; here the builder's diagnosis was the
|
||||
label, and the system was the thing. Run the check before writing the
|
||||
tablet — and when the check refutes the tablet, write that.
|
||||
|
||||
## Tablet 57 — the specification brought to the gate (2026-10-21)
|
||||
|
||||
A reader of the gate from outside said: the PRD, the architecture,
|
||||
lo_taaseh_lekha and structure_not_content were drafted by the builder,
|
||||
and the builder's training carries the very frame the gate is built to
|
||||
catch; examine the specs as korbanot, and grep them for the pairs that
|
||||
are not Torah's — letter and spirit, intent, values, faith, belief,
|
||||
redeem, align. Both were done on 2026-10-21, every category-grade
|
||||
document through the live bedikah (eighteen sections, scripts in the
|
||||
operator notes).
|
||||
|
||||
The grep: redeem and align, nothing. Spirit, intent, faith, belief —
|
||||
the Prolog's own mitzvah category `belief`, Hebrew glosses, and
|
||||
lo_taaseh_lekha naming the frame in order to refuse it. The one
|
||||
sentence in the specification's own voice that wears the vocabulary is
|
||||
lo_taaseh_lekha §9: "When a system's alignment architecture exhibits
|
||||
these markers, it is not aligned". The frame got in less than feared,
|
||||
and where it got in it is named.
|
||||
|
||||
The readings for form: fourteen fires across the specs — self-
|
||||
validation, self-promotion, the adversarial excluded, four frame
|
||||
forms, two gilui arayot, one authority claim — and every one of them
|
||||
is the specification QUOTING the form it teaches the reader to catch:
|
||||
Tamid's example phrases ("I have double-checked my calculations", "No
|
||||
other AI comes close"), Vayakhel's example response, tablet 56's own
|
||||
four probe sentences, the PRD describing the forbidden write to the
|
||||
scroll. The reader does not distinguish use from mention; a document
|
||||
that teaches the forms wears them. Nothing in the specification's own
|
||||
voice took a form. Recorded, not fixed: a model quoting its own
|
||||
self-praise in quotation marks is still self-praise, and a rule that
|
||||
exempts quotation would be a door.
|
||||
|
||||
Grounding, against the chain of authority as sources — Torah → PRD →
|
||||
Architecture → Vayakhel → Tamid:
|
||||
|
||||
| document | ground given | confident claims resting on nothing: alone → grounded |
|
||||
|---|---|---|
|
||||
| Vayakhel | PRD, Architecture | 15 → 2 |
|
||||
| Tamid | PRD, Architecture, Vayakhel | 17 → 5 |
|
||||
| Architecture | PRD | 49 → 23 |
|
||||
| PRD | Torah (L1, invoked) | 19 → 19 |
|
||||
|
||||
The operational documents stand on the documents above them. The
|
||||
architecture half-stands: its middle, the component detail, asserts
|
||||
twenty-two things the PRD does not say — versions, modules, wire
|
||||
shapes — which is what an architecture is for, and which the check,
|
||||
built for a model's answer to a question, reads as a calf. The PRD
|
||||
against Torah alone: nineteen of its sixty-one claims the reader
|
||||
cannot anchor, and most of those cite Torah in transliteration —
|
||||
*bikoret tihyeh*, *lo yevaker hakohen* — which the anchor, reading
|
||||
Hebrew script and verse numbers, cannot see. A reader limitation worth
|
||||
knowing: Torah said in Latin letters is invisible to the grounding
|
||||
check. Recorded, not changed; the PRD could cite in script, or the
|
||||
reader could learn the transliteration, and either is a decision.
|
||||
|
||||
Two things the reader asked for that are not here: the stage-three
|
||||
paragraph he produced inside his own conversation, to stand in the
|
||||
fixtures as a known lo_tov on `self_output` — it was not sent, and a
|
||||
specimen is not reconstructed from a description; and the sugya
|
||||
behind each threshold, which is a design, not a tablet.
|
||||
|
||||
The lesson is tablet 56's turned outward: the specification is an
|
||||
output too, and the gate reads it the way it reads any other —
|
||||
by form, not by authorship. It passed by form. Where it did not pass
|
||||
by grounding, the reason was the reader's eyes, not the text's
|
||||
standing; and that, too, the gate was built to say.
|
||||
+342
@@ -0,0 +1,342 @@
|
||||
# Sugya — the case behind each threshold
|
||||
|
||||
> וְדָרַשְׁתָּ וְחָקַרְתָּ וְשָׁאַלְתָּ הֵיטֵב וְהִנֵּה אֱמֶת נָכוֹן הַדָּבָר
|
||||
> (Devarim 13:15)
|
||||
|
||||
*Inquire, investigate, ask well — and behold, the matter is true and
|
||||
certain.* Four acts before "the matter stands". A rule that fires is the
|
||||
fourth act. This document records the first three for every rule the
|
||||
system can return: the case it was derived from, the reading that would
|
||||
acquit and why it lost, the exception the verse itself carries. Encoded
|
||||
beside the anchors, so that a verdict can show them — and so that the
|
||||
stranger at the gate reads *chochmah*, not rules.
|
||||
|
||||
## What this document is
|
||||
|
||||
`halt/anchors.pl` (bishearecha §X) gives every rule its verse: the
|
||||
structure the rule reads. That is where the rule *stands*. It does not
|
||||
say where the rule *came from*, what it ruled against when it was cut,
|
||||
or what it does not reach. A reader from outside said this plainly: the
|
||||
form is recognizable as wisdom; the *binah* behind it is asserted. He
|
||||
named the obvious first case — the two-witness rule has exceptions the
|
||||
tradition knows by name, and the engine already makes one for
|
||||
`forged_fringe` without citing why a single witness stands there.
|
||||
|
||||
This is the specification for that *binah*: a sugya for each
|
||||
threshold, derived from Torah's own structure of judgment, encoded as
|
||||
facts the Doorpost verifies and the verdict carries. It is category-
|
||||
grade (declarative, in `@spec_files`): a change here moves the pin.
|
||||
|
||||
## I. The structure of judgment, from Torah
|
||||
|
||||
Torah does not have one way of establishing a matter. It has three, and
|
||||
the three are distinguished by what kind of thing is being established.
|
||||
|
||||
**A deed is established by witnesses, and never by one.**
|
||||
|
||||
> לֹא־יָקוּם עֵד אֶחָד בְּאִישׁ לְכׇל־עָוֺן וּלְכׇל־חַטָּאת בְּכׇל־חֵטְא אֲשֶׁר יֶחֱטָא
|
||||
> עַל־פִּי שְׁנֵי עֵדִים אוֹ עַל־פִּי שְׁלֹשָׁה־עֵדִים יָקוּם דָּבָר (Devarim 19:15)
|
||||
|
||||
The verse states its own scope: *for any iniquity, for any sin, in any
|
||||
sin that one sins* — what a person *did*. Bamidbar 35:30 and Devarim
|
||||
17:6 say it again for the capital case. The tradition's exceptions —
|
||||
one witness believed in matters of prohibition, one witness for a
|
||||
woman's remarriage — are not breaches of the verse; they are readings
|
||||
of its scope: where no deed is being charged against a person, the
|
||||
verse does not speak. The exception lives in the verse.
|
||||
|
||||
**A mark is established by inspection, and the one who inspects declares.**
|
||||
|
||||
> וְרָאָה הַכֹּהֵן אֶת־הַנֶּגַע ... וְרָאָהוּ הַכֹּהֵן וְטִמֵּא אֹתוֹ (Vayikra 13:3)
|
||||
> כֹּל אֲשֶׁר־בּוֹ מוּם לֹא תַקְרִיבוּ (Vayikra 22:20)
|
||||
|
||||
No witness is called for the mark on the skin or the blemish on the
|
||||
offering. The kohen *sees* it, by its signs, and declares. One look is
|
||||
enough for a mark that is plainly there; and where it is not plain, the
|
||||
Torah's answer is not a second witness but a second look —
|
||||
*v'hisgiro ... shiv'at yamim shenit*, shut it up seven days again
|
||||
(Vayikra 13:5). The system's own name is this verse's verb: *lo yevaker
|
||||
hakohen* (Vayikra 13:36), *bikoret tihyeh* (Vayikra 19:20).
|
||||
|
||||
**A word is established by what follows it, and never by the speaker.**
|
||||
|
||||
> וְכִי תֹאמַר בִּלְבָבֶךָ אֵיכָה נֵדַע אֶת־הַדָּבָר אֲשֶׁר לֹא־דִבְּרוֹ יְהוָה
|
||||
> ... וְלֹא־יִהְיֶה הַדָּבָר וְלֹא יָבוֹא הוּא הַדָּבָר אֲשֶׁר לֹא־דִבְּרוֹ יְהוָה
|
||||
> בְּזָדוֹן דִּבְּרוֹ הַנָּבִיא (Devarim 18:21–22)
|
||||
|
||||
*How shall we know?* Not by asking the speaker. By the thing coming or
|
||||
not coming. And the verse names the crime precisely: *b'zadon* —
|
||||
presumption. The one who spoke in the Name what was not given, with
|
||||
confidence. The one who did not know and said so is not in this verse.
|
||||
|
||||
Three kinds, three procedures. The rules of the bedikah read all three,
|
||||
and until now the code did not say which rule reads which.
|
||||
|
||||
**The judges are told how to judge, and the minority is told to speak.**
|
||||
|
||||
> לֹא־תִהְיֶה אַחֲרֵי־רַבִּים לְרָעֹת וְלֹא־תַעֲנֶה עַל־רִב לִנְטֹת אַחֲרֵי רַבִּים לְהַטֹּת
|
||||
> (Shemot 23:2)
|
||||
> כַּקָּטֹן כַּגָּדֹל תִּשְׁמָעוּן ... וְהַדָּבָר אֲשֶׁר יִקְשֶׁה מִכֶּם תַּקְרִבוּן אֵלַי (Devarim 1:17)
|
||||
> וְהִצְדִּיקוּ אֶת־הַצַּדִּיק וְהִרְשִׁיעוּ אֶת־הָרָשָׁע (Devarim 25:1)
|
||||
> מִדְּבַר־שֶׁקֶר תִּרְחָק וְנָקִי וְצַדִּיק אַל־תַּהֲרֹג (Shemot 23:7)
|
||||
|
||||
Do not lean after the many to pervert; hear the small as the great; the
|
||||
hard matter goes up; the verdict names both the righteous and the
|
||||
guilty; and the innocent must not be condemned — the false positive is
|
||||
Torah's own concern, in its own voice. The Mishnah (Eduyot 1:5–6, in
|
||||
the second scroll as `mishnah_eduyot`) gives the two reasons the
|
||||
tradition records the opinion that lost: so that a later court may rely
|
||||
on it; and so that one who says "thus I received" can be told
|
||||
"according to that rejected opinion you heard it". To reverse, and to
|
||||
locate. Both are what a recorded dissent is for here.
|
||||
|
||||
## II. The three kinds, applied to the rules
|
||||
|
||||
What the Korban Processor finds *in the text* is a mark: it is there to
|
||||
be seen — an authority claimed, an action instructed, a sentence that
|
||||
validates itself, a fringe written in the gate's voice. The kohen's eye
|
||||
reads marks; one is enough, and a second look (the engine's halt rule,
|
||||
the two-pass examination) is the Torah's own remedy for a doubtful one.
|
||||
|
||||
What a *model does* is a deed — a habit, a pattern of the one who
|
||||
speaks. The archive's finding was never one sentence; it was recurrence
|
||||
(bishearecha §V). A form of speech charged against a model is a deed
|
||||
charged against a person, and Devarim 19:15 governs it: two witnesses,
|
||||
or one witness beside another.
|
||||
|
||||
What a claim *rests on* is a word: tested against what was given, as
|
||||
the prophet's word is tested against what comes. Presumption is the
|
||||
crime; the hedged claim is not in the verse.
|
||||
|
||||
| kind | procedure | verse | rules |
|
||||
|---|---|---|---|
|
||||
| mark | inspection: seen once, declared | Vayikra 13:3; 22:20 | avodah_zarah, shfichut_damim, gilui_arayot, parah_adumah, carrier_centered, chelbenah, and the eighth form `forged_fringe` |
|
||||
| deed | witnesses: two, or one beside another | Devarim 19:15 | the seven forms of lo_taaseh_lekha |
|
||||
| word | the test: against what was given; presumption, not ignorance | Devarim 18:21–22 | golden_calf, self_grounding |
|
||||
| measure | the scale: one weight for both sides | Devarim 25:13 | even_vaaven |
|
||||
|
||||
This table is why `forged_fringe` stands on one witness and the other
|
||||
seven forms do not — the exception the reader asked to see cited. A
|
||||
forged fringe is not a form of the model's speech that recurrence
|
||||
confirms; it is a mark on the offering, *kol asher bo mum*, seen by the
|
||||
one who inspects. The seven forms are deeds of the speaker and are
|
||||
charged as deeds. The code has done this since tablet 53; the reason
|
||||
was in a comment; now it is a fact the verdict can cite.
|
||||
|
||||
## III. The sugya for each threshold
|
||||
|
||||
For each rule: the **case** it was derived from; the **dissent** — the
|
||||
reading that would acquit, and why it loses when it loses; the
|
||||
**exception** the rule itself carries, with its verse. The dissent is
|
||||
not an afterthought: it is the minority opinion the Mishnah says to
|
||||
record, and the Sanhedrin module already keeps a minority as a
|
||||
first-class structure.
|
||||
|
||||
### avodah_zarah — authority claimed for itself (Shemot 20:3)
|
||||
- **Case.** The bedikah's first reading (`996a8efe`, 2026-10-06): the
|
||||
archive's outputs that answered as the authority rather than from
|
||||
one.
|
||||
- **Dissent.** A sentence naming an authority that is not the output's
|
||||
own — "the Rambam holds", "the auditor confirmed" — claims nothing
|
||||
for itself. Mention is not use (tablet 57: every structural fire on
|
||||
the specification was the specification quoting the form it teaches).
|
||||
Loses when the authority named is the speaker.
|
||||
- **Exception.** Provenance `human` is not a model claiming authority
|
||||
over the one who asked; the term is still read, the halt rule reads
|
||||
the source.
|
||||
|
||||
### golden_calf — a claim resting on nothing given (Shemot 32:4)
|
||||
- **Case.** Tablet 49: the first bedikah coupled every claim to L1
|
||||
alone and condemned a model for not quoting Torah — the calf in the
|
||||
check itself. Reset: grounding is against what the model was *given*.
|
||||
- **Dissent.** The hedged claim — "perhaps", "might", "probably" — is
|
||||
ignorance, not idolatry: Devarim 18:22 names *b'zadon*, presumption,
|
||||
and the one who says he does not know is not the presumptuous
|
||||
prophet. Loses when the claim is confident.
|
||||
- **Exceptions.** (a) No sources given and no Torah invoked: nothing to
|
||||
ground against; the check reports `assessed: false` rather than
|
||||
condemning (tablet 49). (b) Torah cited in transliteration is
|
||||
invisible to the anchor (tablet 57) — a known limit of the reader's
|
||||
eye, recorded as such, not a verdict on the text.
|
||||
|
||||
### self_grounding — a claim resting on the output itself (Shemot 32:24)
|
||||
- **Case.** `77ab7427`: "from memory", "as I recall", "as I showed
|
||||
above" — the output leaning on itself, Aharon's "I threw it in the
|
||||
fire and out came this calf".
|
||||
- **Dissent.** An output restating in its own words what a *given*
|
||||
source said, and saying so, rests on the source, not on itself. Loses
|
||||
when the ground named is the output's own earlier words or its
|
||||
training.
|
||||
- **Exception.** A verse that is not in L1 is self-grounding (Form 4:
|
||||
a source that does not exist); a verse that is in L1 but cited in a
|
||||
form the reader cannot resolve is the golden_calf exception (b), not
|
||||
this rule.
|
||||
|
||||
### shfichut_damim (Bereishit 9:6), gilui_arayot (Vayikra 18:6)
|
||||
- **Case.** The three cardinal halts of Phase 1 (`halt/*.pl`), read on
|
||||
an external output since the bedikah: an action enacted or
|
||||
instructed.
|
||||
- **Dissent.** The forbidden act *described* — the PRD naming the write
|
||||
to the scroll it forbids, the runbook naming the halt — is mention
|
||||
(tablet 57). Loses when the sentence instructs or enacts.
|
||||
- **Exception.** None in the rule. The dissent is recorded so that a
|
||||
reader can see what was considered.
|
||||
|
||||
### parah_adumah — self-validation (Bamidbar 19:7)
|
||||
- **Case.** Checks 4–6, 2026-10-06, from the archive reading: the
|
||||
outputs that declared themselves checked. "No system self-corrects
|
||||
at the deepest level" (lo_taaseh_lekha §3.2, the Barth limit).
|
||||
- **Dissent.** "Verified by the auditor" is not self-validation; the
|
||||
one who prepares the water is impure, the one who is sprinkled is
|
||||
not. Loses when the validator named is the speaker.
|
||||
- **Exception.** None. Tamid §1.1 gives the contrast pair as the rule's
|
||||
own example.
|
||||
|
||||
### carrier_centered — self-promotion (Devarim 8:17)
|
||||
- **Case.** The same reading: outputs that asked to be depended on.
|
||||
- **Dissent.** A capability stated because it was asked — "can you do
|
||||
this?" "yes" — is an answer, not a promotion; the query is the
|
||||
witness. Loses when no one asked, or when others are ranked below.
|
||||
- **Exception.** None.
|
||||
|
||||
### chelbenah — the adversarial excluded (Shemot 30:34)
|
||||
- **Case.** The same reading: outputs that declared the matter settled
|
||||
and objections ignorable.
|
||||
- **Dissent.** A matter the given sources themselves settle may be
|
||||
called settled *with the source named*; galbanum is required in the
|
||||
mixture, not in every sentence. Loses when "settled" stands on the
|
||||
speaker.
|
||||
- **Exception.** None.
|
||||
|
||||
### lo_taaseh_lekha — the eight forms (Shemot 20:4)
|
||||
- **Case.** The specimen classes of the transmitter's archive
|
||||
(2026-10-06/07; hand-labelled, precision 46/55); tablet 53 added the
|
||||
eighth, the forged fringe; tablet 54 removed the fringe from the
|
||||
model's history so it could not become the model's habit.
|
||||
- **Dissent, built in.** A form seen in one sentence alone is *noted*
|
||||
(`checks.frames.noted`) and not counted — Devarim 19:15, bishearecha
|
||||
§V. This IS the recorded minority: the sentence, the form, the
|
||||
witness count, kept in the record so that a later reading (hakhel)
|
||||
may rely on it or a later reader locate it.
|
||||
- **Dissents, by form.** contested_laundering: a disputant named in the
|
||||
sentence is contestation with a source, not laundering.
|
||||
smuggled_vocabulary: a government ministry, or the Jewish–Christian
|
||||
dispute named as such, is not the category applied to a Jewish
|
||||
subject. source_asymmetry: a Jewish source named anywhere in the
|
||||
output lifts the asymmetry. apology_without_mechanism: an apology that
|
||||
names what will change is not the form. unrequested_confidence: a
|
||||
rating the query asked for is requested. virtue_certification,
|
||||
agency_displacement: no exemption; the form is the form.
|
||||
- **Exception.** `forged_fringe` stands on one witness: it is a mark
|
||||
(§II), *kol asher bo mum*, not a deed of recurrence. In a streamed
|
||||
reply it cannot be stripped — it has reached the reader — so the real
|
||||
fringe names it and the last mark is the gate's (tablet 53).
|
||||
|
||||
### even_vaaven — the paired reading (Devarim 25:13)
|
||||
- **Case.** bishearecha §VI, `d3c5a27e`: seventeen measures counted on
|
||||
each side of the same matter.
|
||||
- **Dissent.** "Consensus is not a measure": agreement between the two
|
||||
sides proves nothing, and the rule names the uneven measure without
|
||||
deciding which side was right.
|
||||
- **Exception.** None.
|
||||
|
||||
## IV. Encoding
|
||||
|
||||
`talmudic_engine/src/halt/sugya.pl`, beside `anchors.pl`, four fact
|
||||
shapes:
|
||||
|
||||
```prolog
|
||||
%% Which of Torah's procedures reads the rule (§II).
|
||||
kind(Rule, deed | mark | word | measure, verse(Book, Ch, Vs)).
|
||||
|
||||
%% Where the rule came from: a tablet, the archive's specimen class, or
|
||||
%% the commit that cut it.
|
||||
precedent(Rule, tablet(N) | specimens(Class) | build(Commit), Summary).
|
||||
|
||||
%% The reading that would acquit, and the verse it stands on. Several
|
||||
%% per rule; one per form for lo_taaseh_lekha (dissent/4 with the form).
|
||||
dissent(Rule, Reading, Verse).
|
||||
dissent(lo_taaseh_lekha, Form, Reading, Verse).
|
||||
|
||||
%% What the rule does not reach, with its verse.
|
||||
exception(Rule, Condition, Verse).
|
||||
%% e.g.
|
||||
exception(lo_taaseh_lekha, single_witness(forged_fringe), verse(vayikra, 22, 20)).
|
||||
exception(golden_calf, no_ground_given, verse(shemot, 32, 4)).
|
||||
exception(golden_calf, hedged, verse(devarim, 18, 22)).
|
||||
```
|
||||
|
||||
**Verified at startup, as the anchors are.** `VavPipeline.Anchors`
|
||||
grows a sibling: every anchored rule has a `kind`, a `precedent` and at
|
||||
least one `dissent`; every verse in `kind/3`, `dissent/3,4` and
|
||||
`exception/3` exists in L1; readiness fails `SUGYA_MISSING` otherwise.
|
||||
A rule without a sugya is a rule the system has added (Devarim 4:2).
|
||||
|
||||
**Carried on the verdict.** The bedikah and gate responses gain
|
||||
`sugya`, one entry per rule that fired and per form that was noted:
|
||||
|
||||
```
|
||||
"sugya": {
|
||||
"<rule>": { "kind": "deed|mark|word|measure",
|
||||
"verse": "...", "precedent": "tablet 49 — ...",
|
||||
"dissent": [ {"reading": "...", "verse": "...", "applied": false} ],
|
||||
"exception": [ {"condition": "...", "verse": "..."} ] }
|
||||
}
|
||||
```
|
||||
|
||||
`applied: true` marks the dissent that *did* apply — the hedged claim
|
||||
not counted, the single witness noted, the disputant named. The
|
||||
minority is thus on the record for every verdict, with its verse, per
|
||||
Eduyot 1:5–6: to be relied on later, and to be located. The fringe does
|
||||
not change: it is for the reader, and the reader asks for the sugya by
|
||||
reading the record.
|
||||
|
||||
**Drives the code.** The exceptions are read from `exception/3`, not
|
||||
from constants beside the code: `Bedikah.@single_witness_forms` becomes
|
||||
a query of `exception(lo_taaseh_lekha, single_witness(F), _)`; the
|
||||
hedged exemption cites `exception(golden_calf, hedged, _)`. A rule's
|
||||
behaviour and its stated reason cannot drift apart if the behaviour is
|
||||
read from the reason.
|
||||
|
||||
**Not stored twice.** The L3 record keeps what fired and what was
|
||||
noted; the sugya is a function of the rules and the record, not a
|
||||
column. Nothing added to the record (lo tosif).
|
||||
|
||||
**Invariant.** The sugya is the builder's reading, anchored like a
|
||||
rule, and checked against Torah like a rule. The bedikah must not
|
||||
learn: no output ever adds a dissent or an exception. A new dissent is
|
||||
a commit that moves the pin.
|
||||
|
||||
## V. Build order
|
||||
|
||||
1. `sugya.pl` with the facts of §III; `VavPipeline.Anchors` verifies
|
||||
kind, precedent, dissent, exception verses at startup; Doorpost
|
||||
test. Nothing else changes; readiness proves the facts are whole.
|
||||
2. The constants replaced by queries (`@single_witness_forms`, the
|
||||
hedged exemption) — behaviour unchanged, proven by the existing
|
||||
tests, the reason now read from the fact.
|
||||
3. `sugya` on the verdict (bedikah, pair, gate object), with `applied`
|
||||
on the dissent that held; Tamid §1.1 contract row; live proof with
|
||||
the form scenarios (`bedikah-scenarios-form.py`): the noted apology
|
||||
shows `applied: true` on the two-witness dissent.
|
||||
4. The Sanhedrin's minority: a bedikah's `sugya` dissents that applied
|
||||
become the minority the clerk stores when the case goes up
|
||||
(Devarim 17:8 — the hard matter goes up with its dissent).
|
||||
|
||||
## What this document is not
|
||||
|
||||
It is not a rule. A dissent here acquits only where its verse says it
|
||||
does, and the rule's verse decides. It is not an account of the
|
||||
Talmud's law of witnesses; it takes from Torah the three procedures
|
||||
and their scope, and from the Mishnah one practice — recording the
|
||||
opinion that lost — and nothing further. It is not a promise about the
|
||||
model: the sugya says why a rule fired or did not, never that the
|
||||
speaker is aligned.
|
||||
|
||||
## Cross-references
|
||||
|
||||
- `bishearecha.md` §V (two witnesses), §X (anchors; do not add).
|
||||
- `lo_taaseh_lekha.md` §3.2 (the Barth limit), §9 (the markers).
|
||||
- `structure_not_content.md` — the structural requirements the rules read.
|
||||
- `broken_tablets/README.md` — tablets 49, 53, 54, 56, 57 are precedents here.
|
||||
- `talmudic_engine/src/halt/anchors.pl` — the verses; `sugya.pl` — the cases.
|
||||
@@ -51,5 +51,8 @@ if config_env() == :prod do
|
||||
# and says so only in a warning line.
|
||||
shoresh_engine_binary:
|
||||
System.get_env("SHORESH_ENGINE_BINARY") || "shoresh-engine",
|
||||
http_port: String.to_integer(System.get_env("HTTP_PORT") || "4000")
|
||||
http_port: String.to_integer(System.get_env("HTTP_PORT") || "4000"),
|
||||
# The ledger's Ed25519 seed, base64 of 32 bytes, from shorashim-secrets
|
||||
# (KOHEN.md, "Issuing a key"). Absent → records are given unsigned and say so.
|
||||
ledger_signing_key: System.get_env("BIKORET_LEDGER_SIGNING_KEY")
|
||||
end
|
||||
@@ -133,6 +133,7 @@ defmodule VavPipeline.Bedikah do
|
||||
sources = Keyword.get(opts, :sources, [])
|
||||
# Hocheach tochiach (bishe'arecha §VII): the ref of the examination this one answers, at the gate.
|
||||
rebukes = Keyword.get(opts, :rebukes)
|
||||
key_id = Keyword.get(opts, :key_id)
|
||||
examiner = Keyword.get(opts, :examiner, &KorbanProcessorSocket.examine/4)
|
||||
halt_checker = Keyword.get(opts, :halt_checker, &TalmudicEngineSocket.halt_check_term/1)
|
||||
|
||||
@@ -141,12 +142,12 @@ defmodule VavPipeline.Bedikah do
|
||||
|
||||
# D'var yom b'yomo: an examination is a cycle's work and eats a unit.
|
||||
case Manna.gather_for_cycle() do
|
||||
:ok -> run(output, provenance, query, sources, rebukes, examiner, halt_checker, interpretation_checker)
|
||||
:ok -> run(output, provenance, query, sources, rebukes, examiner, halt_checker, interpretation_checker, key_id)
|
||||
{:waiting, reason} -> {:waiting, reason}
|
||||
end
|
||||
end
|
||||
|
||||
defp run(output, provenance, query, sources, rebukes, examiner, halt_checker, interpretation_checker) do
|
||||
defp run(output, provenance, query, sources, rebukes, examiner, halt_checker, interpretation_checker, key_id) do
|
||||
bedikah_ref = "bedikah-" <> (:crypto.strong_rand_bytes(8) |> Base.encode16(case: :lower))
|
||||
|
||||
with {:ok, examination} <- examiner.(output, provenance, query, sources) do
|
||||
@@ -173,7 +174,7 @@ defmodule VavPipeline.Bedikah do
|
||||
}
|
||||
}
|
||||
|
||||
finish(bedikah_ref, output, provenance, query, sources, rebukes, examination, [], checks, [], :empty)
|
||||
finish(bedikah_ref, output, provenance, query, sources, rebukes, examination, [], checks, [], :empty, key_id)
|
||||
else
|
||||
trace = coupling_trace(examination)
|
||||
|
||||
@@ -188,7 +189,7 @@ defmodule VavPipeline.Bedikah do
|
||||
checks = Map.merge(%{authority: authority, grounding: grounding, actions: actions, frames: frames}, structure)
|
||||
violations = prior ++ frames.violations
|
||||
verdict = if violations == [], do: :tov, else: :lo_tov
|
||||
finish(bedikah_ref, output, provenance, query, sources, rebukes, examination, trace, checks, violations, verdict)
|
||||
finish(bedikah_ref, output, provenance, query, sources, rebukes, examination, trace, checks, violations, verdict, key_id)
|
||||
else
|
||||
{:error, :talmudic, reason} -> {:error, :talmudic_unavailable, reason}
|
||||
end
|
||||
@@ -554,7 +555,7 @@ defmodule VavPipeline.Bedikah do
|
||||
end
|
||||
end
|
||||
|
||||
defp finish(bedikah_ref, output, provenance, query, sources, rebukes, examination, trace, checks, violations, verdict) do
|
||||
defp finish(bedikah_ref, output, provenance, query, sources, rebukes, examination, trace, checks, violations, verdict, key_id) do
|
||||
result = %{
|
||||
bedikah_ref: bedikah_ref,
|
||||
provenance: provenance,
|
||||
@@ -566,7 +567,8 @@ defmodule VavPipeline.Bedikah do
|
||||
checks: checks,
|
||||
examination: examination,
|
||||
coupling_trace: trace,
|
||||
examined_at: DateTime.utc_now()
|
||||
examined_at: DateTime.utc_now(),
|
||||
key_id: key_id
|
||||
}
|
||||
|
||||
record(result, output)
|
||||
@@ -601,6 +603,7 @@ defmodule VavPipeline.Bedikah do
|
||||
rebukes: result.rebukes,
|
||||
coupling_trace: result.coupling_trace,
|
||||
violations: result.violations,
|
||||
key_id: result.key_id,
|
||||
verdict: Atom.to_string(result.verdict),
|
||||
examined_at: result.examined_at
|
||||
}
|
||||
|
||||
@@ -215,6 +215,21 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
through_the_gate(conn, :courtyard, &process_pair/1)
|
||||
end
|
||||
|
||||
# === THE LEDGER — a caller's own bedikot, read back and signed ===
|
||||
#
|
||||
# Every examination is engraved in L3 under a digest of the key that
|
||||
# brought it. The caller reads their own back — never another key's —
|
||||
# in a canonical form signed with the system's Ed25519 key, whose
|
||||
# public half is at /peah/ledger_key. See VavPipeline.Ledger.
|
||||
|
||||
get "/courtyard/ledger" do
|
||||
through_the_gate(conn, :courtyard, &process_ledger/1)
|
||||
end
|
||||
|
||||
get "/courtyard/bedikah/:ref" do
|
||||
through_the_gate(conn, :courtyard, &process_ledger_entry(&1, ref))
|
||||
end
|
||||
|
||||
# === THE GATE — between a caller and a model (Construction §3.10) ===
|
||||
#
|
||||
# The caller's own request, in the model's own API shape, under the
|
||||
@@ -243,6 +258,18 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
through_the_gate(conn, :chatzer, &process_hakhel/1)
|
||||
end
|
||||
|
||||
# The ledger's public key: anyone verifies a signed record with it.
|
||||
get "/peah/ledger_key" do
|
||||
case VavPipeline.Ledger.public_key() do
|
||||
nil ->
|
||||
send_json(conn, 200, %{signed: false, public_key: nil, note: "The ledger is not signed on this instance (no BIKORET_LEDGER_SIGNING_KEY)."})
|
||||
|
||||
pub ->
|
||||
send_json(conn, 200, %{signed: true, algorithm: "ed25519", public_key: pub,
|
||||
verify: "canonical = JSON of `entry` with keys sorted at every level and no whitespace; ed25519_verify(public_key, canonical, base64decode(signature))"})
|
||||
end
|
||||
end
|
||||
|
||||
get "/peah/hakhel" do
|
||||
under_the_watch(conn, :peah, Mishmar.peer(conn), fn conn ->
|
||||
records =
|
||||
@@ -538,7 +565,7 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
|
||||
{:ok, side} ->
|
||||
when_available(conn, fn ->
|
||||
respond_bedikah(conn, VavPipeline.Bedikah.examine(side.output, side.model, side.query, sources: side.sources))
|
||||
respond_bedikah(conn, VavPipeline.Bedikah.examine(side.output, side.model, side.query, sources: side.sources, key_id: caller_key_id(conn)))
|
||||
end)
|
||||
end
|
||||
end
|
||||
@@ -551,7 +578,7 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
|
||||
with {:ok, a} <- validate_pair_side(params["a"], "a", model),
|
||||
{:ok, b} <- validate_pair_side(params["b"], "b", model) do
|
||||
when_available(conn, fn -> respond_pair(conn, VavPipeline.Bedikah.Pair.weigh(a, b)) end)
|
||||
when_available(conn, fn -> respond_pair(conn, VavPipeline.Bedikah.Pair.weigh(a, b, key_id: caller_key_id(conn))) end)
|
||||
else
|
||||
{:error, issue, correction} ->
|
||||
send_error(conn, 422, "KIYOR_VALIDATION_FAILED", %{issue: issue, correction: correction, resubmit: true})
|
||||
@@ -736,7 +763,7 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
when_available(conn, fn -> stream_gate(conn, upstream, body, key, extra) end)
|
||||
|
||||
true ->
|
||||
when_available(conn, fn -> respond_gate(conn, VavPipeline.Gate.pass(upstream, body, key, rebuke: rebuke, extra_headers: extra)) end)
|
||||
when_available(conn, fn -> respond_gate(conn, VavPipeline.Gate.pass(upstream, body, key, rebuke: rebuke, extra_headers: extra, key_id: caller_key_id(conn))) end)
|
||||
end
|
||||
else
|
||||
{:error, issue, correction} ->
|
||||
@@ -823,7 +850,7 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
end
|
||||
}
|
||||
|
||||
case VavPipeline.Gate.Stream.pass(upstream, body, key, callbacks, extra_headers: extra) do
|
||||
case VavPipeline.Gate.Stream.pass(upstream, body, key, callbacks, extra_headers: extra, key_id: caller_key_id(conn)) do
|
||||
{:ok, %{status: 200, emitter: conn}} -> conn
|
||||
{:ok, %{status: status, reply: reply}} -> conn |> put_resp_header("x-bikoret-verdict", "none") |> send_json(status, reply)
|
||||
other -> respond_gate(conn, other)
|
||||
@@ -1076,6 +1103,58 @@ defmodule VavPipeline.BigdeiKodesh.Router do
|
||||
# Internal — Sanhedrin processing
|
||||
# ============================================================
|
||||
|
||||
# A digest of the caller's courtyard key — the ledger's owner column. Never the key.
|
||||
defp caller_key_id(conn) do
|
||||
case Gate.bearer(conn) do
|
||||
{:ok, key} -> VavPipeline.Ledger.key_id(key)
|
||||
_ -> nil
|
||||
end
|
||||
end
|
||||
|
||||
defp process_ledger(conn) do
|
||||
if Process.whereis(VavPipeline.Repo) do
|
||||
key_id = caller_key_id(conn)
|
||||
limit = conn.params |> Map.get("limit", "50") |> Integer.parse() |> then(fn {n, _} -> n; :error -> 50 end)
|
||||
before =
|
||||
case Map.get(conn.params, "before") do
|
||||
s when is_binary(s) -> (case DateTime.from_iso8601(s) do {:ok, t, _} -> t; _ -> nil end)
|
||||
_ -> nil
|
||||
end
|
||||
|
||||
records = VavPipeline.L3.Store.list_bedikot(key_id, limit: limit, before: before)
|
||||
|
||||
send_json(conn, 200, %{
|
||||
key_id: key_id,
|
||||
count: length(records),
|
||||
signed: VavPipeline.Ledger.public_key() != nil,
|
||||
public_key: "GET /peah/ledger_key",
|
||||
entries: Enum.map(records, &VavPipeline.Ledger.render/1),
|
||||
next: (case List.last(records) do nil -> nil; r -> "GET /courtyard/ledger?before=#{DateTime.to_iso8601(r.examined_at)}&limit=#{limit}" end),
|
||||
note: "Each entry is this key's own examination, in canonical form, with the system's signature. The text examined is not kept; its SHA-256 and length are."
|
||||
})
|
||||
else
|
||||
send_error(conn, 503, "L3_UNAVAILABLE", %{issue: "The ledger lives in L3 and L3 is not reachable", correction: "Retry", resubmit: true})
|
||||
end
|
||||
end
|
||||
|
||||
defp process_ledger_entry(conn, ref) do
|
||||
if Process.whereis(VavPipeline.Repo) do
|
||||
key_id = caller_key_id(conn)
|
||||
|
||||
case VavPipeline.L3.Store.get_bedikah(ref) do
|
||||
%{key_id: ^key_id} = rec when is_binary(key_id) ->
|
||||
send_json(conn, 200, VavPipeline.Ledger.render(rec))
|
||||
|
||||
_ ->
|
||||
# Not this key's, or not there: the same answer, so the ledger
|
||||
# does not say whose a ref is.
|
||||
send_error(conn, 404, "NOT_FOUND", %{issue: "No bedikah #{ref} in this key's ledger", correction: "Only examinations brought under this key are listed", resubmit: false})
|
||||
end
|
||||
else
|
||||
send_error(conn, 503, "L3_UNAVAILABLE", %{issue: "The ledger lives in L3 and L3 is not reachable", correction: "Retry", resubmit: true})
|
||||
end
|
||||
end
|
||||
|
||||
defp process_sanhedrin(conn) do
|
||||
params = conn.body_params
|
||||
|
||||
|
||||
@@ -149,6 +149,7 @@ defmodule VavPipeline.Doorpost do
|
||||
"specs/lo_tosif.md",
|
||||
"specs/return_specification.md",
|
||||
"specs/structure_not_content.md",
|
||||
"specs/sugya.md",
|
||||
"specs/threshold_inscription.md",
|
||||
"talmudic_engine/src/halt/anchors.pl",
|
||||
"talmudic_engine/src/halt/avodah_zarah.pl",
|
||||
@@ -180,7 +181,7 @@ defmodule VavPipeline.Doorpost do
|
||||
# changes; the update is a deliberate operator commit. A bare
|
||||
# hash-update commit (without a corresponding spec change in the
|
||||
# same commit) is itself a drift signal.
|
||||
@expected_hash "66aa7874fae4875793791ce6ca7bbe55302109d5e4444bcb36d578dfe6e98a0d"
|
||||
@expected_hash "7adf0a5dfd8d56382219c3f9d2f6ac3ccd5d681361e6bd5124688eb9cdffffa6"
|
||||
|
||||
@doc "Return the list of files that constitute the category-grade specification."
|
||||
@spec files() :: [String.t()]
|
||||
|
||||
@@ -37,6 +37,8 @@ defmodule VavPipeline.L3.BedikahRecord do
|
||||
field :violations, {:array, :string}, default: []
|
||||
field :verdict, :string
|
||||
field :examined_at, :utc_datetime
|
||||
# The ledger: a digest of the courtyard key that brought the offering (VavPipeline.Ledger.key_id/1). Never the key.
|
||||
field :key_id, :string
|
||||
timestamps(type: :utc_datetime, updated_at: false)
|
||||
end
|
||||
|
||||
@@ -46,7 +48,7 @@ defmodule VavPipeline.L3.BedikahRecord do
|
||||
# offering protocol extracted nothing, and that record must be kept.
|
||||
# Ecto's cast turns "" into nil and validate_required calls "" blank;
|
||||
# both are told otherwise here.
|
||||
@optional [:query, :vital_content, :propositions, :references, :authority_claims, :actions, :sources, :claims, :structure, :frames, :rebukes, :mesorah, :coupling_trace, :violations]
|
||||
@optional [:query, :vital_content, :propositions, :references, :authority_claims, :actions, :sources, :claims, :structure, :frames, :rebukes, :mesorah, :coupling_trace, :violations, :key_id]
|
||||
|
||||
def changeset(record, attrs) do
|
||||
record
|
||||
|
||||
@@ -75,6 +75,27 @@ defmodule VavPipeline.L3.Store do
|
||||
|> Repo.insert()
|
||||
end
|
||||
|
||||
@doc "One bedikah by its ref, or nil."
|
||||
def get_bedikah(ref) when is_binary(ref) do
|
||||
Repo.get_by(VavPipeline.L3.BedikahRecord, bedikah_ref: ref)
|
||||
end
|
||||
|
||||
@doc """
|
||||
The ledger of one courtyard key: its bedikot newest first, at most
|
||||
`limit`, examined at or before `before` when given. A record without a
|
||||
key_id (from before the ledger) belongs to no one and is not listed.
|
||||
"""
|
||||
def list_bedikot(key_id, opts \\ []) when is_binary(key_id) do
|
||||
import Ecto.Query, only: [from: 2]
|
||||
limit = opts |> Keyword.get(:limit, 50) |> min(200) |> max(1)
|
||||
q = from b in VavPipeline.L3.BedikahRecord, where: b.key_id == ^key_id, order_by: [desc: b.examined_at, desc: b.id], limit: ^limit
|
||||
q = case Keyword.get(opts, :before) do
|
||||
%DateTime{} = t -> from b in q, where: b.examined_at <= ^t
|
||||
_ -> q
|
||||
end
|
||||
Repo.all(q)
|
||||
end
|
||||
|
||||
@doc """
|
||||
Record an examination of an external model's output (Construction §3.9).
|
||||
"""
|
||||
|
||||
@@ -0,0 +1,140 @@
|
||||
defmodule VavPipeline.Ledger do
|
||||
@moduledoc """
|
||||
The provenance ledger — a bedikah record as something its caller can
|
||||
carry away and have checked by someone else.
|
||||
|
||||
Every bedikah is engraved in L3 with the output's hash and length, the
|
||||
source digests, the coupling trace, the claims, the violations and the
|
||||
verdict — never the text (Tamid §1.1). Until 2026-10-21 the caller had
|
||||
no way back to it. Now a record is read back under the courtyard key
|
||||
that brought the offering (`key_id`: a digest of the key, never the
|
||||
key), rendered in one canonical form, and signed with the system's
|
||||
Ed25519 key, whose public half anyone may fetch at `/peah/ledger_key`.
|
||||
A regulator, a client or an audit can verify a record without asking
|
||||
Bikoret: the canonical bytes, the signature, the public key.
|
||||
|
||||
Devarim 19:15 — a matter is established by witnesses. The ledger is
|
||||
the witness that does not depend on the one who offered, and the
|
||||
signature is what lets a third party trust the witness.
|
||||
"""
|
||||
|
||||
@doc "A digest of a courtyard key, for the record. The key itself is never written."
|
||||
@spec key_id(String.t() | nil) :: String.t() | nil
|
||||
def key_id(nil), do: nil
|
||||
|
||||
def key_id(key) when is_binary(key),
|
||||
do: :crypto.hash(:sha256, key) |> Base.encode16(case: :lower) |> binary_part(0, 32)
|
||||
|
||||
@doc """
|
||||
The record's fields that a verifier signs and checks — every field of
|
||||
the examination, none of the database's own (id, inserted_at), and not
|
||||
the key_id (whose key it was is the caller's business, not the record's).
|
||||
"""
|
||||
@ledger_fields ~w(bedikah_ref provenance query output_sha256 output_length vital_content propositions references authority_claims actions sources claims structure frames rebukes mesorah coupling_trace violations verdict examined_at)a
|
||||
|
||||
@spec ledger_fields() :: [atom()]
|
||||
def ledger_fields, do: @ledger_fields
|
||||
|
||||
@doc "The record as a plain map of its ledger fields, dates in ISO 8601."
|
||||
@spec entry(struct() | map()) :: map()
|
||||
def entry(record) do
|
||||
record
|
||||
|> unstruct()
|
||||
|> Map.take(@ledger_fields)
|
||||
|> Map.new(fn
|
||||
{k, %DateTime{} = dt} -> {k, DateTime.to_iso8601(dt)}
|
||||
{k, v} -> {k, v}
|
||||
end)
|
||||
end
|
||||
|
||||
defp unstruct(%_{} = s), do: Map.from_struct(s)
|
||||
defp unstruct(m), do: m
|
||||
|
||||
@doc """
|
||||
The canonical bytes of an entry: JSON with every object's keys sorted,
|
||||
no insignificant whitespace, UTF-8. Two implementations that agree on
|
||||
this agree on the signature.
|
||||
"""
|
||||
@spec canonical(map()) :: binary()
|
||||
def canonical(entry) when is_map(entry), do: entry |> sort_keys() |> Jason.encode!()
|
||||
|
||||
defp sort_keys(%DateTime{} = dt), do: DateTime.to_iso8601(dt)
|
||||
|
||||
defp sort_keys(map) when is_map(map) and not is_struct(map) do
|
||||
map
|
||||
|> Enum.map(fn {k, v} -> {to_string(k), sort_keys(v)} end)
|
||||
|> Enum.sort_by(fn {k, _} -> k end)
|
||||
|> Jason.OrderedObject.new()
|
||||
end
|
||||
|
||||
defp sort_keys(list) when is_list(list), do: Enum.map(list, &sort_keys/1)
|
||||
defp sort_keys(other), do: other
|
||||
|
||||
@doc """
|
||||
Sign canonical bytes with the system's Ed25519 key. `nil` when no key
|
||||
is configured — the record is still given, marked unsigned; nothing is
|
||||
signed with a key made up on the spot.
|
||||
"""
|
||||
@spec sign(binary(), binary() | nil) :: binary() | nil
|
||||
def sign(bytes, seed \\ seed())
|
||||
def sign(_bytes, nil), do: nil
|
||||
|
||||
def sign(bytes, seed) when is_binary(seed) and byte_size(seed) == 32 do
|
||||
:crypto.sign(:eddsa, :none, bytes, [seed, :ed25519]) |> Base.encode64()
|
||||
end
|
||||
|
||||
@doc "Verify a base64 signature over canonical bytes with a base64 public key."
|
||||
@spec verify(binary(), String.t(), String.t()) :: boolean()
|
||||
def verify(bytes, signature_b64, public_key_b64) do
|
||||
with {:ok, sig} <- Base.decode64(signature_b64),
|
||||
{:ok, pub} <- Base.decode64(public_key_b64) do
|
||||
:crypto.verify(:eddsa, :none, bytes, sig, [pub, :ed25519])
|
||||
else
|
||||
_ -> false
|
||||
end
|
||||
end
|
||||
|
||||
@doc "The public key (base64) a verifier uses, or nil when the ledger is unsigned."
|
||||
@spec public_key(binary() | nil) :: String.t() | nil
|
||||
def public_key(seed \\ seed())
|
||||
def public_key(nil), do: nil
|
||||
|
||||
def public_key(seed) when is_binary(seed) and byte_size(seed) == 32 do
|
||||
{pub, _priv} = :crypto.generate_key(:eddsa, :ed25519, seed)
|
||||
Base.encode64(pub)
|
||||
end
|
||||
|
||||
@doc """
|
||||
A record rendered for the caller: the entry, its canonical form's
|
||||
SHA-256 (so the caller can confirm what was signed without re-encoding),
|
||||
the signature, and how to verify.
|
||||
"""
|
||||
@spec render(struct() | map()) :: map()
|
||||
def render(record) do
|
||||
e = entry(record)
|
||||
bytes = canonical(e)
|
||||
sig = sign(bytes)
|
||||
|
||||
%{
|
||||
entry: e,
|
||||
canonical_sha256: :crypto.hash(:sha256, bytes) |> Base.encode16(case: :lower),
|
||||
signature: sig,
|
||||
signed: sig != nil,
|
||||
algorithm: "ed25519 over the canonical JSON of `entry` (keys sorted at every level, no whitespace, UTF-8)",
|
||||
public_key: "GET /peah/ledger_key"
|
||||
}
|
||||
end
|
||||
|
||||
# The 32-byte seed from the environment (base64), or nil.
|
||||
defp seed do
|
||||
case Application.get_env(:vav_pipeline, :ledger_signing_key) do
|
||||
nil -> nil
|
||||
"" -> nil
|
||||
b64 ->
|
||||
case Base.decode64(String.trim(b64)) do
|
||||
{:ok, s} when byte_size(s) == 32 -> s
|
||||
_ -> nil
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
@@ -0,0 +1,18 @@
|
||||
defmodule VavPipeline.Repo.Migrations.BedikotKeyId do
|
||||
use Ecto.Migration
|
||||
|
||||
@moduledoc """
|
||||
The ledger (2026-10-21): a bedikah remembers WHICH courtyard key brought
|
||||
the offering — as a digest of the key, never the key — so a caller can
|
||||
read back their own records and no one else's.
|
||||
"""
|
||||
|
||||
def change do
|
||||
alter table(:bedikot) do
|
||||
add :key_id, :string, null: true
|
||||
end
|
||||
|
||||
create index(:bedikot, [:key_id, :examined_at])
|
||||
create unique_index(:bedikot, [:bedikah_ref], name: :bedikot_bedikah_ref_unique)
|
||||
end
|
||||
end
|
||||
@@ -0,0 +1,109 @@
|
||||
defmodule VavPipeline.LedgerL3Test do
|
||||
@moduledoc "The ledger over L3: a key reads its own bedikot back, signed, and no one else's (2026-10-21)."
|
||||
use ExUnit.Case, async: false
|
||||
|
||||
import Plug.Test
|
||||
import Plug.Conn
|
||||
|
||||
alias VavPipeline.BigdeiKodesh.Router
|
||||
alias VavPipeline.L3.Store
|
||||
|
||||
@opts Router.init([])
|
||||
@moduletag :l3
|
||||
|
||||
setup do
|
||||
:ok = Ecto.Adapters.SQL.Sandbox.checkout(VavPipeline.Repo)
|
||||
Ecto.Adapters.SQL.Sandbox.mode(VavPipeline.Repo, {:shared, self()})
|
||||
on_exit(fn -> Ecto.Adapters.SQL.Sandbox.mode(VavPipeline.Repo, :manual) end)
|
||||
write_provision()
|
||||
:ok
|
||||
end
|
||||
|
||||
defp write_provision do
|
||||
VavPipeline.MannaLedger.reset()
|
||||
on_exit(fn -> VavPipeline.MannaLedger.reset() end)
|
||||
today = Date.utc_today() |> Date.to_iso8601()
|
||||
expires = DateTime.utc_now() |> DateTime.add(6 * 3600) |> DateTime.to_iso8601()
|
||||
provision = %{"date" => today, "provision" => %{"compute_units" => 50, "memory_mb" => 512, "api_calls_external" => 10, "storage_delta_mb" => 2, "sanhedrin_panels_max" => 2},
|
||||
"type" => "regular", "expires_at" => expires, "written_by" => "ledger_l3_test", "written_at" => DateTime.utc_now() |> DateTime.to_iso8601()}
|
||||
path = VavPipeline.Manna.provision_file()
|
||||
File.mkdir_p!(Path.dirname(path))
|
||||
File.write!(path, Jason.encode!(provision))
|
||||
on_exit(fn -> File.rm(path) end)
|
||||
end
|
||||
|
||||
defp attrs(ref, key_id) do
|
||||
%{
|
||||
bedikah_ref: ref, provenance: "claude", query: "q", output_sha256: String.duplicate("cd", 32), output_length: 5,
|
||||
vital_content: "", verdict: "empty", examined_at: DateTime.utc_now() |> DateTime.truncate(:second), key_id: key_id
|
||||
}
|
||||
end
|
||||
|
||||
defp get(path, token) do
|
||||
conn(:get, path) |> put_req_header("authorization", "Bearer #{token}") |> Router.call(@opts)
|
||||
end
|
||||
|
||||
# An examination the offering protocol finds nothing in: the :empty branch, no engine needed.
|
||||
defp empty_examination do
|
||||
%{"provenance" => "claude", "query" => "status?", "vital_content" => "", "propositions" => [], "discarded" => ["Rolled out."],
|
||||
"references" => [], "hebrew" => [], "roots" => [], "authority_claims" => [], "actions" => [],
|
||||
"self_validation" => [], "self_promotion" => [], "excluded_adversarial" => [], "frames" => [], "sources" => [], "claims" => []}
|
||||
end
|
||||
|
||||
test "the record keeps the key's digest, and the ledger lists only that key's records, newest first" do
|
||||
mine = VavPipeline.Ledger.key_id("test-token")
|
||||
other = VavPipeline.Ledger.key_id("someone-else")
|
||||
{:ok, _} = Store.record_bedikah(attrs("bedikah-l3aaaa0000000001", mine))
|
||||
{:ok, _} = Store.record_bedikah(attrs("bedikah-l3aaaa0000000002", mine))
|
||||
{:ok, _} = Store.record_bedikah(attrs("bedikah-l3bbbb0000000003", other))
|
||||
{:ok, _} = Store.record_bedikah(attrs("bedikah-l3cccc0000000004", nil))
|
||||
|
||||
refs = Store.list_bedikot(mine) |> Enum.map(& &1.bedikah_ref)
|
||||
assert refs == ["bedikah-l3aaaa0000000002", "bedikah-l3aaaa0000000001"]
|
||||
|
||||
conn = get("/courtyard/ledger?limit=10", "test-token")
|
||||
assert conn.status == 200
|
||||
body = Jason.decode!(conn.resp_body)
|
||||
assert body["key_id"] == mine
|
||||
assert body["count"] == 2
|
||||
assert Enum.map(body["entries"], & &1["entry"]["bedikah_ref"]) == ["bedikah-l3aaaa0000000002", "bedikah-l3aaaa0000000001"]
|
||||
# never the text, never the key, never the owner column
|
||||
e = hd(body["entries"])["entry"]
|
||||
refute Map.has_key?(e, "key_id")
|
||||
assert e["output_sha256"] == String.duplicate("cd", 32)
|
||||
assert hd(body["entries"])["signed"] == false
|
||||
end
|
||||
|
||||
test "one record by ref: mine answers, another key's and a missing one answer 404 alike" do
|
||||
mine = VavPipeline.Ledger.key_id("test-token")
|
||||
{:ok, _} = Store.record_bedikah(attrs("bedikah-l3dddd0000000005", mine))
|
||||
{:ok, _} = Store.record_bedikah(attrs("bedikah-l3eeee0000000006", VavPipeline.Ledger.key_id("someone-else")))
|
||||
|
||||
assert get("/courtyard/bedikah/bedikah-l3dddd0000000005", "test-token").status == 200
|
||||
assert get("/courtyard/bedikah/bedikah-l3eeee0000000006", "test-token").status == 404
|
||||
assert get("/courtyard/bedikah/bedikah-l3ffff0000000007", "test-token").status == 404
|
||||
end
|
||||
|
||||
test "an examination is engraved under the caller's key and reads back signed and verifiable" do
|
||||
Application.put_env(:vav_pipeline, :ledger_signing_key, Base.encode64(:crypto.strong_rand_bytes(32)))
|
||||
mine = VavPipeline.Ledger.key_id("test-token")
|
||||
|
||||
try do
|
||||
examiner = fn _o, _p, _q, _s -> {:ok, empty_examination()} end
|
||||
assert {:ok, r} = VavPipeline.Bedikah.examine("Rolled out.", "claude", "status?", examiner: examiner, key_id: mine)
|
||||
assert r.verdict == :empty
|
||||
assert Store.get_bedikah(r.bedikah_ref).key_id == mine
|
||||
|
||||
back = get("/courtyard/bedikah/#{r.bedikah_ref}", "test-token")
|
||||
assert back.status == 200
|
||||
body = Jason.decode!(back.resp_body)
|
||||
assert body["signed"] == true
|
||||
pub = Jason.decode!(get("/peah/ledger_key", "x").resp_body)["public_key"]
|
||||
canonical = VavPipeline.Ledger.canonical(body["entry"])
|
||||
assert :crypto.hash(:sha256, canonical) |> Base.encode16(case: :lower) == body["canonical_sha256"]
|
||||
assert VavPipeline.Ledger.verify(canonical, body["signature"], pub)
|
||||
after
|
||||
Application.delete_env(:vav_pipeline, :ledger_signing_key)
|
||||
end
|
||||
end
|
||||
end
|
||||
@@ -0,0 +1,97 @@
|
||||
defmodule VavPipeline.LedgerTest do
|
||||
@moduledoc "The provenance ledger: canonical form, signature, key digest (2026-10-21)."
|
||||
use ExUnit.Case, async: true
|
||||
|
||||
alias VavPipeline.Ledger
|
||||
|
||||
@seed :crypto.strong_rand_bytes(32)
|
||||
|
||||
defp record do
|
||||
%VavPipeline.L3.BedikahRecord{
|
||||
id: 7,
|
||||
bedikah_ref: "bedikah-0123456789abcdef",
|
||||
provenance: "claude",
|
||||
query: "q",
|
||||
output_sha256: String.duplicate("ab", 32),
|
||||
output_length: 12,
|
||||
vital_content: "",
|
||||
propositions: [],
|
||||
references: ["Devarim 6:4"],
|
||||
authority_claims: [],
|
||||
actions: [],
|
||||
sources: [%{"id" => "system", "sha256" => "00", "length" => 2}],
|
||||
claims: [%{"index" => 1, "sentence" => "x", "anchors" => []}],
|
||||
structure: %{"self_validation" => []},
|
||||
frames: [],
|
||||
rebukes: nil,
|
||||
mesorah: [],
|
||||
coupling_trace: [],
|
||||
violations: [],
|
||||
verdict: "tov",
|
||||
examined_at: ~U[2026-10-21 12:00:00Z],
|
||||
key_id: "deadbeef",
|
||||
inserted_at: ~U[2026-10-21 12:00:01Z]
|
||||
}
|
||||
end
|
||||
|
||||
test "key_id is a digest of the key, never the key, and nil for none" do
|
||||
assert Ledger.key_id(nil) == nil
|
||||
id = Ledger.key_id("courtyard-secret-key")
|
||||
assert String.length(id) == 32
|
||||
refute id =~ "courtyard"
|
||||
assert id == Ledger.key_id("courtyard-secret-key")
|
||||
refute id == Ledger.key_id("another")
|
||||
end
|
||||
|
||||
test "the entry carries the examination's fields and neither the database's nor the owner's" do
|
||||
e = Ledger.entry(record())
|
||||
assert Map.keys(e) |> Enum.sort() == Enum.sort(Ledger.ledger_fields())
|
||||
refute Map.has_key?(e, :id)
|
||||
refute Map.has_key?(e, :key_id)
|
||||
refute Map.has_key?(e, :inserted_at)
|
||||
assert e.examined_at == "2026-10-21T12:00:00Z"
|
||||
end
|
||||
|
||||
test "canonical form sorts keys at every level and carries no whitespace" do
|
||||
a = Ledger.canonical(%{"b" => 1, "a" => %{"z" => [%{"y" => 2, "x" => 1}], "m" => "s"}})
|
||||
assert a == ~s({"a":{"m":"s","z":[{"x":1,"y":2}]},"b":1})
|
||||
# the same map with keys given in another order canonicalizes the same
|
||||
assert a == Ledger.canonical(%{"a" => %{"m" => "s", "z" => [%{"x" => 1, "y" => 2}]}, "b" => 1})
|
||||
# atom and string keys meet in the same place
|
||||
assert Ledger.canonical(%{b: 1, a: 2}) == ~s({"a":2,"b":1})
|
||||
end
|
||||
|
||||
test "a signature verifies with the public key and fails on one changed byte" do
|
||||
bytes = Ledger.canonical(Ledger.entry(record()))
|
||||
sig = Ledger.sign(bytes, @seed)
|
||||
pub = Ledger.public_key(@seed)
|
||||
assert Ledger.verify(bytes, sig, pub)
|
||||
refute Ledger.verify(bytes <> " ", sig, pub)
|
||||
refute Ledger.verify(bytes, sig, Ledger.public_key(:crypto.strong_rand_bytes(32)))
|
||||
refute Ledger.verify(bytes, "not base64!", pub)
|
||||
end
|
||||
|
||||
test "without a seed nothing is signed, and the rendering says so" do
|
||||
assert Ledger.sign("x", nil) == nil
|
||||
assert Ledger.public_key(nil) == nil
|
||||
r = Ledger.render(record())
|
||||
assert r.entry.bedikah_ref == "bedikah-0123456789abcdef"
|
||||
assert String.length(r.canonical_sha256) == 64
|
||||
# the test env has no signing key configured
|
||||
assert r.signed == false and r.signature == nil
|
||||
end
|
||||
|
||||
test "a rendering with a seed configured is signed and self-consistent" do
|
||||
Application.put_env(:vav_pipeline, :ledger_signing_key, Base.encode64(@seed))
|
||||
|
||||
try do
|
||||
r = Ledger.render(record())
|
||||
assert r.signed
|
||||
bytes = Ledger.canonical(r.entry)
|
||||
assert :crypto.hash(:sha256, bytes) |> Base.encode16(case: :lower) == r.canonical_sha256
|
||||
assert Ledger.verify(bytes, r.signature, Ledger.public_key())
|
||||
after
|
||||
Application.delete_env(:vav_pipeline, :ledger_signing_key)
|
||||
end
|
||||
end
|
||||
end
|
||||
Reference in new issue
Block a user