Laboratoire IMATH

Par Daniel Augot :
Titre :
La modélisation R1CS des circuits arithmétiques, et l’arithmétisation de Spartan

Résumé :
Nous avons vu le modèle d’exécution AIR (algebraic intermediate representation) qui représente une trace d’exécution comme des colonnes de registres avec des contraintes de transition d’une ligne à l’autre au fur et à mesure de l’exécution.

Je présenterai un autre modèle, dit de circuit arithmétique, et sa représentation sous forme de matrices, dite R1CS (rank-1 contrained system). Cette représentation est beaucoup utilisée et forme, avec AIR, le point de départ de beaucoup de cryptographe concevant le post-traitement cryptographique proprement dit.

Ensuite, nous verrons Spartan qui est un de ces post-traitements qui réduit R1CS à des relations polynomiales. Ces relations polynomiales sont traitées par le Prouveur et le Vérifieur en interaction, avec des sous protocoles, comme sum-check et les "polynomial commitments", en boîte noire.

Enfin, je donnerai deux constructions de "polynomials commitments", un à base de codes de Reed-Solomon, et un à base de courbes elliptiques avec couplage.

Par Hugo Delavenne :
Titre :
Tests de proximité à des codes sur les graphes

Résumé :
Les codes de Tanner sont des codes correcteurs dans lesquels des contraintes locales sont appliqués sur des petits ensembles de coordonnées. Ces codes sont étudiés pour leurs propriétés locales : décodage parallélisable pour l’efficacité, correction locale pour le stockage, tests locaux pour les premières constructions à la PCP... Cependant, ces tests de proximité sont plutôt théoriques et asymptotiques.

Un cas particulier des codes de Tanner sont les codes expanseurs, pour lesquels chaque coordonnée apparaît dans exactement deux jeux de contraintes locales. On peut alors représenter ces codes sous forme de graphes où les coordonnées sont les arêtes et les nœuds décrivent les contraintes appliqués sur les arêtes adjacentes.

Je présenterai dans cet exposé mes travaux pour adapter le test de proximité interactif aux codes de Reed-Solomon que nous avons vu la dernière fois à des familles de codes sur certains graphes. Je présenterai également notre tentative d’exploiter spécifiquement ce test de proximité pour du partage de secret vérifiable asynchrone.

Cet exposé est la conclusion de la série de séminaires, et fait suite aux deux exposés précédents :
 le 12 février : Présentation pour des codeurs de la preuve originelle du théorème PCP par Daniel Augot
 le 12 mars : Calcul vérifiable (SNARK) à base de tests de proximités à des codes de Reed-Solomon par Hugo Delavenne