OAI/Analysis/MatrixSigning/Realization/FoldRoutine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.FoldRoutine.source line 11
  2. abbrev OAI.CurrentKS.FoldRoutine.accumulator line 12
  3. abbrev OAI.CurrentKS.FoldRoutine.work line 13
  4. abbrev OAI.CurrentKS.FoldRoutine.temp line 14
  5. def OAI.CurrentKS.FoldRoutine.ports line 15
  6. def OAI.CurrentKS.FoldRoutine.state line 16
  7. def OAI.CurrentKS.FoldRoutine.initialPorts line 19
  8. def OAI.CurrentKS.FoldRoutine.decodePorts line 21
  9. def OAI.CurrentKS.FoldRoutine.framePorts line 23
  10. lemma OAI.CurrentKS.FoldRoutine.initialPorts_apply line 26
  11. lemma OAI.CurrentKS.FoldRoutine.decodePorts_apply line 29
  12. lemma OAI.CurrentKS.FoldRoutine.framePorts_apply line 32
  13. def OAI.CurrentKS.FoldRoutine.setup line 35
  14. def OAI.CurrentKS.FoldRoutine.decode line 38
  15. def OAI.CurrentKS.FoldRoutine.frame line 39
  16. def OAI.CurrentKS.FoldRoutine.prepend line 40
  17. def OAI.CurrentKS.FoldRoutine.save line 41
  18. def OAI.CurrentKS.FoldRoutine.finish line 42
  19. def OAI.CurrentKS.FoldRoutine.body line 47
  20. def OAI.CurrentKS.FoldRoutine.scan line 51
  21. def OAI.CurrentKS.FoldRoutine.program line 54
  22. lemma OAI.CurrentKS.FoldRoutine.state_ports line 58
  23. lemma OAI.CurrentKS.FoldRoutine.state_other line 63
  24. lemma OAI.CurrentKS.FoldRoutine.setup_spec line 68
  25. lemma OAI.CurrentKS.FoldRoutine.decode_spec line 87
  26. lemma OAI.CurrentKS.FoldRoutine.frame_spec line 95
  27. lemma OAI.CurrentKS.FoldRoutine.prepend_spec line 103
  28. lemma OAI.CurrentKS.FoldRoutine.save_spec line 112
  29. lemma OAI.CurrentKS.FoldRoutine.finish_spec line 120
  30. def OAI.CurrentKS.FoldRoutine.bodyTicks line 129
  31. lemma OAI.CurrentKS.FoldRoutine.body_spec line 134
  32. def OAI.CurrentKS.FoldRoutine.scanTicks line 149
  33. lemma OAI.CurrentKS.FoldRoutine.scan_trace line 153
  34. def OAI.CurrentKS.FoldRoutine.ticks line 167
  35. def OAI.CurrentKS.FoldRoutine.routine line 172