OAI/Analysis/MatrixSigning/Machines/FixedDotControl.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W12.FixedDot.registers line 11
2. def OAI.KS.W12.FixedDot.boundary line 15
3. def OAI.KS.W12.FixedDot.guard line 18
4. def OAI.KS.W12.FixedDot.loopProgram line 21
5. def OAI.KS.W12.FixedDot.loopConfig line 23
6. theorem OAI.KS.W12.FixedDot.step_empty line 27
7. theorem OAI.KS.W12.FixedDot.step_cons line 38
8. theorem OAI.KS.W12.FixedDot.step_pair line 53
9. def OAI.KS.W12.FixedDot.loopTicks line 62
10. theorem OAI.KS.W12.FixedDot.run_loop_of_body_spec line 66
11. theorem OAI.KS.W12.FixedDot.transient_stack_bound line 100
12. theorem OAI.KS.W12.FixedDot.loop_table_length line 109