OAI/Analysis/MatrixSigning/Optimization/StoredWitnessLift.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W12.StoredWitnessLift.saved line 10
  2. def OAI.KS.W12.StoredWitnessLift.work line 14
  3. def OAI.KS.W12.StoredWitnessLift.padPorts line 18
  4. def OAI.KS.W12.StoredWitnessLift.headPorts line 19
  5. def OAI.KS.W12.StoredWitnessLift.copyPorts line 20
  6. def OAI.KS.W12.StoredWitnessLift.framePorts line 21
  7. def OAI.KS.W12.StoredWitnessLift.headProgram line 22
  8. def OAI.KS.W12.StoredWitnessLift.program line 24
  9. def OAI.KS.W12.StoredWitnessLift.headBudget line 29
  10. def OAI.KS.W12.StoredWitnessLift.ticks line 32
  11. theorem OAI.KS.W12.StoredWitnessLift.full_spec line 39
  12. def OAI.KS.W12.StoredWitnessLift.inputLength line 94
  13. theorem OAI.KS.W12.StoredWitnessLift.headBudget_le line 97
  14. theorem OAI.KS.W12.StoredWitnessLift.runSpec_stack_length_le line 113
  15. theorem OAI.KS.W12.StoredWitnessLift.head_length_le_budget line 125
  16. theorem OAI.KS.W12.StoredWitnessLift.ticks_polynomial line 134
  17. theorem OAI.KS.W12.StoredWitnessLift.polynomial_spec line 149