read safe
ProvedResourceScheduling.Graph.read_safealgorithmspolynomial-time
Matrix lookup keeps every numeric register bounded when both indices and the dimension are bounded by N and the global bound exceeds N squared plus N.
Preamble
import Definitions.Def_ResourceScheduling_Graph_ReductionProgram import Definitions.Def_ResourceScheduling_Graph_RAMSafe open ResourceScheduling.Graph GraphReg
Formal statement
namespace ResourceScheduling.Graph
theorem read_safe (a b dst : GraphReg) (h : b ≠ index) (B N : ℕ) (s : RAMState GraphReg)
(hs : RAMBound B s) (ha : s.val a ≤ N) (hn : s.val n ≤ N) (hb : s.val b ≤ N)
(hB : N * N + N ≤ B) (hpos : 1 ≤ B) : RAMSafe (GraphProgram.read a b dst h) B s := by sorry
end ResourceScheduling.GraphSource
New auxiliary formalization for the ResourceScheduling Q2 reduction. The target is the unchanged CookPvsNP one-tape machine model, following Cook, The P versus NP problem, Clay Mathematics Institute (2000), Appendix. This explicit finite-column stack compiler and its simulation lemmas are new contributions, not numbered claims from Cook or the scheduling source paper.