OAI/Analysis/MatrixSigning/Machines/DenseFieldCounter.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.DenseFieldCounter.unary line 13
  2. def OAI.CurrentKS.DenseFieldCounter.state line 15
  3. def OAI.CurrentKS.DenseFieldCounter.unaryPorts line 18
  4. def OAI.CurrentKS.DenseFieldCounter.countPorts line 19
  5. def OAI.CurrentKS.DenseFieldCounter.bodyCopyPorts line 20
  6. def OAI.CurrentKS.DenseFieldCounter.doublePorts line 21
  7. def OAI.CurrentKS.DenseFieldCounter.decode line 22
  8. def OAI.CurrentKS.DenseFieldCounter.countCopy line 23
  9. def OAI.CurrentKS.DenseFieldCounter.bodyCopy line 24
  10. def OAI.CurrentKS.DenseFieldCounter.movePart line 25
  11. def OAI.CurrentKS.DenseFieldCounter.popCount line 26
  12. def OAI.CurrentKS.DenseFieldCounter.body line 27
  13. def OAI.CurrentKS.DenseFieldCounter.square line 28
  14. def OAI.CurrentKS.DenseFieldCounter.doubleCopy line 29
  15. def OAI.CurrentKS.DenseFieldCounter.clear line 30
  16. def OAI.CurrentKS.DenseFieldCounter.program line 31
  17. lemma OAI.CurrentKS.DenseFieldCounter.base_decode_spec line 34
  18. lemma OAI.CurrentKS.DenseFieldCounter.decode_spec line 45
  19. lemma OAI.CurrentKS.DenseFieldCounter.countCopy_spec line 58
  20. lemma OAI.CurrentKS.DenseFieldCounter.bodyCopy_spec line 66
  21. lemma OAI.CurrentKS.DenseFieldCounter.movePart_spec line 75
  22. lemma OAI.CurrentKS.DenseFieldCounter.popCount_spec line 84
  23. lemma OAI.CurrentKS.DenseFieldCounter.body_spec line 93
  24. lemma OAI.CurrentKS.DenseFieldCounter.square_trace line 104
  25. lemma OAI.CurrentKS.DenseFieldCounter.doubleCopy_spec line 128
  26. lemma OAI.CurrentKS.DenseFieldCounter.clear_spec line 137
  27. theorem OAI.CurrentKS.DenseFieldCounter.program_spec line 145