OAI/Analysis/MatrixSigning/Machines/SparseCoefficientStage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.SparseCoefficientStage.ports line 11
  2. def OAI.KS.W19.SparseCoefficientStage.arithmetic line 13
  3. def OAI.KS.W19.SparseCoefficientStage.put line 15
  4. def OAI.KS.W19.SparseCoefficientStage.after line 17
  5. theorem OAI.KS.W19.SparseCoefficientStage.arithmetic_spec line 21
  6. def OAI.KS.W19.SparseCoefficientStage.cleanupPorts line 51
  7. def OAI.KS.W19.SparseCoefficientStage.cleanup line 52
  8. def OAI.KS.W19.SparseCoefficientStage.program line 53
  9. def OAI.KS.W19.SparseCoefficientStage.ticks line 55
  10. def OAI.KS.W19.SparseCoefficientStage.result line 58
  11. theorem OAI.KS.W19.SparseCoefficientStage.full_spec line 62