diff --git a/profile/README.md b/profile/README.md index ae4b137..911c828 100644 --- a/profile/README.md +++ b/profile/README.md @@ -56,6 +56,21 @@ The diagram is a project map, not a deployment diagram. Its status labels are part of the architecture: public research, published specifications, active development, and private candidates are intentionally distinguished. +## Assurance chain + +

+ + + Mechanized Isabelle/HOL models feed bounded bridges that carry evidence today, and those bridges pin named implementations; a dashed band states the target of full core refinement from models to runtime, distinguished from the bounded evidence that exists now + +

+ +The chain reads left to right: machine-checked models, the bounded bridges +that carry evidence today, and the pinned implementations they are meant to +land on. The dashed band is the target, full core refinement from models to +runtime, closed stepwise and published with its evidence; it is a goal +statement, not a current claim. + ## Repository portfolio ### Public now diff --git a/profile/assets/org-assurance-chain-mobile.svg b/profile/assets/org-assurance-chain-mobile.svg new file mode 100644 index 0000000..fe3d18d --- /dev/null +++ b/profile/assets/org-assurance-chain-mobile.svg @@ -0,0 +1,127 @@ + + Oraclizer assurance chain for narrow screens + A vertically stacked assurance chain. Mechanized Isabelle/HOL models feed bounded bridges that carry evidence today, and those bridges pin named implementations. A dashed band at the bottom states the target of full core refinement from models to runtime, kept visually separate from the bounded evidence that exists now. + + + + + + + + + + + + + + + + + + + + + + + + ORACLIZER ASSURANCE CHAIN + Models, bridges, implementations + What each layer proves today, and how much is still open + + + + MECHANIZED MODELS + Isabelle/HOL sessions + + + + Cross-domain state preservation + preservation morphisms and degrees + + + Regulatory action composition + outcomes, commutativity, normal forms + + + Protected-behavior obstructions + independent partial companion + + + GKR protocol soundness + layered reduction, derived bound + + + SMT circuit-compiler correctness + both directions, all three operations + + + machine-checked, sorry-free sessions + + + + + + + BOUNDED BRIDGES + Evidence that exists today + + + + Recorded contracts + Creusot replay + named Rust functions in five crates + + + KEVM runtime claims + Certora rules + bounded rules, selected bytecode proofs + + + Deterministic builds + frozen source identity, identical hashes + + + External proof receipt + recorded on a public verification chain + + + each bridge states its exact scope + + + + + + + PINNED IMPLEMENTATIONS + Where the models are meant to land + + + + StateSync-GKR prover + + RUST + prover and verification crates + + + ERC-TRUST reference + + SOLIDITY + reference implementation under review + + + Settlement EVM reference + + FOUNDRY + reference design on draft branches + + + each repository pins its own toolchain + + + + + TARGET + Full core refinement, models to runtime, closed stepwise + and published with its evidence. + The bridges above are bounded today and each states its own scope. + This band is the goal, not a current claim. + + diff --git a/profile/assets/org-assurance-chain.svg b/profile/assets/org-assurance-chain.svg new file mode 100644 index 0000000..2ea42d4 --- /dev/null +++ b/profile/assets/org-assurance-chain.svg @@ -0,0 +1,130 @@ + + Oraclizer assurance chain + Three columns read left to right. Mechanized Isabelle/HOL models feed bounded bridges that carry evidence today, and those bridges pin named implementations. A dashed band across the bottom states the target of full core refinement from models to runtime, distinguished from the bounded evidence that exists now. + + + + + + + + + + + + + + + + + + + + + + + + + + + ORACLIZER ASSURANCE CHAIN + From mechanized models to pinned implementations + What each layer proves today, and how much of the chain is still open + + + + + + + + + MECHANIZED MODELS + Isabelle/HOL sessions + + + + Cross-domain state preservation + preservation morphisms and degrees + + + Regulatory action composition + outcomes, commutativity, normal forms + + + Protected-behavior obstructions + independent partial companion + + + GKR protocol soundness + layered reduction, derived bound + + + SMT circuit-compiler correctness + both directions, all three operations + + + machine-checked, sorry-free sessions + + + + BOUNDED BRIDGES + Evidence that exists today + + + + Recorded contracts + Creusot replay + named Rust functions in five crates + + + KEVM runtime claims + Certora rules + bounded rules, selected bytecode proofs + + + Deterministic builds + frozen source identity, identical hashes + + + External proof receipt + recorded on a public verification chain + + + each bridge states its exact scope + + + + PINNED IMPLEMENTATIONS + Where the models are meant to land + + + + StateSync-GKR prover + + RUST + prover and verification crates + + + ERC-TRUST reference + + SOLIDITY + reference implementation under review + + + Settlement EVM reference + + FOUNDRY + reference design on draft branches + + + each repository pins its own toolchain + + + + + + + + TARGET + Full core refinement, models to runtime, closed stepwise and published with its evidence. + The bridges above are bounded today and each states its own scope. This band is the goal, not a current claim. + +