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 = Z.t
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 -> person -> 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 -> person -> bool = <fun>
module CX : sig val state : state val person : person end
Counterexample (after 2 steps, 0.011s):
let state : state =
  {status = Idle; callIncomingFrom = None; peopleInCall = []}
let person : int = 2
Refuted
proof attempt
ground_instances:2
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
num checks:5
arith assert lower:3
arith tableau max rows:2
arith tableau max columns:7
arith pivots:1
rlimit count:1064
mk clause:7
datatype occurs check:21
mk bool var:41
arith assert upper:2
datatype splits:7
decisions:9
propagations:4
conflicts:2
arith fixed eqs:1
datatype accessor ax:12
arith num rows:2
datatype constructor ax:13
num allocs:7239796
final checks:6
added eqs:41
del clause:3
arith eq adapter:2
memory:17.600000
max memory:17.600000
Expand
  • start[0.011s] if List.length … > 0 then … = CallActive else true
  • simplify

    into:
    (List.length (( :var_0: ) :: ( :var_1: ).peopleInCall) <= 0)
    || (… = CallActive)
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|List.length_466/server|
          (|::| person_1355/client (peopleInCall_1276/client state_1354/client)))
        expansions:
        • unroll
          expr:
          (|List.length_466/server| (peopleInCall_1276/client state_1354/client))
          expansions:
          • Sat (Some let state : state = {status = Idle; callIncomingFrom = None; peopleInCall = []} let person : int = (Z.of_nativeint (2n)) )

          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.state.peopleInCall);
          
          Out[12]:
          - : person = 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 (actions => call_with_people_in_is_active_property(update_v2, initial_state, actions));
          
          Out[14]:
          val initial_state : state =
            {status = Idle; callIncomingFrom = None; peopleInCall = []}
          - : action_v2 list -> bool = <fun>
          module CX : sig val actions : action_v2 list end
          
          Counterexample (after 4 steps, 0.012s):
          let actions : action_v2 list = [AddPerson 3]
          
          Refuted
          proof attempt
          ground_instances:4
          definitions:0
          inductions:0
          search_time:
          0.012s
          details:
          Expand
          smt_stats:
          num checks:9
          arith assert lower:6
          arith tableau max rows:4
          arith tableau max columns:10
          arith pivots:5
          rlimit count:3952
          mk clause:32
          datatype occurs check:77
          mk bool var:210
          arith assert upper:4
          datatype splits:22
          decisions:80
          arith row summations:9
          propagations:89
          conflicts:10
          arith fixed eqs:5
          datatype accessor ax:41
          minimized lits:1
          arith num rows:4
          arith assert diseq:2
          datatype constructor ax:55
          num allocs:12683522
          final checks:9
          added eqs:283
          del clause:9
          arith eq adapter:6
          memory:18.370000
          max memory:18.370000
          Expand
          • start[0.012s]
              let (_x_0 : state)
                  = List.fold_left update_v2
                    {status = Idle; callIncomingFrom = None; peopleInCall = []}
                    ( :var_0: )
              in
              if List.length _x_0.peopleInCall > 0 then _x_0.status = CallActive
              else true
          • simplify

            into:
            let (_x_0 : state)
                = List.fold_left update_v2
                  {status = …; callIncomingFrom = …; peopleInCall = …} ( :var_0: )
            in (_x_0.status = CallActive) || (List.length _x_0.peopleInCall <= 0)
            expansions:
            []
            rewrite_steps:
              forward_chaining:
              • unroll
                expr:
                (|List.length_528/server|
                  (peopleInCall_1276/client
                    (|List.fold_left_523/server|
                      (|rec_m…
                expansions:
                • unroll
                  expr:
                  (|List.fold_left_523/server|
                    (|rec_mk.state_513/server| Idle_1268/client None |[]|)
                    actions_1363…
                  expansions:
                  • unroll
                    expr:
                    (let ((a!1 (|get.::.1_518/server|
                                 (peopleInCall_1276/client
                                   (|List.fold_…
                    expansions:
                    • unroll
                      expr:
                      (|List.fold_left_523/server|
                        (update_v2_1294/client
                          (|rec_mk.state_513/server| Idle_1268/clien…
                      expansions:
                      • Sat (Some let actions : action_v2 list = [AddPerson (Z.of_nativeint (3n))] )

                      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 (actions => call_with_people_in_is_active_property(update, initial_state, actions));
                      
                      Out[16]:
                      - : action list -> bool = <fun>
                      module CX : sig val actions : action list end
                      
                      Counterexample (after 7 steps, 0.017s):
                      let actions : action list =
                        [CallIncomingFrom 3; CallAccepted; CallIncomingFrom 8]
                      
                      Refuted
                      proof attempt
                      ground_instances:7
                      definitions:0
                      inductions:0
                      search_time:
                      0.017s
                      details:
                      Expand
                      smt_stats:
                      arith offset eqs:16
                      num checks:15
                      arith assert lower:34
                      arith tableau max rows:8
                      arith tableau max columns:15
                      arith pivots:13
                      rlimit count:10688
                      mk clause:143
                      datatype occurs check:260
                      mk bool var:607
                      arith assert upper:35
                      datatype splits:45
                      decisions:284
                      arith row summations:37
                      arith bound prop:7
                      propagations:429
                      conflicts:49
                      arith fixed eqs:52
                      datatype accessor ax:130
                      minimized lits:26
                      arith num rows:8
                      arith assert diseq:14
                      datatype constructor ax:189
                      num allocs:19745330
                      final checks:19
                      added eqs:1405
                      del clause:48
                      arith eq adapter:41
                      time:0.001000
                      memory:19.020000
                      max memory:19.020000
                      Expand
                      • start[0.017s]
                          let (_x_0 : state)
                              = List.fold_left update
                                {status = …; callIncomingFrom = …; peopleInCall = …}
                                ( :var_0: )
                          in
                          if List.length _x_0.peopleInCall > 0 then _x_0.status = CallActive
                          else true
                      • simplify

                        into:
                        let (_x_0 : state)
                            = List.fold_left update
                              {status = …; callIncomingFrom = …; peopleInCall = …} ( :var_0: )
                        in (_x_0.status = CallActive) || (List.length _x_0.peopleInCall <= 0)
                        expansions:
                        []
                        rewrite_steps:
                          forward_chaining:
                          • unroll
                            expr:
                            (|List.length_565/server|
                              (peopleInCall_1276/client
                                (|List.fold_left_560/server|
                                  (|rec_m…
                            expansions:
                            • unroll
                              expr:
                              (|List.fold_left_560/server|
                                (|rec_mk.state_550/server| Idle_1268/client None |[]|)
                                actions_1365…
                              expansions:
                              • unroll
                                expr:
                                (let ((a!1 (|get.::.1_555/server|
                                             (peopleInCall_1276/client
                                               (|List.fold_…
                                expansions:
                                • unroll
                                  expr:
                                  (|List.fold_left_560/server|
                                    (update_1279/client
                                      (|rec_mk.state_550/server| Idle_1268/client N…
                                  expansions:
                                  • unroll
                                    expr:
                                    (let ((a!1 (|get.::.1_555/server|
                                                 (peopleInCall_1276/client
                                                   (|List.fold_…
                                    expansions:
                                    • unroll
                                      expr:
                                      (|List.fold_left_560/server|
                                        (update_1279/client
                                          (update_1279/client
                                            (|rec_mk.state_550/…
                                      expansions:
                                      • unroll
                                        expr:
                                        (let ((a!1 (update_1279/client
                                                     (update_1279/client
                                                       (update_1279/client
                                         …
                                        expansions:
                                        • Sat (Some let actions : action list = [CallIncomingFrom (Z.of_nativeint (3n)); CallAccepted; CallIncomingFrom (Z.of_nativeint (8n))] )

                                        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:20 (actions => call_with_people_in_is_active_property(good_update, initial_state, actions));
                                        
                                        Out[19]:
                                        - : action_v2 list -> bool = <fun>
                                        
                                        Proved up to 20 steps

                                        Imandra's standard unrolling verification method can't find any issues up to our bound of 20 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 (actions => call_with_people_in_is_active_property(good_update, initial_state, actions));
                                        
                                        Out[20]:
                                        - : action_v2 list -> bool = <fun>
                                        Goal:
                                        
                                        call_with_people_in_is_active_property good_update initial_state actions.
                                        
                                        1 nontautological subgoal.
                                        
                                        Subgoal 1:
                                        
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).status
                                             = CallActive
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                        
                                        
                                        Must try induction.
                                        
                                        We shall induct according to a scheme derived from List.fold_left.
                                        
                                        Induction scheme:
                                        
                                         (not (actions <> []) ==> φ actions)
                                         && (actions <> [] && φ (List.tl actions) ==> φ actions).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.2:
                                        
                                        |---------------------------------------------------------------------------
                                         C0. actions <> []
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).status
                                             = CallActive
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_left and List.length.
                                        
                                        Subgoal 1.1:
                                        
                                         H0. actions <> []
                                         H1. ((List.fold_left good_update
                                               {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                               (List.tl actions)).status
                                              = CallActive)
                                             || (List.length
                                                 (List.fold_left good_update
                                                  {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                  (List.tl actions)).peopleInCall
                                                 <= 0)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).status
                                             = CallActive
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to the
                                        following 2 subgoals:
                                        
                                        Subgoal 1.1.2:
                                        
                                         H0. actions <> []
                                         H1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl actions)).peopleInCall
                                             <= 0
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (List.tl actions)).status
                                             = CallActive
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).status
                                             = CallActive
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         actions -> actions1 :: actions2
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2':
                                        
                                         H0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions2).peopleInCall
                                             <= 0
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions2).status
                                             = CallActive
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (actions1 :: actions2)).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                              (actions1 :: actions2)).status
                                             = CallActive
                                        
                                        This simplifies, using the definition of List.fold_left to:
                                        
                                        Subgoal 1.1.2'':
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions2).peopleInCall
                                             <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, actions1));
                                               peopleInCall = []}
                                              actions2).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = CallIncoming;
                                               callIncomingFrom = Some (Destruct(CallIncomingFrom, 0, actions1));
                                               peopleInCall = []}
                                              actions2).status
                                             = CallActive
                                         C2. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions2).status
                                             = CallActive
                                        
                                        
                                        Candidates for generalization:
                                        
                                         Some (Destruct(CallIncomingFrom, 0, actions1))
                                         List.fold_left good_update
                                         {status = Idle; callIncomingFrom = None; peopleInCall = []} actions2
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2''':
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).status
                                             = CallActive
                                         C2. gen_2.status = CallActive
                                        
                                        
                                        Candidates for generalization:
                                        
                                         List.fold_left good_update
                                         {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                         actions2
                                        
                                        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. Is_a(CallIncomingFrom, actions1)
                                         H1. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length gen_3.peopleInCall <= 0
                                         C1. gen_3.status = CallActive
                                         C2. gen_2.status = CallActive
                                        
                                        Must try induction.
                                        
                                        We shall induct according to a scheme derived from List.fold_left.
                                        
                                        Induction scheme:
                                        
                                         (not (actions2 <> []) ==> φ actions1 actions2 gen_1 gen_2)
                                         && (actions2 <> [] && φ actions1 (List.tl actions2) gen_1 gen_2
                                             ==> φ actions1 actions2 gen_1 gen_2).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.1.2'''.2:
                                        
                                         H0. List.length gen_2.peopleInCall <= 0
                                         H1. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. actions2 <> []
                                         C1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).status
                                             = CallActive
                                         C2. gen_2.status = CallActive
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).peopleInCall
                                             <= 0
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_left and List.length.
                                        
                                        Subgoal 1.1.2'''.1:
                                        
                                         H0. List.length gen_2.peopleInCall <= 0
                                         H1. actions2 <> []
                                         H2. (List.length
                                              (List.fold_left good_update
                                               {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                               (List.tl actions2)).peopleInCall
                                              <= 0)
                                             || ((List.fold_left good_update
                                                  {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                                  (List.tl actions2)).status
                                                 = CallActive)
                                             || not (List.length gen_2.peopleInCall <= 0)
                                             || (gen_2.status = CallActive) || not Is_a(CallIncomingFrom, actions1)
                                         H3. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).status
                                             = CallActive
                                         C1. gen_2.status = CallActive
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).peopleInCall
                                             <= 0
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to the
                                        following 2 subgoals:
                                        
                                        Subgoal 1.1.2'''.1.2:
                                        
                                         H0. List.length gen_2.peopleInCall <= 0
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              (List.tl actions2)).status
                                             = CallActive
                                         H2. actions2 <> []
                                         H3. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              (List.tl actions2)).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).status
                                             = CallActive
                                         C2. gen_2.status = CallActive
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).peopleInCall
                                             <= 0
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         actions2 -> actions21 :: actions22
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2'''.1.2':
                                        
                                         H0. List.length gen_2.peopleInCall <= 0
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H2. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              (actions21 :: actions22)).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C2. gen_2.status = CallActive
                                         C3. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              (actions21 :: actions22)).status
                                             = CallActive
                                        
                                        This simplifies, using the definition of List.fold_left to the following 2
                                        subgoals:
                                        
                                        Subgoal 1.1.2'''.1.2'.2:
                                        
                                         H0. Is_a(Some, gen_1)
                                         H1. List.length gen_2.peopleInCall <= 0
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H3. actions21 = CallAccepted
                                         H4. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. actions21 = CallRejected
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Option.get gen_1]}
                                              actions22).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Option.get gen_1]}
                                              actions22).status
                                             = CallActive
                                         C4. gen_2.status = CallActive
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to:
                                        
                                        Subgoal 1.1.2'''.1.2'.2':
                                        
                                         H0. Is_a(Some, gen_1)
                                         H1. List.length gen_2.peopleInCall <= 0
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H3. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Option.get gen_1]}
                                              actions22).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None;
                                               peopleInCall = [Option.get gen_1]}
                                              actions22).status
                                             = CallActive
                                         C3. gen_2.status = CallActive
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         gen_1 -> Some gen_11
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2'''.1.2'.2'':
                                        
                                         H0. List.length gen_2.peopleInCall <= 0
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H2. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).status
                                             = CallActive
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).peopleInCall
                                             <= 0
                                         C3. gen_2.status = CallActive
                                        
                                        
                                        Candidates for generalization:
                                        
                                         List.fold_left good_update
                                         {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                         actions22
                                         List.fold_left good_update
                                         {status = CallIncoming; callIncomingFrom = Some gen_11; peopleInCall = []}
                                         actions22
                                        
                                        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. List.length gen_2.peopleInCall <= 0
                                         H1. gen_2.status = CallActive
                                         H2. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. gen_1.status = CallActive
                                         C1. List.length gen_2.peopleInCall <= 0
                                         C2. List.length gen_1.peopleInCall <= 0
                                         C3. gen_2.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:
                                        
                                         (not (actions22 <> []) ==> φ actions1 actions22 gen_11 gen_2)
                                         && (actions22 <> [] && φ actions1 (List.tl actions22) gen_11 gen_2
                                             ==> φ actions1 actions22 gen_11 gen_2).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.1.2'''.1.2'.2''.2:
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H2. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C1. actions22 <> []
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).status
                                             = CallActive
                                         C4. gen_2.status = CallActive
                                        
                                        But simplification reduces this to true, using the definition of
                                        List.fold_left.
                                        
                                        Subgoal 1.1.2'''.1.2'.2''.1:
                                        
                                         H0. actions22 <> []
                                         H1. not Is_a(CallIncomingFrom, actions1)
                                             || (List.length
                                                 (List.fold_left good_update
                                                  {status = CallIncoming; callIncomingFrom = Some gen_11;
                                                   peopleInCall = []}
                                                  (List.tl actions22)).peopleInCall
                                                 <= 0)
                                             || ((List.fold_left good_update
                                                  {status = CallActive; callIncomingFrom = None;
                                                   peopleInCall = [gen_11]}
                                                  (List.tl actions22)).status
                                                 = CallActive)
                                             || not
                                                ((List.fold_left good_update
                                                  {status = CallIncoming; callIncomingFrom = Some gen_11;
                                                   peopleInCall = []}
                                                  (List.tl actions22)).status
                                                 = CallActive)
                                             || (List.length
                                                 (List.fold_left good_update
                                                  {status = CallActive; callIncomingFrom = None;
                                                   peopleInCall = [gen_11]}
                                                  (List.tl actions22)).peopleInCall
                                                 <= 0)
                                             || (gen_2.status = CallActive)
                                             || not (List.length gen_2.peopleInCall <= 0)
                                         H2. Is_a(CallIncomingFrom, actions1)
                                         H3. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H4. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).status
                                             = CallActive
                                         C3. gen_2.status = CallActive
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to the
                                        following 4 subgoals:
                                        
                                        Subgoal 1.1.2'''.1.2'.2''.1.4:
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              (List.tl actions22)).peopleInCall
                                             <= 0
                                         H2. actions22 <> []
                                         H3. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              (List.tl actions22)).status
                                             = CallActive
                                         H4. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H5. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              (List.tl actions22)).peopleInCall
                                             <= 0
                                         C2. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              (List.tl actions22)).status
                                             = CallActive
                                         C3. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).peopleInCall
                                             <= 0
                                         C4. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).status
                                             = CallActive
                                         C5. gen_2.status = CallActive
                                        
                                        
                                        We can eliminate destructors by the following
                                        substitution:
                                         actions22 -> actions221 :: actions222
                                        
                                        This produces the modified subgoal:
                                        
                                        Subgoal 1.1.2'''.1.2'.2''.1.4':
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).status
                                             = CallActive
                                         H2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).peopleInCall
                                             <= 0
                                         H3. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              (actions221 :: actions222)).status
                                             = CallActive
                                         H4. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              (actions221 :: actions222)).peopleInCall
                                             <= 0
                                         C1. gen_2.status = CallActive
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              (actions221 :: actions222)).peopleInCall
                                             <= 0
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).status
                                             = CallActive
                                         C4. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              (actions221 :: actions222)).status
                                             = CallActive
                                         C5. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).peopleInCall
                                             <= 0
                                        
                                        This simplifies, using the definition of List.fold_left to the following 2
                                        subgoals:
                                        
                                        Subgoal 1.1.2'''.1.2'.2''.1.4'.2:
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. Is_a(EndCall, actions221)
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).status
                                             = CallActive
                                         H3. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).peopleInCall
                                             <= 0
                                         H4. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222).peopleInCall
                                             <= 0
                                         C1. actions221 = CallRejected
                                         C2. Is_a(AddPerson, actions221)
                                         C3. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222).status
                                             = CallActive
                                         C4. gen_2.status = CallActive
                                         C5. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).status
                                             = CallActive
                                         C6. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).peopleInCall
                                             <= 0
                                         C7. actions221 = CallAccepted
                                        
                                        This simplifies, using the forward-chaining rule List.len_nonnegative to:
                                        
                                        Subgoal 1.1.2'''.1.2'.2''.1.4'.2':
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. Is_a(EndCall, actions221)
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).status
                                             = CallActive
                                         H3. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).peopleInCall
                                             <= 0
                                         H4. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222).status
                                             = CallActive
                                         C2. gen_2.status = CallActive
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).status
                                             = CallActive
                                         C4. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).peopleInCall
                                             <= 0
                                        
                                        
                                        Candidates for generalization:
                                        
                                         List.fold_left good_update
                                         {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                         actions222
                                         List.fold_left good_update
                                         {status = CallIncoming; callIncomingFrom = Some gen_11; peopleInCall = []}
                                         actions222
                                         List.fold_left good_update
                                         {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222
                                        
                                        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. Is_a(CallIncomingFrom, actions1)
                                         H1. Is_a(EndCall, actions221)
                                         H2. gen_2.status = CallActive
                                         H3. List.length gen_1.peopleInCall <= 0
                                         H4. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length gen_3.peopleInCall <= 0
                                         C1. gen_3.status = CallActive
                                         C2. gen_2.status = CallActive
                                         C3. gen_1.status = CallActive
                                         C4. List.length gen_2.peopleInCall <= 0
                                        
                                        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. Is_a(CallIncomingFrom, actions1)
                                         H1. Is_a(EndCall, actions221)
                                         H2. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).status
                                             = CallActive
                                         H3. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).peopleInCall
                                             <= 0
                                         H4. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions222).status
                                             = CallActive
                                         C2. gen_2.status = CallActive
                                         C3. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions222).status
                                             = CallActive
                                         C4. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions222).peopleInCall
                                             <= 0
                                        
                                         H0. List.length gen_2.peopleInCall <= 0
                                         H1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).status
                                             = CallActive
                                         H2. Is_a(CallIncomingFrom, actions1)
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).status
                                             = CallActive
                                         C1. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = Some gen_11;
                                               peopleInCall = []}
                                              actions22).peopleInCall
                                             <= 0
                                         C2. List.length
                                             (List.fold_left good_update
                                              {status = CallActive; callIncomingFrom = None; peopleInCall = [gen_11]}
                                              actions22).peopleInCall
                                             <= 0
                                         C3. gen_2.status = CallActive
                                        
                                         H0. Is_a(CallIncomingFrom, actions1)
                                         H1. List.length gen_2.peopleInCall <= 0
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).peopleInCall
                                             <= 0
                                         C1. (List.fold_left good_update
                                              {status = CallIncoming; callIncomingFrom = gen_1; peopleInCall = []}
                                              actions2).status
                                             = CallActive
                                         C2. gen_2.status = CallActive
                                        
                                        Error:
                                          Maximum induction depth reached (3). You can set this with #max_induct.
                                          At <none>:1
                                          

                                        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(actions => call_with_people_in_is_active_property_fold_right(good_update, initial_state, actions));
                                        
                                        Out[22]:
                                        - : action_v2 list -> bool = <fun>
                                        Goal:
                                        
                                        call_with_people_in_is_active_property_fold_right good_update initial_state
                                        actions.
                                        
                                        1 nontautological subgoal.
                                        
                                        Subgoal 1:
                                        
                                        |---------------------------------------------------------------------------
                                         C0. (List.fold_right
                                              (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                               good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).status
                                             = CallActive
                                         C1. List.length
                                             (List.fold_right
                                              (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                               good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                        
                                        
                                        Must try induction.
                                        
                                        We shall induct according to a scheme derived from List.fold_right.
                                        
                                        Induction scheme:
                                        
                                         (not (actions <> []) ==> φ actions)
                                         && (actions <> [] && φ (List.tl actions) ==> φ actions).
                                        
                                        2 nontautological subgoals.
                                        
                                        Subgoal 1.2:
                                        
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_right
                                              (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                               good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                         C1. (List.fold_right
                                              (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                               good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).status
                                             = CallActive
                                         C2. actions <> []
                                        
                                        But simplification reduces this to true, using the definitions of
                                        List.fold_right and List.length.
                                        
                                        Subgoal 1.1:
                                        
                                         H0. actions <> []
                                         H1. ((List.fold_right
                                               (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                good_update)
                                               {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                               (List.tl actions)).status
                                              = CallActive)
                                             || (List.length
                                                 (List.fold_right
                                                  (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                   good_update)
                                                  {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                  (List.tl actions)).peopleInCall
                                                 <= 0)
                                        |---------------------------------------------------------------------------
                                         C0. List.length
                                             (List.fold_right
                                              (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                               good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).peopleInCall
                                             <= 0
                                         C1. (List.fold_right
                                              (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                               good_update)
                                              {status = Idle; callIncomingFrom = None; peopleInCall = []} actions).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_instances:0
                                        definitions:11
                                        inductions:1
                                        search_time:
                                        0.365s
                                        Expand
                                        • start[0.365s, "Goal"]
                                            let (_x_0 : state)
                                                = List.fold_right
                                                  (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                   good_update)
                                                  {status = …; callIncomingFrom = …; peopleInCall = …}
                                                  ( :var_0: )
                                            in
                                            if List.length _x_0.peopleInCall > 0 then _x_0.status = CallActive
                                            else true
                                        • subproof

                                          let (_x_0 : state) = List.fold_right (anon_fun.call_with_people_in_is_active_property_fold_right.1 good_update) {status = Idle; callIncomingFrom = None; peopleInCall = []} actions in (_x_0.status = CallActive) || (List.length _x_0.peopleInCall <= 0)
                                          • start[0.365s, "1"]
                                              let (_x_0 : state)
                                                  = List.fold_right
                                                    (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                     good_update)
                                                    {status = Idle; callIncomingFrom = None; peopleInCall = []} actions
                                              in (_x_0.status = CallActive) || (List.length _x_0.peopleInCall <= 0)
                                          • induction on (functional ?)
                                            :scheme (not (actions <> []) ==> φ actions)
                                                    && (actions <> [] && φ (List.tl actions) ==> φ actions)
                                          • Split (let (_x_0 : state)
                                                       = {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                   in
                                                   let (_x_1 : state)
                                                       = List.fold_right
                                                         (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                          good_update)
                                                         _x_0 actions
                                                   in
                                                   let (_x_2 : bool)
                                                       = (List.length _x_1.peopleInCall <= 0)
                                                         || (_x_1.status = CallActive)
                                                   in
                                                   let (_x_3 : bool) = actions <> [] in
                                                   let (_x_4 : state)
                                                       = List.fold_right
                                                         (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                          good_update)
                                                         _x_0 (List.tl actions)
                                                   in
                                                   (_x_2 || _x_3)
                                                   && (_x_2
                                                       || not
                                                          (_x_3
                                                           && ((_x_4.status = CallActive)
                                                               || (List.length _x_4.peopleInCall <= 0))))
                                                   :cases [let (_x_0 : state)
                                                               = List.fold_right
                                                                 (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                                  good_update)
                                                                 {status = …; callIncomingFrom = …;
                                                                  peopleInCall = …}
                                                                 actions
                                                           in
                                                           (List.length _x_0.peopleInCall <= 0)
                                                           || (_x_0.status = CallActive) || actions <> [];
                                                           let (_x_0 : state)
                                                               = {status = Idle; callIncomingFrom = None;
                                                                  peopleInCall = []}
                                                           in
                                                           let (_x_1 : state)
                                                               = List.fold_right
                                                                 (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                                  good_update)
                                                                 _x_0 (List.tl actions)
                                                           in
                                                           let (_x_2 : state)
                                                               = List.fold_right
                                                                 (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                                  good_update)
                                                                 _x_0 actions
                                                           in
                                                           not (actions <> [])
                                                           || not
                                                              ((_x_1.status = CallActive)
                                                               || (List.length _x_1.peopleInCall <= 0))
                                                           || (List.length _x_2.peopleInCall <= 0)
                                                           || (_x_2.status = CallActive)])
                                            • subproof
                                              let (_x_0 : state) = {status = Idle; callIncomingFrom = None; peopleInCall = []} in let (_x_1 : state) = List.fold_right (anon_fun.call_with_people_in_is_active_property_fold_right.1 good_update) _x_0 (List.tl actions) in let (_x_2 : state) = List.fold_right (anon_fun.call_with_people_in_is_active_property_fold_right.1 good_update) _x_0 actions in not (actions <> []) || not ((_x_1.status = CallActive) || (List.length _x_1.peopleInCall <= 0)) || (List.length _x_2.peopleInCall <= 0) || (_x_2.status = CallActive)
                                              • start[0.265s, "1.1"]
                                                  let (_x_0 : state)
                                                      = {status = Idle; callIncomingFrom = None; peopleInCall = []}
                                                  in
                                                  let (_x_1 : state)
                                                      = List.fold_right
                                                        (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                         good_update)
                                                        _x_0 (List.tl actions)
                                                  in
                                                  let (_x_2 : state)
                                                      = List.fold_right
                                                        (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                         good_update)
                                                        _x_0 actions
                                                  in
                                                  not (actions <> [])
                                                  || not ((_x_1.status = CallActive) || (List.length _x_1.peopleInCall <= 0))
                                                  || (List.length _x_2.peopleInCall <= 0) || (_x_2.status = CallActive)
                                              • simplify
                                                into:
                                                true
                                                expansions:
                                                [List.length, List.fold_right, List.fold_right, List.fold_right,
                                                 List.fold_right, List.fold_right, List.fold_right, 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
                                              • subproof
                                                let (_x_0 : state) = List.fold_right (anon_fun.call_with_people_in_is_active_property_fold_right.1 good_update) {status = …; callIncomingFrom = …; peopleInCall = …} actions in (List.length _x_0.peopleInCall <= 0) || (_x_0.status = CallActive) || actions <> []
                                                • start[0.265s, "1.2"]
                                                    let (_x_0 : state)
                                                        = List.fold_right
                                                          (anon_fun.call_with_people_in_is_active_property_fold_right.1
                                                           good_update)
                                                          {status = …; callIncomingFrom = …; peopleInCall = …} actions
                                                    in
                                                    (List.length _x_0.peopleInCall <= 0) || (_x_0.status = CallActive)
                                                    || actions <> []
                                                • simplify
                                                  into:
                                                  true
                                                  expansions:
                                                  [List.length, List.fold_right]
                                                  rewrite_steps:
                                                    forward_chaining:
                                                    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.