OAI/Analysis/MatrixSigning/Matrices/RowDotMachine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W12.RowDot.initialStacks line 11
  2. def OAI.KS.W12.RowDot.copyVector line 16
  3. def OAI.KS.W12.RowDot.prepareProgram line 17
  4. def OAI.KS.W12.RowDot.prepareTicks line 19
  5. theorem OAI.KS.W12.RowDot.prepare_spec line 22
  6. def OAI.KS.W12.RowDot.clearCounter line 38
  7. def OAI.KS.W12.RowDot.restoreWire line 39
  8. def OAI.KS.W12.RowDot.dotPorts line 40
  9. def OAI.KS.W12.RowDot.dotProgram line 41
  10. def OAI.KS.W12.RowDot.finishProgram line 43
  11. def OAI.KS.W12.RowDot.finishTicks line 45
  12. theorem OAI.KS.W12.RowDot.finish_spec line 48
  13. def OAI.KS.W12.RowDot.program line 78
  14. def OAI.KS.W12.RowDot.totalTicks line 80
  15. theorem OAI.KS.W12.RowDot.full_spec line 83
  16. theorem OAI.KS.W12.RowDot.transient_payload line 95