program run
ProvedResourceScheduling.Graph.program_runalgorithmspolynomial-time
The entire fixed register program produces exactly the total word-program output in reversed storage and executes within the stated quadratic bound on every numeric register and input suffix.
Preamble
import Definitions.Def_ResourceScheduling_Graph_ReductionProgram import Definitions.Def_ResourceScheduling_Graph_RAMFields import Definitions.Def_ResourceScheduling_Graph_RAMSafe open ResourceScheduling.Graph GraphReg GraphProgram
Formal statement
namespace ResourceScheduling.Graph
theorem program_run (B L : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
(hL : s.word.length ≤ L) (hB : 9 * L * L + 3 * L + 2 ≤ B) :
RAMSafe program B s ∧ (program.eval s).out = (wordProgram s.word).reverse ++ s.out := 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.