OAI/Analysis/MatrixSigning/Machines/FixedDotMachine.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W12.FixedDot.pushDispatch line 9
2. def OAI.KS.W12.FixedDot.pushProgram line 13
3. def OAI.KS.W12.FixedDot.pushAfter line 15
4. theorem OAI.KS.W12.FixedDot.push_spec line 18
5. def OAI.KS.W12.FixedDot.«initialize» line 41
6. def OAI.KS.W12.FixedDot.initialStacks line 45
7. theorem OAI.KS.W12.FixedDot.initialize_spec line 47
8. def OAI.KS.W12.FixedDot.program line 61
9. def OAI.KS.W12.FixedDot.machine line 62
10. def OAI.KS.W12.FixedDot.totalTicks line 64
11. theorem OAI.KS.W12.FixedDot.full_spec line 66
12. theorem OAI.KS.W12.FixedDot.machine_stackCount line 72
13. theorem OAI.KS.W12.FixedDot.machine_inputStack line 73
14. theorem OAI.KS.W12.FixedDot.machine_outputStack line 74
15. theorem OAI.KS.W12.FixedDot.init_eq line 76
16. theorem OAI.KS.W12.FixedDot.run_input line 85
17. theorem OAI.KS.W12.FixedDot.output_correct line 90
18. theorem OAI.KS.W12.FixedDot.scratch_cleared line 97
19. theorem OAI.KS.W12.FixedDot.transient_payload line 103