OAI/Analysis/MatrixSigning/Encoding/WireProgramPrimitives.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W15.WireProgram.ports3 line 10
2. def OAI.KS.W15.WireProgram.copyProgram line 15
3. theorem OAI.KS.W15.WireProgram.copy_spec line 18
4. def OAI.KS.W15.WireProgram.transferProgram line 26
5. def OAI.KS.W15.WireProgram.transferAfter line 30
6. theorem OAI.KS.W15.WireProgram.transfer_spec line 34
7. def OAI.KS.W15.WireProgram.stayProgram line 61
8. theorem OAI.KS.W15.WireProgram.stay_spec line 64
9. def OAI.KS.W15.WireProgram.pushProgram line 77
10. theorem OAI.KS.W15.WireProgram.push_spec line 81
11. def OAI.KS.W15.WireProgram.literalProgram line 97
12. theorem OAI.KS.W15.WireProgram.literal_spec line 101