Cacher is the code snippet organizer for pro developers

let incoming_msg_garbled state = 
  match state.incoming_fix_msg with
  | Some (Garbled) -> true  
  | _ -> false
  
theorem garbled_are_ignored ( state : fix_engine_state ) =
  let state' = one_step (state) in  
  let msg_ignored = state' = {state with incoming_fix_msg = None} in
  let no_internal_msgs = state.incoming_int_msg = None in
  let ready_to_receive = 
    not ( state.fe_curr_mode = CacheReplay 
       || state.fe_curr_mode = Retransmit 
       || state.fe_curr_mode = GapDetected 
       || state.fe_curr_mode = ShuttingDown 
    ) in
  ( incoming_msg_garbled state
  && ready_to_receive
  && no_internal_msgs )
  ==> msg_ignored