OAI/Analysis/MatrixSigning/Arithmetic/RationalAddProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W13.RationalAdd.preNormalizeProgram line 13
  2. def OAI.KS.W13.RationalAdd.preNormalizeTicks line 16
  3. def OAI.KS.W13.RationalAdd.rawInputSum line 23
  4. theorem OAI.KS.W13.RationalAdd.preNormalize_spec line 26
  5. def OAI.KS.W13.RationalAdd.payloadBound line 35
  6. theorem OAI.KS.W13.RationalAdd.rawInputSum_bounds line 37
  7. def OAI.KS.W13.RationalAdd.normalizeProgram line 56
  8. def OAI.KS.W13.RationalAdd.serializeProgram line 59
  9. def OAI.KS.W13.RationalAdd.outputState line 62
  10. def OAI.KS.W13.RationalAdd.program line 65
  11. def OAI.KS.W13.RationalAdd.machine line 67
  12. def OAI.KS.W13.RationalAdd.totalTicks line 69
  13. theorem OAI.KS.W13.RationalAdd.full_spec line 77
  14. theorem OAI.KS.W13.RationalAdd.output_length_le line 99