Exploring The Apple FaceTime Bug with ReasonML State Machines

The Apple FaceTime bug swept the news in early 2019 - callers using FaceTime were able to hear the microphone of a new participant being added to a call, before the new participant had accepted the incoming call request. Yikes!

@DavidKPiano recently wrote a very interesting Medium article about the bug, using it to illustrate the dangers of implicit state machines in your codebase. David's post presents a strong case for explicitly identifying your state machines - by making them a prominent part of your design and your code itself, your thinking about changes becomes more robust. I encourage you to check out his post and also his JS library xstate!

I'm going to explore the adapted example from that post from a slightly different angle - we'll look at various ways of encoding his example as a state machine in ReasonML code, and show how this process can help us prevent invalid states from being admitted in the first place. We'll also have a look at using Imandra to verify properties of our state machines.

I'll also add that we're in no way making any assumptions or judgements about how Apple employees actually develop FaceTime here - this post is more to illustrate that these kind of bugs are pervasive, and the more tools we have to help eliminate them, the better.

Overall, I hope to reiterate David's message that state machines are a very useful tool for modelling parts of your applications. Writing them explicitly and using a tool like xstate can help make it easier for you to reason about your system, but it turns out they also make it easier for computers to reason about your system too! Let's dive in.

Remember, you can hit 'Try this!' to open an interactive notebook and play around with the model yourself.

A simplified call model

Let's start with some simple types represeting actions in an application for receiving incoming calls. We'll assume that once remote users make it into the peopleInCall list, they can hear the microphone of the phone running the app:

In [1]:
type person = int;

type action =
  | CallIncomingFrom(person)
  | CallAccepted
  | CallRejected
  | EndCall;
Out[1]:
type person = int
type action =
    CallIncomingFrom of person
  | CallAccepted
  | CallRejected
  | EndCall

We can receive incoming calls from a person, accept or reject an incoming call, and then end a call. So far so good - next, let's come up with a state type for these actions to act on:

In [2]:
type status =
  | Idle
  | CallActive
  | CallIncoming;

type state = {
  status: status,
  callIncomingFrom: option(person),
  peopleInCall: list(person),
};
Out[2]:
type status = Idle | CallActive | CallIncoming
type state = {
  status : status;
  callIncomingFrom : person option;
  peopleInCall : person list;
}

Nothing looks too out of the ordinary here - these are all fields we're likely to need as our app runs. Now let's write the core state update logic:

In [3]:
let update = (state: state, action): state =>
  switch (action) {
  | CallIncomingFrom(person) => {...state, status: CallIncoming, callIncomingFrom: Some(person)}
  | CallRejected => {...state, status: Idle, callIncomingFrom: None}
  | CallAccepted =>
    switch (state.callIncomingFrom) {
    | Some(p) => {status: CallActive, callIncomingFrom: None, peopleInCall: [p]}
    | None => state
    }
  | EndCall => {...state, status: Idle, peopleInCall: []}
  };
Out[3]:
val update : state -> action -> state = <fun>

This function represents the transitions of a state machine!

Encoding this in the Reason/OCaml type system gives us a couple of advantages - the switch statement (match in OCaml syntax) can also check that we've exhaustively covered all the actions. Also, if we decide to wire this up to a React UI, ReasonML's React bindings include a ReducerComponent out of the box that expects a function of this shape. React's new Hooks API also has a similar primitive in the form of the useReducer Hook.

Changing the model

Now let's imagine a new requirement comes in.

Handle messages from the system requesting new people be added to a call.

Let's give that a go. We'll add a new action AddPerson representing the system message:

In [4]:
type action_v2 =
  | CallIncomingFrom(person)
  | CallAccepted
  | CallRejected
  | EndCall
  | AddPerson(person);
Out[4]:
type action_v2 =
    CallIncomingFrom of person
  | CallAccepted
  | CallRejected
  | EndCall
  | AddPerson of person
In [5]:
let update_v2 = (state: state, action: action_v2): state =>
  switch (action) {
  | CallIncomingFrom(person) => {...state, status: CallIncoming, callIncomingFrom: Some(person)}
  | CallRejected => {...state, status: Idle, callIncomingFrom: None}
  | CallAccepted =>
    switch (state.callIncomingFrom) {
    | Some(p) => {status: CallActive, callIncomingFrom: None, peopleInCall: [p]}
    | None => state
    }
  | EndCall => {...state, status: Idle, peopleInCall: []}
  | AddPerson(person) => {...state, peopleInCall: [person, ...state.peopleInCall]}
  };
Out[5]:
val update_v2 : state -> action_v2 -> state = <fun>

We'll even write a test for it:

In [6]:
type test_outcome = | Pass | Fail;

let test_add_person_action = {
  let start_state = { status: CallActive, peopleInCall: [1, 2], callIncomingFrom: None };
  let end_state = update_v2(start_state, AddPerson(3));
  if (List.exists(x => x == 3, end_state.peopleInCall) && end_state.status == CallActive) {
      Pass
  } else {
      Fail
  }
};
Out[6]:
type test_outcome = Pass | Fail
val test_add_person_action : test_outcome = Pass

...and all is right with the world. Or is it? If you look carefully, we've baked into our test an assumption about the starting status of the state when handling the AddPerson action - something that's easily done if we've got our feature implementation blinkers on.

What the test misses is the AddPerson action being used in a state that isn't CallActive. As nothing actually validates that the state is correct, we could potentially end up having a person added to peopleInCall before the call is accepted - similar to what happened with the real bug.

The ideal approach

Although the type system has helped us out here a bit, we can leverage it even further by writing our states in a way that makes expressing this bug impossible in the first place.

In [7]:
type call = {people: list(person)};

type ideal_state =
  | Idle
  | CallActive(call)
  | CallIncoming(person);
Out[7]:
type call = { people : person list; }
type ideal_state = Idle | CallActive of call | CallIncoming of person

Here we're using a variant type to represent mutually exclusive bits of state. This means we can't have any call state unless we're actually in an active call, and similarly it eliminates some possible uncertainty in the CallIncoming state about the person we're receiving the call from.

We also define a type for the outcome of an update:

In [8]:
type update_outcome('a) =
  | Updated('a)
  | Invalid;
Out[8]:
type 'a update_outcome = Updated of 'a | Invalid

Previously we only returned the original state for unexpected actions (returning state for the state.callIncomingFrom == None branch of the CallAccepted action, in update_v2). We know intuitively this shouldn't happen, but let's use the type system to our advantage by explicitly making cases like that an invalid outcome. That way the code that's actually running our state machine can check for invalid outcomes and log an error message to let us know that something is wired up incorrectly, which may indicate another bug somewhere.

Now let's use these new types in our new and improved update function:

In [9]:
let ideal_update = (state: ideal_state, action : action_v2): update_outcome(ideal_state) =>
  switch (state, action) {
  | (Idle, CallIncomingFrom(p)) => Updated(CallIncoming(p))
  | (CallIncoming(_), CallRejected) => Updated(Idle)
  | (CallIncoming(p), CallAccepted) => Updated(CallActive({people: [p]}))
  | (CallActive(_), EndCall) => Updated(Idle)
  | (CallActive(call), AddPerson(p)) =>
    Updated(CallActive({people: [p, ...call.people]}))
  | _ => Invalid
  };
Out[9]:
val ideal_update : ideal_state -> action_v2 -> ideal_state update_outcome =
  <fun>

The types have actually guided us here to make our transition function more correct - we are now forced to switch on both the action coming in and the current state in order to have access to the call state that we need to update when adding a new person to the call.

Meeting halfway

While this representation is ideal for this small example, we can't always quite pull this off. Sometimes we simply can't express the type of constraint we want, due to the limitations of the type system. Sometimes we can, but by doing so we make the code unreadable or very unwieldy to use. Alternatively, we may have started with the original representation, but have too much code dependent on it to be able to make the change under given time constraints (although the Reason/OCaml type system would definitely help with the refactoring!). So let's not let the 'perfect' be the enemy of the good - instead, let's take a step back to the original version of our update function in order to demonstrate what it looks like to meet somewhere in the middle.

One way of looking at static type systems like this is as tools for proving properties of your code at compile time. By writing our code in a way that satisfies the rules of the type system, we're given a certain class of guarantees about our programs - the tradeoff is that we lose some expressiveness. In our ideal representation we can no longer express certain invalid states, which is what we want! But sometimes by following the rules of the type system we find it hard to express certain things that we do want.

If we're using Reason/OCaml, we have another option - we can use Imandra, a cloud-native automated reasoning engine.

Like a type system, Imandra is also a tool that can be used to prove that properties of your program hold true, but we can express these properties themselves as snippets of Reason/OCaml code. This allows us to direct the checking process in a way that's much more tailored to the domain of the program itself, rather than on the more generic language level.

What does this all mean? Let's start by writing a property, or verification goal, about our earlier implementation update_v2:

In [10]:
let add_person_property =
    (state: state, person: int) => {
  let new_state = update_v2(state, AddPerson(person));
  if (List.length(new_state.peopleInCall) > 0) {
    new_state.status == CallActive;
  } else {
    true;
  };
};
Out[10]:
val add_person_property : state -> int -> bool = <fun>

This is a function that takes an arbitrary state and person, performs some actions on them, and then returns true or false to indicate whether the property holds. So here we're saying that if there are people in the call after responding to the AddPerson message, we're in the CallActive state, which is a nice general concept we'd like to be true! We are specifically testing the action that we know is broken here, but let's accept that for now and see what happens when we ask Imandra to verify the property for us (we're specifying a max unrolling depth for verification of 50 with the ~upto flag - we'll come back to this later):

In [11]:
verify ~upto=50 add_person_property;
Out[11]:
- : state -> int -> bool = <fun>
module CX : sig val state : state val person : int end
Counterexample (after 2 steps, 0.044s):
 let (state : state) =
   {status = Idle; callIncomingFrom = None; peopleInCall = []}
 let (person : int) = 2
Refuted
proof attempt
ground_instances2
definitions0
inductions0
search_time
0.044s
details
Expand
smt_stats
num checks5
arith assert lower3
arith pivots1
rlimit count1063
mk clause7
datatype occurs check18
mk bool var42
arith assert upper2
datatype splits9
decisions11
propagations4
conflicts4
arith fixed eqs1
datatype accessor ax12
datatype constructor ax13
num allocs1672378
final checks6
added eqs37
del clause3
arith eq adapter2
memory8.110000
max memory8.110000
Expand
  • start[0.044s]
      if List.length
         (if AddPerson :var_0: = CallRejected then … else …).peopleInCall > 
         0
      then
        (if AddPerson :var_0: = CallRejected then … else …).status =
        CallActive
      else true
  • simplify

    into
    List.length (:var_0: :: :var_1:.peopleInCall) <= 0
    || :var_1:.status = CallActive
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|List.length_1177| (|::_3| person_76 (peopleInCall_27 state_75)))
        expansions
        • unroll
          expr
          (|List.length_1177|
            (|get.::.1_1174| (|::_3| person_76 (peopleInCall_27 state_75))))
          expansions
          • Sat (Some let (state : state) = {status = Idle; callIncomingFrom = None; peopleInCall = []} let (person : int) = 2 )

          Imandra analyses our code symbolically and we don't just get a pass/failure result - we get concrete counterexample values for the inputs to our function that illustrate the flaw in our thinking. If we want, we can compute and experiment with them (which can be very useful for investigating bugs Imandra has found):

          In [12]:
          List.length(CX._x_0.peopleInCall);
          
          Out[12]:
          File "jupyter cell 12", line 1, characters 12-19:
          Error: Unbound value CX._x_0
          

          As we said, the goal above is fairly focused in on our new feature, and we've written it already knowing there's a bug in the area we're targeting - let's work with something that's more universal, helped by the fact that we've modeled things as a state machine. A helpful pattern when dealing with state machines is to check that properties hold under arbitrary sequences of actions:

          In [13]:
          let call_with_people_in_is_active_property = (update_fn, initial_state, actions : list('a)) => {
            let final_state = List.fold_left(update_fn, initial_state, actions);
            if (List.length(final_state.peopleInCall) > 0) {
              final_state.status == CallActive;
            } else {
              true;
            };
          };
          
          Out[13]:
          val call_with_people_in_is_active_property :
            (state -> 'a -> state) -> state -> 'a list -> bool = <fun>
          

          This checks the same underlying idea that we never have more than 0 people in the call unless the call is active, but in a more general way - we no longer check the single specific action. The nice thing about properties like this is that we can imagine that we'd still want them to hold true as we make additional changes to our state machine, and staying decoupled from specific actions helps us achieve that.

          We simulate actions run in a react-like reducer using a fold (fold and reduce are synonymous). We're also passing in a target update_fn as we're going to use it on multiple versions of update as we progress. Imandra will check that the property holds for all possible values of the type 'list of actions' (the last parameter to our property function). Let's try it out:

          In [14]:
          let initial_state = { status: Idle, callIncomingFrom: None, peopleInCall: [] };
          verify ~upto=50 call_with_people_in_is_active_property(update_v2, initial_state);
          
          Out[14]:
          val initial_state : state =
            {status = Idle; callIncomingFrom = None; peopleInCall = []}
          - : action_v2 list -> bool = <fun>
          module CX : sig val _x_0 : action_v2 list end
          
          Counterexample (after 4 steps, 0.039s):
           let (_x_0 : action_v2 list) = [(AddPerson (4))]
          
          Refuted
          proof attempt
          ground_instances4
          definitions0
          inductions0
          search_time
          0.039s
          details
          Expand
          smt_stats
          num checks9
          arith assert lower5
          arith pivots1
          rlimit count5486
          mk clause46
          datatype occurs check292
          mk bool var276
          arith assert upper3
          datatype splits55
          decisions208
          arith add rows1
          propagations172
          conflicts26
          arith fixed eqs5
          datatype accessor ax56
          arith assert diseq2
          datatype constructor ax67
          num allocs4962364
          final checks20
          added eqs377
          del clause6
          arith eq adapter6
          memory8.900000
          max memory8.900000
          Expand
          • start[0.039s]
              if List.length
                 (List.fold_left update_v2
                  {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).peopleInCall
                 > 0
              then
                (List.fold_left update_v2
                 {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).status
                = CallActive
              else true
          • simplify

            into
            List.length
            (List.fold_left update_v2
             {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).peopleInCall
            <= 0
            || (List.fold_left update_v2
                {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).status
               = CallActive
            expansions
            []
            rewrite_steps
              forward_chaining
              • unroll
                expr
                (|`List.fold_left update_v2[0]`_1242|
                  (|rec_mk.state_1232| Idle_21 None_4 |[]_2|)
                  _x_0_85)
                expansions
                • unroll
                  expr
                  (|List.length_1247|
                    (peopleInCall_27 (|`List.fold_left update_v2[0]`_1242|
                                       (|…
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (|get.::.1_1237| (peopleInCall_27 (|`List.fold_left update_v2[0]`_1242|
                                     …
                    expansions
                    • unroll
                      expr
                      (let ((a!1 (|rec_mk.state_1232|
                                   CallIncoming_23
                                   (Some_5 (|get.CallIncoming…
                      expansions
                      • Sat (Some let (_x_0 : action_v2 list) = [(AddPerson (4))] )

                      The sequence of actions with a single AddPerson item already contradicts our property, which immediately shows us our issue and gives us an example to help out:

                      In [15]:
                      update_v2(initial_state, AddPerson(4));
                      
                      Out[15]:
                      - : state = {status = Idle; callIncomingFrom = None; peopleInCall = [4]}
                      

                      Let's try running the same property on our original update function, from before we added the new AddPerson action:

                      In [16]:
                      verify ~upto=50 call_with_people_in_is_active_property(update, initial_state);
                      
                      Out[16]:
                      - : action list -> bool = <fun>
                      module CX : sig val _x_0 : action list end
                      
                      Counterexample (after 7 steps, 0.033s):
                       let (_x_0 : action list) =
                         [(CallIncomingFrom (4)); CallAccepted; (CallIncomingFrom (5))]
                      
                      Refuted
                      proof attempt
                      ground_instances7
                      definitions0
                      inductions0
                      search_time
                      0.033s
                      details
                      Expand
                      smt_stats
                      arith offset eqs15
                      num checks15
                      arith assert lower40
                      arith pivots26
                      rlimit count13631
                      mk clause139
                      datatype occurs check632
                      mk bool var810
                      arith assert upper58
                      datatype splits159
                      decisions429
                      arith add rows65
                      arith bound prop4
                      propagations506
                      conflicts61
                      arith fixed eqs66
                      datatype accessor ax142
                      minimized lits4
                      arith assert diseq22
                      datatype constructor ax181
                      num allocs10192548
                      final checks40
                      added eqs1629
                      del clause70
                      arith eq adapter51
                      memory9.530000
                      max memory9.530000
                      Expand
                      • start[0.033s]
                          if List.length
                             (List.fold_left update
                              {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).peopleInCall
                             > 0
                          then
                            (List.fold_left update
                             {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).status
                            = CallActive
                          else true
                      • simplify

                        into
                        List.length
                        (List.fold_left update
                         {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).peopleInCall
                        <= 0
                        || (List.fold_left update
                            {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).status
                           = CallActive
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|`List.fold_left update[0]`_1331|
                              (|rec_mk.state_1321| Idle_21 None_4 |[]_2|)
                              _x_0_87)
                            expansions
                            • unroll
                              expr
                              (|List.length_1336|
                                (peopleInCall_27 (|`List.fold_left update[0]`_1331|
                                                   (|rec…
                              expansions
                              • unroll
                                expr
                                (let ((a!1 (|get.::.1_1326| (peopleInCall_27 (|`List.fold_left update[0]`_1331|
                                                    …
                                expansions
                                • unroll
                                  expr
                                  (let ((a!1 (|rec_mk.state_1321|
                                               CallIncoming_23
                                               (Some_5 (|get.CallIncoming…
                                  expansions
                                  • unroll
                                    expr
                                    (let ((a!1 (|get.::.1_1326| (peopleInCall_27 (|`List.fold_left update[0]`_1331|
                                                        …
                                    expansions
                                    • unroll
                                      expr
                                      (let ((a!1 (Some_5 (|get.CallIncomingFrom.0_1317|
                                                           (|get.::.0_1319| (|get.::.1_1…
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 ((_ is (CallIncomingFrom_16 (Int) action_15))
                                                     (|get.::.0_1319| (|get.::.1_13…
                                        expansions
                                        • Sat (Some let (_x_0 : action list) = [(CallIncomingFrom (4)); CallAccepted; (CallIncomingFrom (5))] )

                                        This reveals another case we hadn't considered! We don't handle the CallIncomingFrom action from the CallActive state - it drops us straight out of CallActive back into CallIncoming while leaving people in the call, which might not be what we want.

                                        In [17]:
                                        update(update(update(initial_state, CallIncomingFrom(4)), CallAccepted), CallIncomingFrom(5));
                                        
                                        Out[17]:
                                        - : state =
                                        {status = CallIncoming; callIncomingFrom = Some 5; peopleInCall = [4]}
                                        

                                        Now we know there's a problem, we can re-work our update logic to accommodate. We learnt earlier while working on our 'ideal' representation that checking the current state is a good idea, so let's incorporate that here:

                                        In [18]:
                                        let good_update = (state: state, action: action_v2): state =>
                                          switch (state.status, action) {
                                          | (Idle, CallIncomingFrom(person)) =>
                                            {...state, status: CallIncoming, callIncomingFrom: Some(person)}
                                          | (CallIncoming, CallRejected) =>
                                            {...state, status: Idle, callIncomingFrom: None}
                                          | (CallIncoming, CallAccepted) =>
                                            switch (state.callIncomingFrom) {
                                            | Some(p) =>
                                              {status: CallActive, callIncomingFrom: None, peopleInCall: [p]}
                                            | _ => state
                                            }
                                        
                                          | (CallActive, AddPerson(p)) =>
                                            {...state, peopleInCall: [p, ...state.peopleInCall]}
                                          | (CallActive, EndCall) =>
                                            {...state, status: Idle, peopleInCall: []}
                                          | _ => state
                                          };
                                        
                                        Out[18]:
                                        val good_update : state -> action_v2 -> state = <fun>
                                        

                                        Next, let's check it with our general property:

                                        In [19]:
                                        verify ~upto=50 call_with_people_in_is_active_property(good_update, initial_state);
                                        
                                        Out[19]:
                                        - : action_v2 list -> bool = <fun>
                                        
                                        Proved up to 50 steps

                                        Imandra's standard unrolling verification method can't find any issues up to our fairly high bound of 50 here. Although it hasn't totally proved things for us, this is a good indicator that we're on the right lines as it can't find any counterexamples. It's pretty hard for us to prove things completely in this case using this method, due to the nature of our property - as the list of actions is arbitrary and our state machine contains cycles, there are valid sequences of actions that are infinite, for example [CallIncoming(1), CallAccepted, EndCall, CallIncoming(1), CallAccepted, EndCall, ...].

                                        If we want to increase our level of confidence even further, we can spend a bit longer to get a complete proof. In this case we can try Imandra's [@auto] method, which performs a proof by induction for all possible inputs:

                                        In [20]:
                                        [@auto] verify call_with_people_in_is_active_property(good_update, initial_state);
                                        
                                        Out[20]:
                                        - : action_v2 list -> bool = <fun>
                                        Goal:
                                        
                                        call_with_people_in_is_active_property good_update initial_state _x_0.
                                        
                                        1 nontautological subgoal.
                                        
                                        Subgoal 1:
                                        
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        
                                        Must try induction.
                                        
                                        The recursive terms in the conjecture suggest 2 inductions.
                                        Subsumption and merging reduces this to 1.
                                        
                                        We shall induct according to a scheme derived from List.fold_left.
                                        
                                        Induction scheme:
                                        
                                         (_x_0 = [] ==> φ _x_0)
                                         && (not (_x_0 = []) && φ (List.tl _x_0) ==> φ _x_0).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.2:
                                        
                                         H0. _x_0 = []
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_left and List.length.
                                        
                                        Subgoal 1.1:
                                        
                                         H0. not (_x_0 = [])
                                         H1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_0)).peopleInCall
                                             <= 0
                                             || (List.fold_left good_update
                                                 {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                 (List.tl _x_0)).status
                                                = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to the
                                        following 2 subgoals:
                                        
                                        Subgoal 1.1.2:
                                        
                                         H0. _x_0 <> []
                                         H1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_0)).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_0)).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         _x_0 -> _x_01 :: _x_02
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2':
                                        
                                         H0. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (_x_01 :: _x_02)).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (_x_01 :: _x_02)).status
                                             = CallActive
                                        
                                        This simplifies, using the definition of List.fold_left to:
                                        
                                        Subgoal 1.1.2'':
                                        
                                         H0. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).status
                                             = CallActive
                                         H1. Is_a(CallIncomingFrom, _x_01)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).status
                                             = CallActive
                                        
                                        
                                        Candidates for generalization:
                                        
                                         List.fold_left good_update
                                         {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02
                                         List.fold_left good_update
                                         {status = CallIncoming;
                                          callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                          peopleInCall = []}
                                         _x_02
                                        
                                        However, we can refute the result of performing this generalization and thus
                                        abandon it.
                                        
                                        Hint: It may be useful to examine the abandoned generalized formula, to help
                                        you derive relevant generalization rules:
                                        
                                         H0. gen_1.status = CallActive
                                         H1. Is_a(CallIncomingFrom, _x_01)
                                        |---------------------------------------------------------------------------
                                         C0. List.length gen_1.peopleInCall <= 0
                                         C1. List.length gen_2.peopleInCall <= 0
                                         C2. gen_2.status = CallActive
                                        
                                        Must try induction.
                                        
                                        The recursive terms in the conjecture suggest 4 inductions.
                                        Subsumption and merging reduces this to 1.
                                        
                                        We shall induct according to a scheme derived from List.fold_left.
                                        
                                        Induction scheme:
                                        
                                         (_x_02 = [] ==> φ _x_02 _x_01)
                                         && (not (_x_02 = []) && φ (List.tl _x_02) _x_01 ==> φ _x_02 _x_01).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.1.2''.2:
                                        
                                         H0. _x_02 = []
                                         H1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).status
                                             = CallActive
                                         H2. Is_a(CallIncomingFrom, _x_01)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).status
                                             = CallActive
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_left and List.length.
                                        
                                        Subgoal 1.1.2''.1:
                                        
                                         H0. not (_x_02 = [])
                                         H1. (((not
                                                ((List.fold_left good_update
                                                  {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                  (List.tl _x_02)).status
                                                 = CallActive)
                                                || not Is_a(CallIncomingFrom, _x_01))
                                               || List.length
                                                  (List.fold_left good_update
                                                   {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                   (List.tl _x_02)).peopleInCall
                                                  <= 0)
                                              || List.length
                                                 (List.fold_left good_update
                                                  {status = CallIncoming;
                                                   callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                                   peopleInCall = []}
                                                  (List.tl _x_02)).peopleInCall
                                                 <= 0)
                                             || (List.fold_left good_update
                                                 {status = CallIncoming;
                                                  callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                                  peopleInCall = []}
                                                 (List.tl _x_02)).status
                                                = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).status
                                             = CallActive
                                         H3. Is_a(CallIncomingFrom, _x_01)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).status
                                             = CallActive
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to the
                                        following 4 subgoals:
                                        
                                        Subgoal 1.1.2''.1.4:
                                        
                                         H0. _x_02 <> []
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              (List.tl _x_02)).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_02)).status
                                             = CallActive
                                         H3. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).status
                                             = CallActive
                                         H4. Is_a(CallIncomingFrom, _x_01)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_02)).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              (List.tl _x_02)).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).peopleInCall
                                             <= 0
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).peopleInCall
                                             <= 0
                                         C4. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).status
                                             = CallActive
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         _x_01 -> CallIncomingFrom _x_011
                                         _x_02 -> _x_021 :: _x_022
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2''.1.4':
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (_x_021 :: _x_022)).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (_x_021 :: _x_022)).peopleInCall
                                             <= 0
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              (_x_021 :: _x_022)).peopleInCall
                                             <= 0
                                         C4. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              (_x_021 :: _x_022)).status
                                             = CallActive
                                        
                                        This simplifies, using the definition of List.fold_left to:
                                        
                                        Subgoal 1.1.2''.1.4'':
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                         H2. _x_021 = CallAccepted
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).status
                                             = CallActive
                                         C4. _x_021 = CallRejected
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to:
                                        
                                        Subgoal 1.1.2''.1.4''':
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).status
                                             = CallActive
                                        
                                        
                                        Candidates for generalization:
                                        
                                         List.fold_left good_update
                                         {status = CallIncoming; callIncomingFrom = Some _x_011; peopleInCall = []}
                                         _x_022
                                         List.fold_left good_update
                                         {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022
                                         List.fold_left good_update
                                         {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                         _x_022
                                        
                                        However, we can refute the result of performing this generalization and thus
                                        abandon it.
                                        
                                        Hint: It may be useful to examine the abandoned generalized formula, to help
                                        you derive relevant generalization rules:
                                        
                                         H0. gen_1.status = CallActive
                                         H1. gen_2.status = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length gen_2.peopleInCall <= 0
                                         C1. List.length gen_1.peopleInCall <= 0
                                         C2. List.length gen_3.peopleInCall <= 0
                                         C3. gen_3.status = CallActive
                                        
                                        Must try induction.
                                        
                                        The recursive terms in the conjecture suggest 6 inductions.
                                        Subsumption and merging reduces this to 1.
                                        
                                        We shall induct according to a scheme derived from List.fold_left.
                                        
                                        Induction scheme:
                                        
                                         (_x_022 = [] ==> φ _x_022 _x_011)
                                         && (not (_x_022 = []) && φ (List.tl _x_022) _x_011 ==> φ _x_022 _x_011).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.1.2''.1.4'''.2:
                                        
                                         H0. _x_022 = []
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).status
                                             = CallActive
                                        
                                        But simplification reduces this to true, using the definition of
                                        List.fold_left.
                                        
                                        Subgoal 1.1.2''.1.4'''.1:
                                        
                                         H0. not (_x_022 = [])
                                         H1. ((((not
                                                 ((List.fold_left good_update
                                                   {status = CallIncoming; callIncomingFrom = Some _x_011;
                                                    peopleInCall = []}
                                                   (List.tl _x_022)).status
                                                  = CallActive)
                                                 || not
                                                    ((List.fold_left good_update
                                                      {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                      (List.tl _x_022)).status
                                                     = CallActive))
                                                || List.length
                                                   (List.fold_left good_update
                                                    {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                    (List.tl _x_022)).peopleInCall
                                                   <= 0)
                                               || List.length
                                                  (List.fold_left good_update
                                                   {status = CallIncoming; callIncomingFrom = Some _x_011;
                                                    peopleInCall = []}
                                                   (List.tl _x_022)).peopleInCall
                                                  <= 0)
                                              || List.length
                                                 (List.fold_left good_update
                                                  {status = CallActive; callIncomingFrom = None;
                                                   peopleInCall = [_x_011]}
                                                  (List.tl _x_022)).peopleInCall
                                                 <= 0)
                                             || (List.fold_left good_update
                                                 {status = CallActive; callIncomingFrom = None;
                                                  peopleInCall = [_x_011]}
                                                 (List.tl _x_022)).status
                                                = CallActive
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H3. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).status
                                             = CallActive
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to the
                                        following 6 subgoals:
                                        
                                        Subgoal 1.1.2''.1.4'''.1.6:
                                        
                                         H0. _x_022 <> []
                                         H1. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              (List.tl _x_022)).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              (List.tl _x_022)).status
                                             = CallActive
                                         H3. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_022)).status
                                             = CallActive
                                         H4. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H5. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_022)).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              (List.tl _x_022)).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              (List.tl _x_022)).peopleInCall
                                             <= 0
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C4. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C5. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).peopleInCall
                                             <= 0
                                         C6. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).status
                                             = CallActive
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         _x_022 -> _x_0221 :: _x_0222
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2''.1.4'''.1.6':
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_0222).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_0222).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222).status
                                             = CallActive
                                         H3. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              (_x_0221 :: _x_0222)).status
                                             = CallActive
                                         H4. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (_x_0221 :: _x_0222)).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (_x_0221 :: _x_0222)).peopleInCall
                                             <= 0
                                         C4. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              (_x_0221 :: _x_0222)).peopleInCall
                                             <= 0
                                         C5. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              (_x_0221 :: _x_0222)).peopleInCall
                                             <= 0
                                         C6. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              (_x_0221 :: _x_0222)).status
                                             = CallActive
                                        
                                        This simplifies, using the definition of List.fold_left to:
                                        
                                        Subgoal 1.1.2''.1.4'''.1.6'':
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_0222).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_0222).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222).status
                                             = CallActive
                                         H3. Is_a(AddPerson, _x_0221)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Destruct(AddPerson, 0, _x_0221); _x_011]}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C4. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Destruct(AddPerson, 0, _x_0221); _x_011]}
                                              _x_0222).status
                                             = CallActive
                                        
                                        
                                        Candidates for generalization:
                                        
                                         List.fold_left good_update
                                         {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                         _x_0222
                                         List.fold_left good_update
                                         {status = CallIncoming; callIncomingFrom = Some _x_011; peopleInCall = []}
                                         _x_0222
                                         List.fold_left good_update
                                         {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222
                                         List.fold_left good_update
                                         {status = CallActive; callIncomingFrom = None;
                                          peopleInCall = [Destruct(AddPerson, 0, _x_0221); _x_011]}
                                         _x_0222
                                        
                                        However, we can refute the result of performing this generalization and thus
                                        abandon it.
                                        
                                        Hint: It may be useful to examine the abandoned generalized formula, to help
                                        you derive relevant generalization rules:
                                        
                                         H0. gen_1.status = CallActive
                                         H1. gen_2.status = CallActive
                                         H2. gen_3.status = CallActive
                                         H3. Is_a(AddPerson, _x_0221)
                                        |---------------------------------------------------------------------------
                                         C0. List.length gen_3.peopleInCall <= 0
                                         C1. List.length gen_2.peopleInCall <= 0
                                         C2. List.length gen_1.peopleInCall <= 0
                                         C3. List.length gen_4.peopleInCall <= 0
                                         C4. gen_4.status = CallActive
                                        
                                        Must try induction.
                                        
                                         Aborting proof attempt for _verify_target.
                                        
                                         Rules:
                                            (:def List.fold_left)
                                            (:def List.length)
                                            (:fc List.len_nonnegative)
                                            (:induct List.fold_left)
                                        
                                        Checkpoints:
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_0222).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_0222).status
                                             = CallActive
                                         H2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222).status
                                             = CallActive
                                         H3. Is_a(AddPerson, _x_0221)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0222).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Destruct(AddPerson, 0, _x_0221); _x_011]}
                                              _x_0222).peopleInCall
                                             <= 0
                                         C4. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Destruct(AddPerson, 0, _x_0221); _x_011]}
                                              _x_0222).status
                                             = CallActive
                                        
                                         H0. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).status
                                             = CallActive
                                         H1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).status
                                             = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_022).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some _x_011;
                                               peopleInCall = []}
                                              _x_022).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [_x_011]}
                                              _x_022).status
                                             = CallActive
                                        
                                         H0. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).status
                                             = CallActive
                                         H1. Is_a(CallIncomingFrom, _x_01)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_02).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, _x_01));
                                               peopleInCall = []}
                                              _x_02).status
                                             = CallActive
                                        
                                        module CX : sig val _x_01 : action_v2 val gen_2 : state val gen_1 : state end
                                        module CX : sig val gen_3 : state val gen_2 : state val gen_1 : state end
                                        module CX :
                                          sig
                                            val gen_4 : state
                                            val gen_3 : state
                                            val gen_2 : state
                                            val _x_0221 : action_v2
                                            val gen_1 : state
                                          end
                                        Error[/server]: Maximum induction depth reached (3). You can set this with #max_induct.
                                        

                                        We run into a limit here due to our use of fold_left. A common trick when using induction is to switch to using fold_right instead, which is easier to induct on (this also means the actions list is 'reduced' in reverse order, but that doesn't make a difference here):

                                        In [21]:
                                        let call_with_people_in_is_active_property_fold_right = (update_fn, initial_state, actions : list('a)) => {
                                          let final_state = List.fold_right((a, b) => update_fn(b, a), ~base=initial_state, actions);
                                          if (List.length(final_state.peopleInCall) > 0) {
                                            final_state.status == CallActive;
                                          } else {
                                            true;
                                          };
                                        };
                                        
                                        Out[21]:
                                        val call_with_people_in_is_active_property_fold_right :
                                          (state -> 'a -> state) -> state -> 'a list -> bool = <fun>
                                        
                                        In [22]:
                                        [@auto] verify(call_with_people_in_is_active_property_fold_right(good_update, initial_state));
                                        
                                        Out[22]:
                                        - : action_v2 list -> bool = <fun>
                                        Goal:
                                        
                                        call_with_people_in_is_active_property_fold_right good_update initial_state
                                        _x_0.
                                        
                                        1 nontautological subgoal.
                                        
                                        Subgoal 1:
                                        
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C1. (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        
                                        Must try induction.
                                        
                                        The recursive terms in the conjecture suggest 2 inductions.
                                        Subsumption and merging reduces this to 1.
                                        
                                        We shall induct according to a scheme derived from List.fold_right.
                                        
                                        Induction scheme:
                                        
                                         (_x_0 = [] ==> φ _x_0)
                                         && (not (_x_0 = []) && φ (List.tl _x_0) ==> φ _x_0).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.2:
                                        
                                         H0. _x_0 = []
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C1. (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_right and List.length.
                                        
                                        Subgoal 1.1:
                                        
                                         H0. not (_x_0 = [])
                                         H1. List.length
                                             (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl _x_0)).peopleInCall
                                             <= 0
                                             || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                 {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                 (List.tl _x_0)).status
                                                = CallActive
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).peopleInCall
                                             <= 0
                                         C1. (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} _x_0).status
                                             = CallActive
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_right and List.length.
                                        
                                         Rules:
                                            (:def List.fold_right)
                                            (:def List.length)
                                            (:fc List.len_nonnegative)
                                            (:induct List.fold_right)
                                        
                                        
                                        Proved
                                        proof
                                        ground_instances0
                                        definitions15
                                        inductions1
                                        search_time
                                        0.815s
                                        Expand
                                        • start[0.815s, "Goal"]
                                            if List.length
                                               (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).peopleInCall
                                               > 0
                                            then
                                              (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                               {status = …; callIncomingFrom = …; peopleInCall = …} :var_0:).status
                                              = CallActive
                                            else true
                                        • subproof

                                          List.length (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall <= 0 || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status = CallActive
                                          • start[0.815s, "1"]
                                              List.length
                                              (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                               {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall
                                              <= 0
                                              || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                  {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status
                                                 = CallActive
                                          • induction on (functional )
                                            :scheme (_x_0 = [] ==> φ _x_0)
                                                    && (not (_x_0 = []) && φ (List.tl _x_0) ==> φ _x_0)
                                          • Split (((not (_x_0 = [])
                                                     || List.length
                                                        (List.fold_right
                                                         ((fun update_fn a b -> update_fn b a) good_update)
                                                         {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall
                                                        <= 0)
                                                    || (List.fold_right
                                                        ((fun update_fn a b -> update_fn b a) good_update)
                                                        {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status
                                                       = CallActive)
                                                   && ((not
                                                        (not (_x_0 = [])
                                                         && (List.length
                                                             (List.fold_right
                                                              ((fun update_fn a b -> update_fn b a) good_update)
                                                              {status = …; callIncomingFrom = …; peopleInCall = …}
                                                              (List.tl _x_0)).peopleInCall
                                                             <= 0
                                                             || (List.fold_right
                                                                 ((fun update_fn a b -> update_fn b a) good_update)
                                                                 {status = …; callIncomingFrom = …;
                                                                  peopleInCall = …}
                                                                 (List.tl _x_0)).status
                                                                = CallActive))
                                                        || List.length
                                                           (List.fold_right
                                                            ((fun update_fn a b -> update_fn b a) good_update)
                                                            {status = …; callIncomingFrom = …; peopleInCall = …}
                                                            _x_0).peopleInCall
                                                           <= 0)
                                                       || (List.fold_right
                                                           ((fun update_fn a b -> update_fn b a) good_update)
                                                           {status = …; callIncomingFrom = …; peopleInCall = …}
                                                           _x_0).status
                                                          = CallActive)
                                                   :cases [(not (_x_0 = [])
                                                            || List.length
                                                               (List.fold_right
                                                                ((fun update_fn a b -> update_fn b a) good_update)
                                                                {status = …; callIncomingFrom = …; peopleInCall = …}
                                                                _x_0).peopleInCall
                                                               <= 0)
                                                           || (List.fold_right
                                                               ((fun update_fn a b -> update_fn b a) good_update)
                                                               {status = …; callIncomingFrom = …; peopleInCall = …}
                                                               _x_0).status
                                                              = CallActive;
                                                           ((_x_0 = []
                                                             || not
                                                                (List.length
                                                                 (List.fold_right
                                                                  ((fun update_fn a b -> update_fn b a) good_update)
                                                                  {status = …; callIncomingFrom = …;
                                                                   peopleInCall = …}
                                                                  (List.tl _x_0)).peopleInCall
                                                                 <= 0
                                                                 || (List.fold_right
                                                                     ((fun update_fn a b -> update_fn b a) good_update)
                                                                     {status = …; callIncomingFrom = …;
                                                                      peopleInCall = …}
                                                                     (List.tl _x_0)).status
                                                                    = CallActive))
                                                            || List.length
                                                               (List.fold_right
                                                                ((fun update_fn a b -> update_fn b a) good_update)
                                                                {status = …; callIncomingFrom = …; peopleInCall = …}
                                                                _x_0).peopleInCall
                                                               <= 0)
                                                           || (List.fold_right
                                                               ((fun update_fn a b -> update_fn b a) good_update)
                                                               {status = …; callIncomingFrom = …; peopleInCall = …}
                                                               _x_0).status
                                                              = CallActive])
                                            • subproof
                                              ((_x_0 = [] || not (List.length (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} (List.tl _x_0)).peopleInCall <= 0 || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} (List.tl _x_0)).status = CallActive)) || List.length (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall <= 0) || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status = CallActive
                                              • start[0.580s, "1.1"]
                                                  ((_x_0 = []
                                                    || not
                                                       (List.length
                                                        (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                         {status = …; callIncomingFrom = …; peopleInCall = …}
                                                         (List.tl _x_0)).peopleInCall
                                                        <= 0
                                                        || (List.fold_right
                                                            ((fun update_fn a b -> update_fn b a) good_update)
                                                            {status = …; callIncomingFrom = …; peopleInCall = …}
                                                            (List.tl _x_0)).status
                                                           = CallActive))
                                                   || List.length
                                                      (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                       {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall
                                                      <= 0)
                                                  || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                      {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status
                                                     = CallActive
                                              • simplify
                                                into
                                                true
                                                expansions
                                                [List.fold_right, List.fold_right, List.fold_right, List.length,
                                                 List.fold_right, List.fold_right, List.fold_right, List.fold_right,
                                                 List.fold_right, List.length, List.fold_right, List.fold_right]
                                                rewrite_steps
                                                  forward_chaining
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                                  • List.len_nonnegative
                                              • subproof
                                                (not (_x_0 = []) || List.length (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall <= 0) || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update) {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status = CallActive
                                                • start[0.580s, "1.2"]
                                                    (not (_x_0 = [])
                                                     || List.length
                                                        (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                         {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).peopleInCall
                                                        <= 0)
                                                    || (List.fold_right ((fun update_fn a b -> update_fn b a) good_update)
                                                        {status = …; callIncomingFrom = …; peopleInCall = …} _x_0).status
                                                       = CallActive
                                                • simplify
                                                  into
                                                  true
                                                  expansions
                                                  [List.length, List.fold_right, List.fold_right]
                                                  rewrite_steps
                                                    forward_chaining
                                                    • List.len_nonnegative
                                                    • List.len_nonnegative

                                            Fully proved! For larger functions going into Imandra's more advanced features will require more expertise, and may or may not be worth it over the guarantees that the basic unrolling method gives us. Whether the cost makes sense will depend on what you're working on.

                                            One other improvement we could make is to incorporate the update_outcome concept from our ideal version, and check that the property holds for valid resulting states only. This would enable us to stop passing the concrete, valid initial_state in as an argument and allow Imandra to verify that this works for all possible state values in our property arguments, as the update function would handle filtering out invalid states for us. Analogously we can 'guard' our states with a separate is_valid function as part of the property. Have a go at doing this yourself in the notebook!

                                            We've given you a quick taste of some new possibilities here, but the takeaway is that state machines are a useful tool - having a formalized way of thinking about a class of system makes life easier for both you and the computer, whether that's via pure human brain power, a type system or an automated reasoning tool like Imandra.