docs: substrate-not-blockchain manifesto#9
Merged
Conversation
Long-form derivation of the substrate/application inversion that has been load-bearing in commit messages but never written down: ProvekIt is the substrate of which blockchains are applications, not the other way around. Five-step argument from subjective-state/objective-correctness through Curry-Howard, body-opacity, per-producer sovereignty, to forward- compatibility through the substrate/application seam. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Warning Rate limit exceeded
To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (1)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Review rate limit: 0/1 reviews remaining, refill in 2 minutes and 43 seconds.Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 055b1a2f98
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| If you accept this framing, the developer move is direct: stop asking "which chain do I publish to?" and start asking "what discipline am I asserting on the bodies I sign?" | ||
|
|
||
| `provekit witness` is the operational surface. You build a binary, hash it, mint a `.proof` bundle whose `binaryCid` pins the artifact and whose discharges carry whatever evidence your discipline requires, then sign and ship the pair. The verifier hashes what it received, looks up the bundle, walks the chain under its policy, emits a report. The report is itself a memento another verifier can take as evidence. |
There was a problem hiding this comment.
provekit witness workflow claim
This sentence presents provekit witness as a complete artifact-production flow (minting a .proof bundle, pinning binaryCid, then signing/shipping), but the current CLI implementation does not do that: in implementations/rust/provekit-cli/src/cmd_witness.rs the success path is still a TODO that only prints “memento would be” and exits. As written, users following this launch doc will try a workflow that is not yet implemented, so this should be revised to match current behavior (or gated as future/planned).
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
This PR adds a new launch document that frames ProvekIt as a general-purpose protocol substrate rather than a blockchain-specific system, positioning blockchains as just one application built on top of the repository’s proof/memento architecture.
Changes:
- Adds a new long-form manifesto in
docs/launch/explaining the “substrate, not blockchain” framing. - Connects that framing to existing protocol concepts such as
.proofbundles, mementos, verifier behavior, andprovekit witness. - Extends the launch/docs narrative alongside the existing
why-plugin-liftersessay.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
|
||
| If you accept this framing, the developer move is direct: stop asking "which chain do I publish to?" and start asking "what discipline am I asserting on the bodies I sign?" | ||
|
|
||
| `provekit witness` is the operational surface. You build a binary, hash it, mint a `.proof` bundle whose `binaryCid` pins the artifact and whose discharges carry whatever evidence your discipline requires, then sign and ship the pair. The verifier hashes what it received, looks up the bundle, walks the chain under its policy, emits a report. The report is itself a memento another verifier can take as evidence. |
|
|
||
| This is the Curry-Howard correspondence operating at the protocol layer. A proof of a proposition is a program that produces a witness for it. ProvekIt's `.proof` bundle is both at once: it carries the canonical IR of the transition AND the discharge mementos that prove the transition satisfies its declared contracts. The catalog memento at the root of the bundle binds the two together under one signature. Anyone who can produce a valid `.proof` has produced a valid transition. Anyone who cannot, has not. | ||
|
|
||
| There is no separate "execution" layer to validate against. Execution and proof collapse into one artifact. At planet scale, this means a producer in Lagos and a verifier in Tallinn never need to talk: the bundle that landed on the verifier's disk either holds up under the four substrate invariants or it does not, and the verifier's report is itself a memento that another verifier can take as evidence. |
Comment on lines
+27
to
+32
| If the proof is the transition, then the substrate's only job is to enforce the SHAPE of that artifact, not its semantics. ProvekIt's discipline reduces to four invariants: | ||
|
|
||
| 1. The bundle's bytes hash to its filename CID. | ||
| 2. Every embedded member's bytes hash to its declared CID. | ||
| 3. The catalog's signature verifies against its declared signer. | ||
| 4. Every required member signature verifies, and the chain DAG resolves under the verifier's policy. |
6 tasks
TSavo
added a commit
that referenced
this pull request
May 5, 2026
…370, #384) Fixes all P1/major/minor issues flagged by Copilot + CodeRabbit: walk.rs: - Bug #1: nested-block let-bindings now substituted at nested callsites; `CallsiteHit` carries `preceding_inner_stmts` (innermost-first) populated during the forward traversal; backward walk applies them before the outer- body statements. - Bug #3: actual-arg lift now delegates to `crate::lift::lift_expr_to_term` (semantic, structure-stable) instead of the old token-string fallback; binary-expr actuals produce Ctor(op, ...) not `<expr:40 + 2>` tokens. - Bug #4: arity mismatch now logs a warning and skips the callsite rather than silently zip-truncating. New test asserts the skip. - Bug #11: stale MVP-scope comment updated (if-strengthening is live). lift.rs: - Bug #5: `debug_assert!` removed from the macro match arm; it is compiled out in release builds and must not contribute to contracts. - Bug #6: `lift_function_postcondition` now scans for later `let` bindings that shadow an entry assertion's free variables and drops unsound asserts. Narrowed to LATER rebindings only (a preceding `let y = x; assert!(y ≥ 5)` is sound). - Bug #7: explicit `return expr;` tails now derive `result = <lifted expr>` postcondition (previously only trailing-no-semicolon expressions matched). canonical.rs: - Bug #8: non-i64 JSON Numbers (floats, large u64) are now encoded as a tagged object `{"__provekit_non_i64_number__": "42.5"}` instead of a plain string, preventing numeric constants and string literals of the same text from sharing a CID. walk_emit.rs / walk_demo.rs: - Bug #9: `all_param_names` now synthesizes stable placeholder names (`__self`, `__arg{i}`) for non-Ident patterns so formal arity stays aligned with actual-argument count. - Bug #10: NaN% division guarded with `if second_run_total > 0`. 11 new unit tests added (156 lib tests total, up from 145; 12 integration tests all still passing). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 5, 2026
…366) (#387) * fix(baselines): resolve P1 review concerns from #293/#326 inline Closes #366 partial (generator + BridgeV14 kit work). P1 concerns addressed: #1 Critical (CodeRabbit) — apply_builtin dead ctor0 branch: removed the unreachable `a == 0` guard introduced by `let a = if arity == 0 { 1 }`. Now arity=0 (serde default) correctly means unary; the ctor0 path is gone. #5 Major (Copilot) — gte double-wrap: the old gte arm applied ctor1(left, ctor1(sig, s)) in both branches of a dead if/else. Fixed to ctor1(left, s) — the property applied directly to the input variable, not to the builtin result. #9 + #11 (CodeRabbit Major) — rust in lang list causes duplicate rust-std-baseline-v1: removed "rust" from the hard-coded langs array. rust is already minted by provekit-baseline-rust-std (#292). rust.toml kept as reference but is not read by this binary. #13 (Copilot) — silent skip on missing config changed to panic: a missing config is always a repo error, not a runtime skip. #14 (Copilot) — unknown predicate kind silently skipped changed to panic: unknown kinds indicate a stale config or missing handler, not a soft warning. #15 (Copilot Major) — missing gte.args.left defaulting to signature changed to panic: malformed configs must not silently produce wrong-but-passing baselines. #19 (CodeRabbit Major) — PHP Minter.php mintBridgeV14 now validates and normalizes the tagged-union target before signing. Extra keys are stripped; missing kind or cid fails with InvalidArgumentException. #20 (CodeRabbit Critical) — Python bridge_v14.py missing `import base64` added. The base64 module is used at line 101 but was not imported. BridgeV14 kit work (from #326, unique to that branch): - C kit: bridge_v14.c + self_contracts.h header - PHP kit: Minter.php (+ validation fix above) - Per-kit BridgeV14 in cpp, csharp, go, python, ruby, swift, ts, zig Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * chore(baselines): regenerate 11 per-kit std baseline catalogs Baselines minted by `mint-all-baselines` against the corrected orchestrator (P1 fixes from previous commit). Rust excluded from this binary — handled by provekit-baseline-rust-std. 11 kits minted: c, cpp, csharp, go, java, php, python, ruby, swift, typescript, zig. CIDs: c blake3-512:6a30a452... cpp blake3-512:64fc0845... csharp blake3-512:e221722e... go blake3-512:efa64a6c... java blake3-512:22a41119... php blake3-512:93028afd... python blake3-512:224e0cbe... ruby blake3-512:1c52edaf... swift blake3-512:313ab922... typescript blake3-512:9da2bdff... zig blake3-512:5f7e1f73... These are byte-deterministic: same seed (FOUNDATION_V0_SEED = [0x42; 32]), same configs, same produced_at timestamp. Regeneration on any platform with the corrected binary must produce identical CIDs. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * chore(baseline-std): silence dead-code warnings + document rust.toml exclusion - Rename ctorN -> ctor_n (snake_case, fixes non_snake_case warning) - Add #[allow(dead_code)] to ctor0/ctor2 with explanatory comment; they are scaffolding for future N-ary predicate kinds, not bugs - Add comment to configs/rust.toml explaining it is intentionally excluded from the mint_all_baselines langs list — Rust baselines are owned by provekit-baseline-rust-std (#292) to avoid duplicate rust-std-baseline-v1 Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Long-form architectural framing that has been load-bearing only in commit messages until now: ProvekIt is the substrate of which blockchains are one application, not the reverse.
Derives the inversion in five steps: (1) subjective state, objective correctness; (2) the transition and the proof are the same act (Curry-Howard at the protocol layer); (3) the substrate enforces the SHAPE of state transitions but is normatively opaque to their SEMANTICS, so EVM-on-ProvekIt is one body shape among many; (4) without consensus, each producer is sovereign over their own CID-DAG; (5) the substrate stays at the four invariants because forward-compat lives at the seam between substrate and application, not in the substrate itself.
Sibling to docs/launch/why-plugin-lifters.md. Closes with
provekit witnessas the operational surface.