Vérification indépendante des 6 facts VPSF on-chain

Six programmes Cairo ont chacun vérifié une preuve Stwo valide d'une claim de l'algèbre de claims Vauban (VPSF, sextuplet ⟨ Subject, Predicate, Evidence, TemporalFrame, RevelationMask, Anchor ⟩, opérateurs ∧ → ⊕ ▷ ¬). Chaque vérification a ensuite été prouvée par récursion Stone et enregistrée sur la vraie FactRegistry du projet integrity (StarkWare) sur Starknet Sepolia. Cette page interroge cette FactRegistry en lecture seule, sans clé ni compte, et affiche exactement ce qui revient de la chaîne au moment où vous ouvrez la page. Rien ci-dessous n'est codé en dur sans confrontation à un appel RPC réel ; en cas d'échec, cet échec s'affiche tel quel, jamais masqué.

Ce qu'un fact atteste précisément : un programme Cairo (vérifieur vendoré, écrit par StarkWare dans le crate verifier_core::poseidon252_verifier, pas par Vauban) a accepté une preuve Stwo valide pour les entrées publiques listées sous chaque carte ci-dessous. Le vérifieur Stwo tourne hors chaîne, dans la CairoVM ; ce n'est pas un vérifieur Stwo on-chain. Son exécution est ensuite elle-même prouvée par une preuve Stone récursive, et c'est cette preuve Stone qui est vérifiée on-chain par le contrat FactRegistry.

Deux couches de sécurité distinctes sont en jeu, à ne jamais confondre dans une même affirmation : la preuve Stwo interne utilise le hachage Poseidon252, une construction conjecturée résistante aux calculateurs quantiques pour cette couche précise ; la preuve Stone qui l'enveloppe pour l'écriture on-chain utilise une sécurité classique conjecturée standard, pas post-quantique. Les clés opérationnelles du rail (signature du compte, transport RPC) sont elles aussi classiques, sans lien avec la résistance quantique de la couche STARK.

Comment recalculer un fact sans nous croire

Chaque fact suit la même formule de rail, réutilisée à l'identique pour les 6 claims (« rail palier-1 » ; voir docs/research/stwo-onchain-verifier-spike.md §14.4.3 et docs/deployments/evidence/p4-rails/rails-4ops.md) :

poseidon(stage1_output) = H1
lbo  = [1, 4, LB_POS, BOOT13, H1]
fact = poseidon([BOOT13, poseidon(lbo)])

stage1_output est la sortie publique du programme de vérification ([1, n, hash_du_programme, <publics de la claim>]), donnée en entier pour chaque claim dans les cartes ci-dessus. LB_POS et BOOT13 sont deux constantes du rail (les hash des programmes layout_bridge et simple_bootloader utilisés pour la récursion), identiques pour les 6 facts :

LB_POS = 0x193aa1de18292f8406be43bd2e0978227a063fc861907a10476e10ec1fefbab
BOOT13 = 0xd16f813fdc43ac794eb60e2477e640ff6731b3ede37eaec4ec8d25159377fb

Un lecteur technique peut rejouer cette formule avec sa propre implémentation Poseidon Starknet (par exemple cairo-lang ou starknet.js) et retrouver le fact publié, sans dépendre de notre code. Cette page ne réimplémente délibérément pas Poseidon en JavaScript : vous demander de faire confiance à notre implémentation irait contre l'objectif même de cette section. Pour la claim DelegationGrant (→), le hash du programme main_grant est abrégé dans le document source d'origine ; la valeur déjà hachée poseidon(stage1_output) est donnée en entier et suffit à poursuivre le calcul jusqu'au fact.

Limites, cadrage honnête

• POC testnet Starknet Sepolia. Pas mainnet, pas de valeur en jeu.
• Le programme qui vérifie la preuve Stwo est le vérifieur Cairo de StarkWare, vendoré tel quel ; Vauban n'en a pas écrit le code, seule l'AIR de la claim VPSF vérifiée par ce programme est d'origine Vauban.
• Le binding n'atteste pas le sens externe des identifiants : subject et authority sont des entiers de démonstration, pas des identités réelles vérifiées hors chaîne.
• Le prouveur Rust actuel fige chaque claim de démonstration à des valeurs fixes ; un prouveur paramétrique généralisé à des entrées arbitraires est un travail distinct, en cours pour la claim DelegationGrant uniquement à ce stade.
• Aucune comparaison de primauté ou de concurrence n'est faite sur cette page.