read eval

import Definitions.Def_ResourceScheduling_Graph_ReductionProgram
open ResourceScheduling.Graph GraphReg

namespace ResourceScheduling.Graph
theorem read_eval (a b dst : GraphReg) (h : b ≠ index) (s : RAMState GraphReg) :
    (GraphProgram.read a b dst h).eval s =
      let z := s.val a * s.val n + s.val b
      (s.set index z).set dst (if s.word.getD z Letter.sep = Letter.one then 1 else 0) := by sorry
end ResourceScheduling.Graph