diff --git a/notebooks/09_dogfood_verified_crypto.ipynb b/notebooks/09_dogfood_verified_crypto.ipynb index 688e52b..e426035 100644 --- a/notebooks/09_dogfood_verified_crypto.ipynb +++ b/notebooks/09_dogfood_verified_crypto.ipynb @@ -112,6 +112,22 @@ "cell_type": "markdown", "metadata": {}, "source": [ + "## Dogfood in BOTH directions\n", + "\n", + "Since this lecture was first written the loop closed on the\n", + "provider's side too: the binary gained a `sign` mode, so the\n", + "transparency log's tree heads are now SIGNED by the merkleized\n", + "library - and before every signature the provider runs the same\n", + "Merkle inclusion check an agent runs, on its own signing library's\n", + "leaf, against the very tree it is about to sign. The verdict is\n", + "embedded in the signature block (`signing_provenance`: backend,\n", + "library commit, leaf index, `self_inclusion: verified`,\n", + "certificates 16/16). Lectures 6a/6b walk both sides of this.\n", + "Honesty note unchanged: the library's VERIFY path is\n", + "certificate-covered; the signing path is declared trusted base -\n", + "but it is the attested artifact, not an un-attested third\n", + "implementation.\n", + "\n", "## The post-quantum line, held honestly\n", "\n", "The dogfood loop deliberately does NOT extend to ML-DSA. There is no formally verified ML-DSA implementation in this corpus, and pretending otherwise would poison the whole posture. The hybrid strategy is therefore asymmetric on purpose:\n", diff --git a/notebooks/README.md b/notebooks/README.md index ed3078d..41d7ab1 100644 --- a/notebooks/README.md +++ b/notebooks/README.md @@ -12,6 +12,7 @@ The course teaches: - proof hygiene, - third-party proof-check provider trust, - RFC 9162-style Merkle transparency logs, +- the mirrored provider/agent domain split (6a: one provider builds and dogfood-signs the log; 6b: many agents verify inclusion in ~25 lines, no Lean), - receipt-gated agent consequences (including the R4 wallet gate, now reachable), - split-view defense: STH pinning, consistency enforcement, freshness, monitoring, - dogfood verified cryptography and the honest hybrid post-quantum posture, diff --git a/scripts/build_curriculum_notebooks.py b/scripts/build_curriculum_notebooks.py index bb51a90..82d1fae 100644 --- a/scripts/build_curriculum_notebooks.py +++ b/scripts/build_curriculum_notebooks.py @@ -1831,6 +1831,22 @@ COURSE = { ), md( """ + ## Dogfood in BOTH directions + + Since this lecture was first written the loop closed on the + provider's side too: the binary gained a `sign` mode, so the + transparency log's tree heads are now SIGNED by the merkleized + library - and before every signature the provider runs the same + Merkle inclusion check an agent runs, on its own signing library's + leaf, against the very tree it is about to sign. The verdict is + embedded in the signature block (`signing_provenance`: backend, + library commit, leaf index, `self_inclusion: verified`, + certificates 16/16). Lectures 6a/6b walk both sides of this. + Honesty note unchanged: the library's VERIFY path is + certificate-covered; the signing path is declared trusted base - + but it is the attested artifact, not an un-attested third + implementation. + ## The post-quantum line, held honestly The dogfood loop deliberately does NOT extend to ML-DSA. There is no formally verified ML-DSA implementation in this corpus, and pretending otherwise would poison the whole posture. The hybrid strategy is therefore asymmetric on purpose: @@ -2010,6 +2026,7 @@ The course teaches: - proof hygiene, - third-party proof-check provider trust, - RFC 9162-style Merkle transparency logs, +- the mirrored provider/agent domain split (6a: one provider builds and dogfood-signs the log; 6b: many agents verify inclusion in ~25 lines, no Lean), - receipt-gated agent consequences (including the R4 wallet gate, now reachable), - split-view defense: STH pinning, consistency enforcement, freshness, monitoring, - dogfood verified cryptography and the honest hybrid post-quantum posture,