OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredQueryCells.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Executed stored-mask query continuation cells

Membership and local-code recursion are instrumented below. The incidence array is shared; each of the two subsequent binary searches is tail recursive and carries only its array pointer, cut, counter and scalar endpoints.

  1. def OAI.LowSpaceSubsetSum.StoredQueryCells.member line 16
  2. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.member_value line 24
  3. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.member_cells line 30
  4. def OAI.LowSpaceSubsetSum.StoredQueryCells.code line 36
  5. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.code_value line 44
  6. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.code_cells line 50
  7. def OAI.LowSpaceSubsetSum.StoredQueryCells.localCode line 63
  8. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.localCode_value line 72
  9. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.localCode_cells line 86
  10. def OAI.LowSpaceSubsetSum.StoredQueryCells.lookup line 93
  11. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.lookup_value line 98
  12. def OAI.LowSpaceSubsetSum.StoredQueryCells.query line 105

    Source documentation

    Binary search allocates no list; its tail-state and both saved scalar cutoffs are covered by the additional 32 cells.

    def query (row : Vector (Fin n) g) (x : StoredEntry n)
    (store : Array (Array ℕ)) (hs : store.size = 2 ^ g)
    (steps lo hi : ℕ) : (Bool × ℕ) × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.StoredEntry

  13. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.query_value line 112
  14. theorem OAI.LowSpaceSubsetSum.StoredQueryCells.query_cells line 120