diff --git a/profile/README.md b/profile/README.md index dcb710c..d582c7f 100644 --- a/profile/README.md +++ b/profile/README.md @@ -47,7 +47,7 @@ semantics, mechanized models, and proving infrastructure.

- + Oraclizer system and research map showing on-chain and off-chain systems connected through the OIP and OSS target architecture, with regulatory semantics and assurance layers

@@ -60,7 +60,7 @@ development, and private candidates are intentionally distinguished.

- + 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

diff --git a/profile/assets/oraclizer-system-map-mobile.svg b/profile/assets/oraclizer-system-map-mobile.svg index 752ce20..066bb91 100644 --- a/profile/assets/oraclizer-system-map-mobile.svg +++ b/profile/assets/oraclizer-system-map-mobile.svg @@ -1,99 +1,77 @@ - + Oraclizer system and research map for narrow screens - A vertically arranged project map showing off-chain and on-chain systems bidirectionally synchronized through the OIP and OSS target architecture, with regulatory semantics, assurance work, and current publication and maturity labels. + A vertically arranged project map showing off-chain and on-chain systems synchronized through the OIP and OSS target architecture, with regulatory semantics, assurance work, and current publication and maturity labels. - - - - - - - - - - - - - - + + + + + + + + + - - - - + + ORACLIZER SYSTEM MAP + Protocol, semantics, and assurance + Current publication and maturity boundaries - - ORACLIZER SYSTEM MAP - Protocol, semantics, and assurance - Current publication and maturity boundaries + + SOURCE SYSTEMS + + + OFF-CHAIN + Financial, identity,and regulated state + + + ON-CHAIN + Token, contract,and settlement state + + + STATE SYNC - - - OFF-CHAIN SYSTEMS - Financial, identity, and - regulated state + + + TARGET ARCHITECTURE + ORACLE STATE MACHINE + Bidirectional coordination of state transitions + + OIP v0.5 · PUBLISHED + + OSS · IN DEVELOPMENT + BIND → VERIFY → COMMIT - - - ON-CHAIN SYSTEMS - Token, contract, and - settlement state + + + Regulatory semantics + Shared meaning, transitions, and execution boundaries + + RCP / ERC-8319 + Public proposal · open editor review + PUBLIC + + ERC-TRUST + Public pre-ERC candidate · community review + PUBLIC - - - - - - STATE SYNC - - + + + Assurance + Machine-checked models and proving infrastructure + + formal-verification + Production-maintained model artifacts + PUBLIC + + StateSync-GKR + Private prover stack · public release planned + PRIVATE - - TARGET ARCHITECTURE - ORACLE STATE MACHINE - Bidirectional coordination of state transitions - - OIP v0.5 · PUBLISHED - - OSS · IN DEVELOPMENT - BIND → VERIFY → COMMIT - - - - - REGULATORY SEMANTICS - Shared meaning, state transitions, and execution boundaries - - RCP / ERC-8319 - Public proposal · open and under editor review - - PUBLIC - - ERC-TRUST - Public pre-ERC candidate · unaudited, not for production - - PUBLIC - - - - - ASSURANCE - Machine-checked models and proving infrastructure - - formal-verification - Production-maintained, model-level research artifacts - - PUBLIC - - StateSync-GKR - Private prover stack · public release planned - - PRIVATE - - - - ASSURANCE BOUNDARY - Project map, not a deployment diagram. No audit, legal, deployment, or refinement claim. + + + ASSURANCE BOUNDARY + Project map only. No audit, deployment, legal, or full-refinement claim. diff --git a/profile/assets/org-assurance-chain-mobile.svg b/profile/assets/org-assurance-chain-mobile.svg index fe3d18d..55d7ab4 100644 --- a/profile/assets/org-assurance-chain-mobile.svg +++ b/profile/assets/org-assurance-chain-mobile.svg @@ -1,127 +1,56 @@ - - 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 for narrow screens + A vertically stacked assurance chain. Mechanized Isabelle models feed bounded evidence bridges, which pin named implementations. A separate final band states the target of full core refinement and is not a current claim. - - - - - - - - - - - - - - + + + + - - - - - - - - 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. + + + + + ORACLIZER ASSURANCE CHAIN + Models, bridges, implementations + What each layer proves today, and what remains open + + + MECHANIZED MODELS + Isabelle/HOL sessions + + Cross-domain state preservationpreservation morphisms and degrees + Regulatory action compositionoutcomes, commutativity, normal forms + Protected-behavior obstructionsindependent partial companion + GKR protocol soundnesslayered reduction with a derived bound + SMT circuit-compiler correctnessboth directions across all three operations + Machine-checked, sorry-free sessions + + + + BOUNDED BRIDGES + Evidence that exists today + + Recorded contracts + Creusot replaynamed Rust functions in five crates + KEVM runtime claims + Certora rulesbounded rules and selected bytecode proofs + Deterministic buildsfrozen source identity and identical hashes + External proof receiptrecorded on a public verification chain + Every bridge states its exact scope + + + + PINNED IMPLEMENTATIONS + Where the models are meant to land + + StateSync-GKR proverRUSTprover and verification crates + ERC-TRUST referenceSOLIDITYpublic reference implementation + Settlement EVM referenceFOUNDRYreference design on draft branches + + + TARGET + Full core refinement from models to runtime, + closed stepwise and published with its evidence. + The bridges above are bounded and state their scope. + This band is a goal, not a current claim.