Randomize checking of each optimization pass
- Lingua principale
- Rust
- Stelle
- 96
- Fork
- 39
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Descrizione
With each optimization pass, we are running the risk that our transformations might have a bug that would lead to an invalid set of constraints.
As an extra precautionary measure, we should try to check that each successive pass ensures the correctness of the transformation. I *think* we could implement this as an internal check in each pass.
The idea is to again use randomized polynomial identity testing. Given a list of expressions $f_1, \ldots, f_n$, which get transformed into $g_1, \ldots, g_n$, we should make sure that $f_i(r) = g_i(r)$ for some randomly sampled $r$ from a large enough field (`QuadFelt` seems the safest, although we can repeat the test with multiple random `Felt`).
This technique is easy when an optimization pass simply maps one constraint to another, but is more complicated if we are reordering or removing redundant constraints. It seems like we would need some extra logic to be able to accurately compare the the set of input and set of output expressions as a whole.
Making our transformations more robust in this way would give us way more confidence in our pipeline. Applying this test to our dummy examples may not catch all mistakes, but for our main use case which is writing the Miden VM constraints, we could be sure that the generated code matches the initial description.
Moreover, this should make it much easier to audit the compiler since we could focus mainly on whether this randomized test is correct, rather than having to check that the individual optimizations are sound.
Guida per i contributori
Apri la guida per i contributori
Direzione di ricerca
Esamina le passate di ottimizzazione nella pipeline del compilatore, probabilmente in una directory come `src/optimization`. Comprendi come ogni passata trasforma i vincoli. Il test prevede il campionamento casuale di elementi di campo (QuadFelt, Felt) e la valutazione delle espressioni di input e output. Inizia implementando un helper per i test di identità polinomiale randomizzati su una singola passata. Controlla i test esistenti per esempi fittizi e i vincoli di Miden VM per vedere il punto di integrazione.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Valutazione
- Stack tecnologico
- rust
- Ambito
- compilers
- Tipo di issue
- Funzionalità
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Stato di attività
- Ferma
- Chiarezza
- Abbastanza chiara
- Idoneità per principianti
- 35/100