fact: Definition exec (t : table) (st:State) : option State := do instr <- lookupInstr st; match instr, st with | BCall n, St μ m (x @ l :: σ) (xpc@lpc) => match run_tmr t OpBCall <|l|> lpc with | Some (Some rl, rpcl) => let pc' := x @ rpcl in let ret_pc := (xpc + 1 @ rl) in do σ' <- insert σ n ret_pc; Some (St μ m σ' pc') | _ => None end | BRet, St μ m ((ax@al)::σ) (xpc@lpc) => do tmp <- findRet σ; let '(xrpc @ lrpc, σ') := tmp in match run_tmr t OpBRet <|lrpc; al|> lpc with | Some (Some rl, rpcl) => let pc' := xrpc @ rpcl in Some (St μ m ((ax@rl)::σ') pc') | _ => None end | Load, St μ m ((x @ l) :: σ) (xpc@lpc) => do a <- nth m x; let '(ax @ al) := a in match run_tmr t OpLoad <|al; l|> lpc with | Some (Some rl, rpcl) => Some (St μ m ((ax @ rl)::σ) ((xpc+1) @ rpcl)) | _ => None end | Store, St μ m ((x @ lx) :: (a@la) :: σ) (xpc@lpc) => do inMem <- nth m x; match run_tmr t OpStore <|lx; la; ∂inMem|> lpc with | Some (Some rl, rpcl) => do m' <- upd m x (a@rl); Some (St μ m' σ ((xpc+1)@rpcl)) | _ => None end | Push r, St μ m σ (xpc@lpc) => match run_tmr t OpPush <||> lpc with | Some (Some rl, rpcl) => Some (St μ m ((r@rl)::σ) ((xpc+1)@rpcl)) | _ => None end | Nop, St μ m σ (xpc@lpc) => match run_tmr t OpNop <||> lpc with | Some (_, rpcl) => Some (St μ m σ ((xpc+1)@rpcl)) | _ => None end | Add, St μ m ((x @ lx) :: (y @ ly) :: σ) (xpc@lpc) => match run_tmr t OpAdd <|lx ; ly|> lpc with | Some (Some rl, rpcl) => Some (St μ m (((x + y) @ rl) :: σ) ((xpc+1)@rpcl)) | _ => None end | _,_ => None end.
imports: ZArith List MSetPositive