OAI/Combinatorics/LowSpaceSubsetSum/Word/WordCandidateExecution.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Materializing the actual words used by bounded rejection

The modulus is an already computed scalar argument. Each tail step reads one word, reduces it modulo that scalar, and pushes the result into the candidate array. The array is retained as part of the successful seed. The counter charges five scalar operations per step and the final return; the cell trace permits both the old and new array during a push.

  1. def OAI.LowSpaceSubsetSum.WordCandidateExecution.low line 19
  2. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.low_eq line 22
  3. structure OAI.LowSpaceSubsetSum.WordCandidateExecution.Raw line 27
  4. def OAI.LowSpaceSubsetSum.WordCandidateExecution.loop line 33
  5. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.loop_data line 42
  6. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.loop_size line 63
  7. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.loop_cursor line 69
  8. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.loop_work line 81
  9. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.loop_cells line 95
  10. structure OAI.LowSpaceSubsetSum.WordCandidateExecution.Buffer line 111
  11. def OAI.LowSpaceSubsetSum.WordCandidateExecution.run line 117
  12. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.run_data line 124
  13. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.run_cursor line 134
  14. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.run_work line 138
  15. theorem OAI.LowSpaceSubsetSum.WordCandidateExecution.run_cells line 142