fact: Definition fast_step_fun task s: option State := match task with | SchedProc n => match s n with | Build_NodeState (KVStore.put _ k v p) u d r m => let u' := u ++ [(t_put k v d)] in let d' := (put_id n (List.length u')) :: d in let r' := SysPredefs.override r n ((r n) + 1) in let m' := SysPredefs.override m k (entry v n (List.length u') nil) in Some (SysPredefs.override s n (node_state p u' d' r' m')) | Build_NodeState (KVStore.get _ k p) u d r m => let n'' := entry_nid (m k) in let d' := if Nat.eqb n'' max_nid then d else d ++ [put_id n'' (entry_clock (m k))] ++ entry_dep (m k) in Some (SysPredefs.override s n (node_state (p (entry_val (m k))) u d' r m)) | Build_NodeState (KVStore.fault _) u d r m => Some (SysPredefs.override s n (node_state skip u d r m)) | _ => None end | SchedUpdate n1 n2 => match s n1, s n2 with | Build_NodeState p_1 u_1 d_1 r_1 m_1, Build_NodeState p_2 u_2 d_2 r_2 m_2 => let d := t_put_dep (List.nth (r_1 n2) u_2 dummy_t_put) in if negb (Nat.eqb n1 n2) && Nat.ltb (r_1 n2) (List.length u_2) && List.forallb (fun pid => Nat.leb (put_id_clock pid) (r_1 (put_id_nid pid))) d then let x:= List.nth (r_1 n2) u_2 dummy_t_put in let k := t_put_key x in let v := t_put_val x in let r_1' := SysPredefs.override r_1 n2 ((r_1 n2) + 1) in let m_1' := SysPredefs.override m_1 k (entry v n2 (r_1' n2) d) in Some ( SysPredefs.override (SysPredefs.override s n1 (node_state p_1 u_1 d_1 r_1' m_1')) n2 (node_state p_2 u_2 d_2 r_2 m_2)) else None end end%list%bool.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)