OAI/Analysis/MatrixSigning/Matrices/MatrixAddressArithmetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W08.MatrixAddress.addPorts line 16
  2. def OAI.KS.W08.MatrixAddress.addProgram line 17
  3. def OAI.KS.W08.MatrixAddress.cleanupProgram line 19
  4. def OAI.KS.W08.MatrixAddress.program line 22
  5. def OAI.KS.W08.MatrixAddress.rawProduct line 26
  6. def OAI.KS.W08.MatrixAddress.rawAddress line 27
  7. def OAI.KS.W08.MatrixAddress.ticks line 30
  8. theorem OAI.KS.W08.MatrixAddress.add_spec line 35
  9. theorem OAI.KS.W08.MatrixAddress.reoutput_spec line 49
  10. theorem OAI.KS.W08.MatrixAddress.cleanup_spec line 56
  11. theorem OAI.KS.W08.MatrixAddress.full_spec line 69
  12. theorem OAI.KS.W08.MatrixAddress.ticks_le line 88
  13. theorem OAI.KS.W08.MatrixAddress.run_encoded line 103
  14. theorem OAI.KS.W08.MatrixAddress.matrix_address_budget line 119
  15. theorem OAI.KS.W08.MatrixAddress.run_matrix_address line 128