OAI/Analysis/MatrixSigning/Arithmetic/BinaryAddressLookup.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W08.matrixCursorPorts line 15
2. def OAI.KS.W08.matrixCursorProgram line 21
3. theorem OAI.KS.W08.accessConfig_ext line 24
4. theorem OAI.KS.W08.ofMachine_lift_run_eq line 30
5. theorem OAI.KS.W08.run_matrixCursorProgram line 39
6. def OAI.KS.W08.binaryMatrixLookupProgram line 81
7. theorem OAI.KS.W08.binaryMatrixLookupProgram_states line 84
8. theorem OAI.KS.W08.run_binaryMatrix_lookup line 86
9. theorem OAI.KS.W08.binaryMatrix_lookup_time line 117