Quand la couverture de ligne ment

Cette note est écrite pour être lue deux fois. Les deux premières sections ne supposent aucune exposition préalable aux systèmes de contraintes et construisent le mécanisme depuis la base. Le reste est écrit pour ceux qui construisent et auditent ces circuits, et va droit au code exact, à l’algèbre de l’exploit et à une validation conçue pour ne pas pouvoir se flatter elle-même.

Ce qu’un système de contraintes vérifie réellement

Une preuve zero knowledge d’un calcul repose sur une seule idée. Au lieu de réexécuter le travail, un vérificateur contrôle qu’une table remplie, appelée la trace, obéit à un ensemble fixe de règles algébriques. Chaque ligne est une étape du calcul et chaque colonne est un registre ou une valeur intermédiaire. Formellement la trace est $T\in {\mathbb{F}}^{n\times w}$, une matrice de $n$ lignes et $w$ colonnes sur un corps fini.

Chaque règle est un polynôme qui doit s’évaluer à zéro. Une règle qui agit sur une seule ligne demande qu’un certain polynôme $C$ s’annule sur chaque ligne :

Une règle qui relie une étape à la suivante agit sur une paire de lignes adjacentes, $C({\mathbf{t}}_i,{\mathbf{t}}_{i+1})=0$. Le prouveur envoie une trace et le vérificateur contrôle que chaque règle s’annule. Si toutes s’annulent, le vérificateur est convaincu que le calcul a été mené correctement.

La soundness est la propriété qui rend cela digne de confiance. Les règles doivent verrouiller la trace, de sorte que, pour une entrée publique donnée, il n’existe pas de trace valide autre que l’honnête. Quand les règles sont trop faibles, une trace différente les satisfait toutes et le système est sous-contraint.

Un prouveur qui veut tricher remplit cette autre trace, chaque règle s’annule encore et le résultat est une preuve valide d’un énoncé faux. La sous-contrainte n’est pas une inquiétude théorique. C’est la classe de bug de soundness dominante dans les systèmes zero knowledge de production, et elle a déplacé de l’argent réel.

Ce qui compte ici, c’est la conditionnalité. La plupart des règles ne s’appliquent que parfois. Une règle de frontière ne s’applique que sur la première ligne, une règle de transition s’applique entre lignes consécutives mais pas à travers le rebouclage à la fin, une règle d’instruction ne s’applique que sur les lignes où un drapeau d’opcode particulier est mis. Le framework n’écrit pas de if. Il multiplie la règle par un polynôme sélecteur $s$ qui vaut un là où la règle doit s’appliquer et zéro ailleurs, puis demande au produit de s’annuler :

Tout découle de cette seule équation. Là où $s=1$ la ligne doit satisfaire $C$. Là où $s=0$ le produit vaut zéro quel que soit $C$, donc sur ces lignes la contrainte n’impose rien. Elle est inerte.

L’angle mort

Un circuit est du code, et les équipes le testent comme du code. Le réflexe habituel est la couverture de ligne : lancer les tests, confirmer que chaque ligne de la définition de la contrainte s’est exécutée, considérer le vert comme sûr.

La couverture de ligne répond à une autre question que celle dont la soundness a besoin. Elle demande si l’instruction d’assertion s’est exécutée, et elle l’a fait. L’évaluateur parcourt chaque ligne de la trace et appelle la contrainte sur chacune, si bien que la ligne est couverte sur toutes, même les lignes où le sélecteur vaut zéro et où la contrainte n’impose rien. L’instruction s’est exécutée pendant que la contrainte restait non testée.

En haut, ce qu’un outil de couverture rapporte, cent pour cent : l’assertion s’est exécutée sur les huit lignes. La bande du dessous est ce qui s’est réellement passé, la contrainte imposée sur trois d’entre elles. Un outil de ligne ne peut pas séparer une garde correctement câblée d’une garde cassée, car les deux exécutent la même ligne le même nombre de fois. La coche verte mesure l’exécution et la rapporte comme de la sûreté.

Ce n’est pas un coin rare. Les contraintes conditionnelles sont la forme par défaut dans ces systèmes, ce qui est proche de la totalité d’entre elles.

Le bug que cela dissimule

Une famille de bugs vit dans l’interstice, et elle s’énonce simplement : une contrainte correcte rattachée au mauvais sélecteur. Elle s’exécute, elle affiche du vert et elle échoue à contraindre les lignes qui comptent.

Prenez un accumulateur. L’exponentiation par carrés successifs construit une valeur courante où chaque étape élève la précédente au carré et multiplie par un facteur dépendant d’un bit :

où la valeur sur la dernière ligne, $a_{n-1}$, est le résultat revendiqué $r$. La récurrence doit tenir sur chaque ligne après la première, puisque la ligne zéro n’a pas de prédécesseur. Gardée correctement, avec un sélecteur qui vaut un partout sauf sur la première ligne, elle est imposée sur les lignes $1$ à $n-1$ et atteint la dernière ligne, si bien que le résultat est lié au calcul.

Gardée avec le mauvais sélecteur, un qui vaut zéro sur la dernière ligne au lieu de la première, elle est imposée sur les lignes $0$ à $n-2$ et ne touche jamais la ligne de sortie. Une trace honnête paraît correcte, car une trace honnête satisfait de toute façon la récurrence partout. Le résultat est désormais libre.

Un prouveur fixe $a_{n-1}$ à n’importe quelle valeur choisie, chaque ligne imposée tient encore, la règle de frontière qui lie la colonne de sortie à la revendication publique est satisfaite par construction et le vérificateur accepte une preuve d’un exposant faux. Ceci est un constat réel issu d’un audit publié d’une machine virtuelle zero knowledge de production, et tout le défaut tient en un seul mauvais sélecteur.

Une métrique qui mesure l’imposition, pas l’exécution

Le reste de cette note s’adresse à ceux qui travaillent sur ces systèmes.

Le correctif n’est pas un meilleur outil de couverture de ligne mais une mesure différente. Pour chaque site de contrainte, sur une trace valide, enregistrez là où la garde était réellement active plutôt que si l’instruction s’est exécutée. Appelez cet enregistrement son profil d’activation :

struct ConstraintCov {
    active_rows: usize,             // garde non nulle
    inactive_rows: usize,          // garde nulle
    min_active_row: Option<usize>, // première ligne atteinte
    max_active_row: Option<usize>, // dernière ligne atteinte
    // ... plus active_zero / active_nonzero
}

Un point de conception n’était pas évident à l’avance. Un booléen, « cette contrainte a-t-elle été active au moins une fois », n’attrape pas les vrais bugs. Dans l’accumulateur ci-dessus, la garde cassée est active sur sept lignes sur huit et la garde correcte est elle aussi active sur sept lignes sur huit, donc les deux rapportent « active au moins une fois ». Le signal n’est pas combien de lignes mais quelles lignes : la garde correcte atteint la dernière ligne et la cassée non. Le profil d’activation porte cette distinction et le booléen la jette.

L’instrumentation est petite, et c’est là tout l’intérêt. Dans un builder de style Plonky3, la multiplication de la garde vit à exactement un endroit, le builder filtré qui replie une condition dans une assertion :

// FilteredAirBuilder::assert_zero
fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    self.inner.assert_zero(self.condition() * x.into());
}

Chaque contrainte gardée dans tout le système passe par cette unique multiplication. Donc un seul hook là, alimenté par l’évaluateur de trace concrète, les voit toutes :

fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    // Rapporte la garde avant qu’elle soit repliée dans le terme. Après la
    // multiplication, la garde et l’expression contrainte sont indiscernables.
    self.inner.aircov_note_guard(&self.condition);
    self.inner.assert_zero(self.condition() * x.into());
}

Ce recorder est protégé par un feature flag et reste inerte tant qu’une session n’est pas ouverte, si bien que les builds ordinaires ne paient rien. La métrique se lit sur une trace valide : passez les contraintes dans l’évaluateur, et au lieu de réussite ou échec la sortie est l’ensemble des lignes sur lesquelles chaque garde était vivante.

L’exploit, sur le profil d’activation

Le bug de l’accumulateur est désormais visible avant que quiconque lance l’exploit. Basculez la garde ci-dessous et observez la dernière ligne, celle qui porte le résultat.

Sous la garde correcte, la récurrence atteint la ligne de sortie, si bien qu’un résultat erroné ne peut pas passer. La garde cassée laisse la ligne de sortie non contrainte, ce qui est exactement la liberté qu’utilise la falsification. Deux profils, un sélecteur différent, même code et mêmes lignes exécutées. Le bug livré ressemblait à ceci :

// Impose la récurrence d’accumulation.
builder
    .when(local.is_real)
    .when_not(local.is_last)   // garde livrée ; le correctif est is_first
    .assert_eq(local.accum, local.prev_accum_squared_times_multiplier);

La couverture de ligne de cette assertion est de cent pour cent sous n’importe quel test honnête, car l’assertion s’exécute sur chaque ligne. Le profil d’activation est le seul signal bon marché qui la sépare de la version correcte sur une trace valide, sans que personne ait à penser d’abord à la falsification.

Une validation, bâtie pour ne pas pouvoir se flatter elle-même

Il y a une objection évidente. Les champs de position de ligne ont été ajoutés en regardant un bug de garde de ligne, donc valider la métrique sur ce même bug ne prouve rien, car une métrique attrapera toujours le cas autour duquel elle a été façonnée.

Pour séparer la prédiction de l’ajustement, la métrique a été gelée par écrit et les prédictions enregistrées à l’avance. Le critère a été fixé avant qu’aucun bug tenu à l’écart ne soit construit : AIRCov distingue un bug lorsque le profil gelé par site, calculé sur une trace valide, diffère entre le circuit correct et le circuit cassé pour au moins un site partagé. Quatre classes de bug ont alors été reconstruites comme des circuits minimaux écrits à la main, chacune une reconstruction fidèle d’un motif documenté plutôt qu’un bug attrapé dans la nature, et chacune confirmée réellement exploitable, c’est-à-dire une trace forgée que le circuit cassé accepte et que le correct rejette.

Les quatre prédictions ont tenu. Regardez la ligne du mauvais sélecteur, qui porte tout le poids. C’est un mécanisme différent du bug de garde de ligne autour duquel la métrique a été façonnée, donc un attrapé là est une preuve que le profil se généralise à un bug qu’il n’a pas été conçu pour cibler, plutôt qu’une preuve qu’il a mémorisé un cas. Les trois ratés ont été prédits à l’avance et marquent la frontière honnête de la méthode.

Une réserve se loge à l’intérieur du critère. Il demande si le profil diffère entre le circuit correct et le circuit cassé, ce qui présume une référence connue comme correcte pour faire la comparaison. Un vrai audit n’a pas une telle référence. Cette absence est tout le problème. En déploiement la métrique émet un unique profil et un relecteur le juge par lui-même, où une récurrence qui n’atteint jamais la ligne de sortie se lit comme fausse sans aucune jumelle à laquelle la comparer. Le quatre sur quatre est mesuré sous cet oracle plus favorable. Le signal de déploiement est la lecture plus faible de la même empreinte, c’est pourquoi le cadrage de clôture l’appelle l’empreinte d’un relecteur et non un verdict.

Gelez la métrique, écrivez d’abord les prédictions, puis reconstruisez les bugs. Des résultats qui ne tiennent qu’une fois ajustés après coup sont une mesure du recul.

Ce qu’elle ne peut pas attraper

Cette frontière est nette, et l’énoncer clairement est tout l’intérêt d’une métrique digne de confiance.

AIRCov attrape les bugs de garde et de sélecteur dont le profil d’activation diffère sur une trace valide. Trois choses restent hors de portée :

• Contraintes manquantes. Sans site, il n’y a rien à mesurer. Une métrique sur les contraintes qui existent ne peut pas voir celle qui n’existe pas.
• Bugs d’expression étroite. Une règle qui vérifie un seul limb d’un mot là où elle devrait les vérifier tous a le même site, la même garde et le même profil d’activation que la version correcte. Il n’y a pas de différence à détecter, car la différence se loge à l’intérieur de l’expression plutôt que dans le moment où elle se déclenche.
• Bugs de garde invisibles sur des traces valides. Une condition supplémentaire parasite que des données honnêtes satisfont par hasard ne laisse aucune marque dans la couverture mesurée sur des traces valides. C’est une limite de toute couverture sur trace valide, AIRCov compris, pas une lacune qu’une métrique plus fine comble.

Ceci est donc un instrument pour une classe, avec un bord caractérisé. Il fait remonter une empreinte, une récurrence qui n’atteint jamais la ligne de sortie, une contrainte qui se déclenche sur les lignes que sa jumelle saute, qu’un relecteur ou une règle en aval interprète ensuite. Il ne rend pas de verdict.

Sur la vraie pile, et où cela se situe

Rien de ce qui précède ne dépend d’un jouet. L’instrumentation tourne sur la pile de production. Le SP1 actuel évalue ses chips à travers une réexportation de la crate p3-air publiée, si bien que le même hook d’une ligne, intégré dans cette crate et appliqué en patch, traverse le vrai builder de contraintes. La couverture a été collectée sur un chip qui est livré dans SP1, passé par son propre évaluateur. L’exploit a été lancé sur un chip construit avec les vrais traits et le builder de contraintes de SP1 qui porte la même classe de mauvais sélecteur, bien que ce ne soit pas l’un des chips de production préexistants comme les unités arithmétiques. Sur ce chemin vivant le défaut est à la fois exploitable, avec une trace forgée acceptée à zéro ligne en échec, invisible à la couverture de ligne, mesuré à cent pour cent sur la contrainte qui le porte et visible dans le profil d’activation. Injecter des motifs documentés dans les chips de production eux-mêmes est le travail restant.

Un mot sur les travaux antérieurs. Un fuzzer métamorphique pour machines virtuelles zero knowledge trouve déjà des bugs de soundness et de complétude, utilise déjà un retour léger de couverture d’instruction et nomme la couverture taillée pour les contraintes comme travail futur. Il est à la fois la référence de base et une preuve indépendante que la direction vaut la peine d’être suivie. Les tâches diffèrent. Cette ligne de travaux génère des tests et trouve des bugs, tandis qu’AIRCov mesure si une suite de tests déjà en main est adéquate, pour une classe de bug, avec la frontière tracée. Aucune prétention n’est faite d’être le premier au test de mutation dans cet espace. Ce qui est revendiqué est plus étroit : une métrique d’adéquation par profil d’activation à position de ligne, avec une preuve tenue à l’écart et pré-enregistrée qu’elle sépare une vraie classe de bug que la couverture de ligne ne peut pas voir.

Les forks instrumentés et chaque test ci-dessus sont publics, du cas de faisabilité, en passant par l’exploit de preuve forgée et le constat d’audit reconstruit, jusqu’à la validation gelée et pré-enregistrée, si bien que les nombres ici peuvent être relancés plutôt que pris sur la foi.

Reproduisez-le

Deux forks portent l’instrumentation et les tests.

• Fork Plonky3 : le recorder, le hook de garde d’une ligne, et les quatre tests, la faisabilité, l’exploit de preuve forgée, le constat d’audit reconstruit et la validation gelée et pré-enregistrée. Détails dans son AIRCOV.md.
• Fork SP1 : le même hook sur la pile de production, câblé à travers une copie intégrée de p3-air et le propre builder de contraintes de SP1, avec la couverture lancée sur un vrai chip. Détails dans son AIRCOV.md.