Verifying a simple autonomous vehicle controller in Imandra

In this notebook, we'll design and verify a simple autonomous vehicle controller in Imandra. The controller we analyse is due to Boyer, Green and Moore, and is described and analysed in their article The Use of a Formal Simulator to Verify a Simple Real Time Control Program.

This controller will receive sequences of sensor readings measuring changes in wind speed, and will have to respond to keep the vehicle on course. The final theorems we prove will establish the following safety and correctness properties:

  • If the vehicle starts at the initial state (0,0,0), then the controller guarantees the vehicle never strays farther than 3 units from the x-axis.
  • If the wind ever becomes constant for at least 4 sampling intervals, then the vehicle returns to the x-axis and stays there as long as the wind remains constant.

These results formally prove that the simulated vehicle appropriately stays on course under each of the infinite number of possible wind histories.

The controller and its environment

Quantities in the model are measured using integral units. The model is one-dimensional: it considers the y-components of both the vehicle and wind velocity.

Wind speed is measured in terms of the number of units in the y-direction the wind would blow a passive vehicle in one sampling interval. From one sampling interval to the next, the wind speed can change by at most one unit in either direction. The wind is permitted to blow up to arbitrarily high velocities.

At each sampling interval, the controller may increment or decrement the y-component of its velocity. We let v be the accumulated speed in the y-direction measured as the number of units the vehicle would move in one sampling interval if there were no wind. We make no assumption limiting how fast v may be changed by the control program. We permit v to become arbitrary large.

The Imandra model

The Imandra model of our system and its environment is rooted in a state vector consisting of three values:

  • w - current wind velocity
  • y - current y-position of the vehicle
  • v - accumulated velocity of the vehicle
In [1]:
type state = {
  w : int; (* current wind speed *)
  y : int; (* y-position of the vehicle *)
  v : int; (* accumulated velocity *)
}
Out[1]:
type state = { w : int; y : int; v : int; }

Our controller and state transitions

In [2]:
let controller sgn_y sgn_old_y =
  (-3 * sgn_y) + (2 * sgn_old_y)
Out[2]:
val controller : int -> int -> int = <fun>
In [3]:
let sgn x =
  if x < 0 then -1
  else if x = 0 then 0
  else 1
Out[3]:
val sgn : int -> int = <fun>

Given a wind-speed delta sensor reading and a current state, next_state computes the next state of the system as dictated by our controller.

In [4]:
let next_state dw s =
  { w = s.w + dw;
    y = s.y + s.v + s.w + dw;
    v = s.v +
        controller
          (sgn (s.y + s.v + s.w + dw))
          (sgn s.y)
  }
Out[4]:
val next_state : int -> state -> state = <fun>

Sensing the environment

The behaviour of the wind over n sampling intervals is represented as a sequence of length n. Each element of the sequence is either -1, 0, or 1 indicating how the wind changed between sampling intervals.

We define the predicate arbitrary_delta_ws to describe valid sequences of wind sensor readings.

In [5]:
let arbitrary_delta_ws = List.for_all (fun x -> x = -1 || x = 0 || x = 1)
Out[5]:
val arbitrary_delta_ws : int list -> bool = <fun>

The top-level state machine

We now define the final_state function which takes a description of an arbitrary wind sampling history and an initial state, and computes the result of running the controller (i.e., simulating the vehicle) as it responds to the changes in wind.

In [6]:
let rec final_state s dws =
  match dws with
  | [] -> s
  | dw :: dws' ->
    let s' = next_state dw s in
    final_state s' dws'
[@@adm dws]
Out[6]:
val final_state : state -> int list -> state = <fun>
termination proof

Termination proof

call `final_state (next_state (List.hd dws) s) (List.tl dws)` from `final_state s dws`
originalfinal_state s dws
subfinal_state (next_state (List.hd dws) s) (List.tl dws)
original ordinalOrdinal.Int (_cnt dws)
sub ordinalOrdinal.Int (_cnt (List.tl dws))
path[not Is_a([], dws)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
num checks8
arith-make-feasible18
arith-max-columns16
arith-conflicts2
rlimit count2024
mk clause20
datatype occurs check12
mk bool var56
arith-lower15
arith-diseq1
datatype splits1
decisions15
propagations14
arith-max-rows4
conflicts7
datatype accessor ax7
datatype constructor ax5
num allocs864623
final checks4
added eqs38
del clause13
arith eq adapter10
arith-upper12
memory5.900000
max memory5.900000
Expand
  • start[0.017s]
      let (_x_0 : int) = count.list mk_nat dws in
      let (_x_1 : int list) = List.tl dws in
      let (_x_2 : int) = count.list mk_nat _x_1 in
      not Is_a([], dws) && _x_0 >= 0 && _x_2 >= 0
      ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : int list) = List.tl dws in
    let (_x_1 : int) = count.list mk_nat _x_0 in
    let (_x_2 : int) = count.list mk_nat dws in
    (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not Is_a([], dws) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list mk_nat[0]`_1712| dws_1700)
        expansions
        • unroll
          expr
          (|`count.list mk_nat[0]`_1712| (|get.::.1_1698| dws_1700))
          expansions
          • unroll
            expr
            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                (|`count.list mk_nat[0]`_1712| (|get.::.1_1…
            expansions
            • Unsat

            Verifying our controller

            We now partition our state-space into a collection of regions, some "good," most "bad," and show that if we start in a "good" state (like (0,0,0)), then we'll (inductively) always end up in a "good" state.

            In [7]:
            (* What it means to be a ``good'' state *)
            
            let good_state s =
              match s.y, s.w + s.v with
              | -3, 1 -> true
              | -2, 1 -> true
              | -2, 2 -> true
              | -1, 2 -> true
              | -1, 3 -> true
              | 0, -1 -> true
              | 0, 0  -> true
              | 0, 1  -> true
              | 1, -2 -> true
              | 1, -3 -> true
              | 2, -1 -> true
              | 2, -2 -> true
              | 3, -1 -> true
              | _ -> false
            
            Out[7]:
            val good_state : state -> bool = <fun>
            

            Theorem: Single step safety

            We prove: If we start in a good state and evolve the system responding to one sensor reading, we end up in a good state.

            In [8]:
            theorem safety_1 s dw =
              good_state s
              && (dw = -1 || dw = 0 || dw = 1)
             ==>
              good_state (next_state dw s)
              [@@rewrite]
            
            Out[8]:
            val safety_1 : state -> int -> bool = <fun>
            
            Proved
            proof
            ground_instances0
            definitions0
            inductions0
            search_time
            0.065s
            details
            Expand
            smt_stats
            num checks1
            arith-make-feasible240
            arith-max-columns17
            arith-conflicts14
            rlimit count20291
            arith-cheap-eqs100
            mk clause2217
            mk bool var209
            arith-lower951
            arith-diseq1559
            decisions156
            arith-propagations1365
            propagations4123
            arith-bound-propagations-cheap1365
            arith-max-rows3
            conflicts96
            datatype accessor ax1
            minimized lits109
            arith-bound-propagations-lp386
            datatype constructor ax1
            num allocs4782805
            added eqs927
            del clause322
            arith eq adapter99
            arith-upper892
            time0.048000
            memory6.930000
            max memory7.880000
            Expand
            • start[0.065s]
                let (_x_0 : int) = ( :var_0: ).w in
                let (_x_1 : int) = ( :var_0: ).v in
                let (_x_2 : int) = _x_0 + _x_1 in
                let (_x_3 : bool) = 2 = _x_2 in
                let (_x_4 : int) = ( :var_0: ).y in
                let (_x_5 : bool) = -2 = _x_4 in
                let (_x_6 : bool) = 1 = _x_2 in
                let (_x_7 : int) = _x_4 + _x_1 + _x_0 + ( :var_1: ) in
                let (_x_8 : int)
                    = _x_0 + ( :var_1: )
                      + (_x_1
                         + (-3 * (if _x_7 < 0 then -1 else if _x_7 = 0 then 0 else 1)
                            + 2 * (if _x_4 < 0 then -1 else if _x_4 = 0 then 0 else 1)))
                in
                let (_x_9 : bool) = 2 = _x_8 in
                let (_x_10 : bool) = -2 = _x_7 in
                let (_x_11 : bool) = 1 = _x_8 in
                (if _x_6 && -3 = _x_4 then true
                 else
                 if _x_6 && _x_5 then true
                 else
                 if _x_3 && _x_5 then true else if _x_3 && -1 = _x_4 then true else …)
                && (( :var_1: ) = -1 || ( :var_1: ) = 0 || ( :var_1: ) = 1)
                ==> (if _x_11 && -3 = _x_7 then true
                     else
                     if _x_11 && _x_10 then true
                     else
                     if _x_9 && _x_10 then true
                     else if _x_9 && -1 = _x_7 then true else …)
            • simplify

              into
              let (_x_0 : int) = ( :var_0: ).w in
              let (_x_1 : int) = ( :var_0: ).v in
              let (_x_2 : int) = ( :var_0: ).y in
              let (_x_3 : int) = _x_2 + _x_1 + _x_0 + ( :var_1: ) in
              let (_x_4 : int)
                  = _x_0 + ( :var_1: ) + _x_1
                    + -3 * (if 0 <= _x_3 then if _x_3 = 0 then 0 else 1 else -1)
                    + 2 * (if 0 <= _x_2 then if _x_2 = 0 then 0 else 1 else -1)
              in
              let (_x_5 : bool) = 1 = _x_4 in
              let (_x_6 : bool) = -2 = _x_3 in
              let (_x_7 : bool) = 2 = _x_4 in
              let (_x_8 : bool) = -1 = _x_3 in
              let (_x_9 : bool) = -1 = _x_4 in
              let (_x_10 : bool) = 0 = _x_3 in
              let (_x_11 : bool) = -2 = _x_4 in
              let (_x_12 : bool) = 1 = _x_3 in
              let (_x_13 : bool) = 2 = _x_3 in
              let (_x_14 : int) = _x_0 + _x_1 in
              let (_x_15 : bool) = -1 = _x_14 in
              let (_x_16 : bool) = -2 = _x_14 in
              let (_x_17 : bool) = 2 = _x_2 in
              let (_x_18 : bool) = 1 = _x_2 in
              let (_x_19 : bool) = 1 = _x_14 in
              let (_x_20 : bool) = 0 = _x_2 in
              let (_x_21 : bool) = -1 = _x_2 in
              let (_x_22 : bool) = 2 = _x_14 in
              let (_x_23 : bool) = -2 = _x_2 in
              ((((((((((((_x_5 && -3 = _x_3 || _x_5 && _x_6) || _x_7 && _x_6)
                        || _x_7 && _x_8)
                       || 3 = _x_4 && _x_8)
                      || _x_9 && _x_10)
                     || _x_5 && _x_10)
                    || 0 = _x_4 && _x_10)
                   || _x_11 && _x_12)
                  || -3 = _x_4 && _x_12)
                 || _x_9 && _x_13)
                || _x_11 && _x_13)
               || _x_9 && 3 = _x_3)
              || not
                 (((((((((((((_x_15 && 3 = _x_2 || _x_16 && _x_17) || _x_15 && _x_17)
                            || -3 = _x_14 && _x_18)
                           || _x_16 && _x_18)
                          || _x_19 && _x_20)
                         || 0 = _x_14 && _x_20)
                        || _x_15 && _x_20)
                       || 3 = _x_14 && _x_21)
                      || _x_22 && _x_21)
                     || _x_22 && _x_23)
                    || _x_19 && _x_23)
                   || _x_19 && -3 = _x_2)
                  && ((( :var_1: ) = -1 || ( :var_1: ) = 0) || ( :var_1: ) = 1))
              expansions
              []
              rewrite_steps
                forward_chaining
                • Unsat

                Warning

                Pattern will match only if `good_state` is disabled
                (non-recursive function)
                See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

                Warning

                Pattern will match only if `next_state` is disabled
                (non-recursive function)
                See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

                Theorem: Multistep safety

                We prove: If we start in a good state and simulate the controller w.r.t. an arbitrary sequence of sensor readings, then we still end up in a good state.

                In [9]:
                #disable next_state;;
                #disable good_state;;
                
                theorem all_good s dws =
                  good_state s && arbitrary_delta_ws dws
                  ==>
                  good_state ((final_state s dws) [@trigger])
                [@@induct functional final_state]
                [@@forward_chaining]
                
                Out[9]:
                val all_good : state -> int list -> bool = <fun>
                Goal:
                
                good_state s && arbitrary_delta_ws dws ==> good_state (final_state s dws).
                
                1 nontautological subgoal.
                
                We shall induct according to a scheme derived from final_state.
                
                Induction scheme:
                
                 (Is_a([], dws) ==> φ dws s)
                 && (not Is_a([], dws) && φ (List.tl dws) (next_state (List.hd dws) s)
                     ==> φ dws s).
                
                2 nontautological subgoals.
                
                Subgoal 2:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                 H2. Is_a([], dws)
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                But simplification reduces this to true, using the definitions of
                List.for_all and final_state.
                
                Subgoal 1:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                 H2. not Is_a([], dws)
                 H3. good_state (next_state (List.hd dws) s)
                     && List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                     ==> good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                This simplifies, using the definitions of List.for_all and final_state to the
                following 3 subgoals:
                
                Subgoal 1.3:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                 H2. List.hd dws = 1
                |---------------------------------------------------------------------------
                 C0. Is_a([], dws)
                 C1. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C2. good_state (next_state (List.hd dws) s)
                 C3. List.hd dws = -1
                 C4. List.hd dws = 0
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.2:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                 H2. List.hd dws = 0
                |---------------------------------------------------------------------------
                 C0. Is_a([], dws)
                 C1. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C2. good_state (next_state (List.hd dws) s)
                 C3. List.hd dws = -1
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.1:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                 H2. List.hd dws = -1
                |---------------------------------------------------------------------------
                 C0. Is_a([], dws)
                 C1. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C2. good_state (next_state (List.hd dws) s)
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                 Rules:
                    (:def List.for_all)
                    (:def final_state)
                    (:rw safety_1)
                    (:induct final_state)
                
                
                Proved
                proof
                ground_instances0
                definitions11
                inductions1
                search_time
                0.696s
                Expand
                • start[0.696s, "Goal"]
                    good_state ( :var_0: )
                    && List.for_all (fun x -> x = -1 || x = 0 || x = 1) ( :var_1: )
                    ==> good_state (final_state ( :var_0: ) ( :var_1: ))
                • subproof

                  (not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || good_state (final_state s dws)
                  • start[0.696s, "1"]
                      (not (good_state s)
                       || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                      || good_state (final_state s dws)
                  • induction on (functional final_state)
                    :scheme (Is_a([], dws) ==> φ dws s)
                            && (not Is_a([], dws)
                                && φ (List.tl dws) (next_state (List.hd dws) s) ==> φ dws s)
                  • Split (let (_x_0 : bool)
                               = good_state (final_state s dws)
                                 || not
                                    (good_state s
                                     && List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)
                           in
                           let (_x_1 : bool) = not Is_a([], dws) in
                           let (_x_2 : state) = next_state (List.hd dws) s in
                           let (_x_3 : int list) = List.tl dws in
                           (_x_0 || _x_1)
                           && (_x_0
                               || not
                                  (_x_1
                                   && (good_state (final_state _x_2 _x_3)
                                       || not
                                          (good_state _x_2
                                           && List.for_all (fun x -> x = -1 || x = 0 || x = 1)
                                              _x_3))))
                           :cases [((not (good_state s)
                                     || not
                                        (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                                    || not Is_a([], dws))
                                   || good_state (final_state s dws);
                                   let (_x_0 : state) = next_state (List.hd dws) s in
                                   let (_x_1 : int list) = List.tl dws in
                                   (((not (good_state s)
                                      || not
                                         (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                                     || Is_a([], dws))
                                    || not
                                       (good_state _x_0
                                        && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1
                                        ==> good_state (final_state _x_0 _x_1)))
                                   || good_state (final_state s dws)])
                    • subproof
                      let (_x_0 : state) = next_state (List.hd dws) s in let (_x_1 : int list) = List.tl dws in (((not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || Is_a([], dws)) || not (good_state _x_0 && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1 ==> good_state (final_state _x_0 _x_1))) || good_state (final_state s dws)
                      • start[0.695s, "1"]
                          let (_x_0 : state) = next_state (List.hd dws) s in
                          let (_x_1 : int list) = List.tl dws in
                          (((not (good_state s)
                             || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                            || Is_a([], dws))
                           || not
                              (good_state _x_0
                               && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1
                               ==> good_state (final_state _x_0 _x_1)))
                          || good_state (final_state s dws)
                      • simplify
                        into
                        let (_x_0 : int) = List.hd dws in
                        let (_x_1 : state) = next_state _x_0 s in
                        let (_x_2 : int list) = List.tl dws in
                        let (_x_3 : bool)
                            = (((Is_a([], dws) || good_state (final_state _x_1 _x_2))
                                || good_state _x_1)
                               || not (good_state s))
                              || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_2)
                        in
                        let (_x_4 : bool) = _x_0 = -1 in
                        let (_x_5 : bool) = _x_3 || _x_4 in
                        let (_x_6 : bool) = _x_0 = 0 in
                        (((_x_5 || _x_6) || not (_x_0 = 1)) && (_x_5 || not _x_6))
                        && (_x_3 || not _x_4)
                        expansions
                        [final_state, final_state, final_state, List.for_all, List.for_all,
                         final_state, final_state, final_state, List.for_all]
                        rewrite_steps
                          forward_chaining
                            • Subproof
                            • Subproof
                            • Subproof
                        • subproof
                          ((not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || not Is_a([], dws)) || good_state (final_state s dws)
                          • start[0.695s, "2"]
                              ((not (good_state s)
                                || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                               || not Is_a([], dws))
                              || good_state (final_state s dws)
                          • simplify
                            into
                            true
                            expansions
                            [final_state, List.for_all]
                            rewrite_steps
                              forward_chaining

                        Theorem: Cannot get more than 3 units off course.

                        We prove: No matter how the wind behaves, if the vehicle starts at the initial state (0,0,0), then the controller guarantees the vehicle never strays farther than 3 units from the x-axis.

                        In [10]:
                        #enable next_state;;
                        #enable good_state;;
                        
                        theorem vehicle_stays_within_3_units_of_course dws =
                         arbitrary_delta_ws dws
                         ==>
                         let s' = final_state {y=0;w=0;v=0} dws in
                         -3 <= s'.y && s'.y <= 3
                         [@@simp]
                        
                        Out[10]:
                        val vehicle_stays_within_3_units_of_course : int list -> bool = <fun>
                        
                        Proved
                        proof
                        ground_instances0
                        definitions0
                        inductions0
                        search_time
                        0.038s
                        details
                        Expand
                        smt_stats
                        rlimit count8556
                        num allocs740398514
                        time0.008000
                        memory19.770000
                        max memory37.260000
                        Expand
                        • start[0.038s]
                            let (_x_0 : int) = (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y in
                            List.for_all (fun x -> x = -1 || x = 0 || x = 1) ( :var_0: )
                            ==> -3 <= _x_0 && _x_0 <= 3
                        • simplify

                          into
                          let (_x_0 : int) = (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y in
                          not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) ( :var_0: ))
                          || -3 <= _x_0 && _x_0 <= 3
                          expansions
                          []
                          rewrite_steps
                            forward_chaining
                            • simplify

                              into
                              true
                              expansions
                              []
                              rewrite_steps
                                forward_chaining
                                all_good
                              • Unsat

                              Theorem: If wind is stable for 4 intervals, we get back on course.

                              We prove: If the wind ever becomes constant for at least 4 sampling intervals, then the vehicle returns to the x-axis and stays there as long as the wind remains constant.

                              In [11]:
                              let steady_wind = List.for_all (fun x -> x = 0)
                              
                              let at_least_4 xs = match xs with
                                  _ :: _ :: _ :: _ :: _ -> true
                                | _ -> false
                              
                              Out[11]:
                              val steady_wind : int list -> bool = <fun>
                              val at_least_4 : 'a list -> bool = <fun>
                              
                              In [12]:
                              #disable next_state;;
                              #disable good_state;;
                              #max_induct 4;;
                              
                              theorem good_state_find_and_stay_zt_zero s dws =
                               good_state s
                               && steady_wind dws
                               && at_least_4 dws
                               ==>
                               let s' = (final_state s dws) [@trigger] in
                               s'.y = 0
                              [@@induct functional final_state]
                              [@@forward_chaining]
                              ;;
                              
                              Out[12]:
                              val good_state_find_and_stay_zt_zero : state -> int list -> bool = <fun>
                              Goal:
                              
                              good_state s && steady_wind dws && at_least_4 dws
                              ==> let (s' : state) = final_state s dws in s'.y = 0.
                              
                              1 nontautological subgoal.
                              
                              We shall induct according to a scheme derived from final_state.
                              
                              Induction scheme:
                              
                               (Is_a([], dws) ==> φ dws s)
                               && (not Is_a([], dws) && φ (List.tl dws) (next_state (List.hd dws) s)
                                   ==> φ dws s).
                              
                              2 nontautological subgoals.
                              
                              Subgoal 2:
                              
                               H0. Is_a([], dws)
                               H1. good_state s
                               H2. List.for_all (fun x -> x = 0) dws
                               H3. dws <> []
                               H4. (List.tl dws) <> []
                               H5. (List.tl (List.tl dws)) <> []
                               H6. (List.tl (List.tl (List.tl dws))) <> []
                              |---------------------------------------------------------------------------
                               (final_state s dws).y = 0
                              
                              But simplification reduces this to true, using the forward-chaining rule
                              all_good.
                              
                              Subgoal 1:
                              
                               H0. not Is_a([], dws)
                               H1. ((((good_state (next_state (List.hd dws) s)
                                       && List.for_all (fun x -> x = 0) (List.tl dws))
                                      && (List.tl dws) <> [])
                                     && (List.tl (List.tl dws)) <> [])
                                    && (List.tl (List.tl (List.tl dws))) <> [])
                                   && (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                                   ==> (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               H2. good_state s
                               H3. List.for_all (fun x -> x = 0) dws
                               H4. dws <> []
                               H5. (List.tl dws) <> []
                               H6. (List.tl (List.tl dws)) <> []
                               H7. (List.tl (List.tl (List.tl dws))) <> []
                              |---------------------------------------------------------------------------
                               (final_state s dws).y = 0
                              
                              This simplifies, using the definitions of List.for_all and final_state to the
                              following 4 subgoals:
                              
                              Subgoal 1.4:
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. List.hd dws = 0
                               H5. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. good_state (next_state (List.hd dws) s)
                               C2. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all, and the rewrite rule safety_1.
                              
                              Subgoal 1.3:
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. good_state (next_state (List.hd dws) s)
                               H5. List.hd dws = 0
                               H6. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C2. List.hd (List.tl dws) = 0
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.2:
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. good_state (next_state (List.hd dws) s)
                               H5. List.hd (List.tl dws) = 0
                               H6. List.hd dws = 0
                               H7. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C2. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.1:
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. good_state (next_state (List.hd dws) s)
                               H5. List.hd (List.tl dws) = 0
                               H6. List.hd dws = 0
                               H7. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                               H8. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C2. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              This simplifies, using the definition of List.for_all, and the rewrite rule
                              safety_1 to:
                              
                              Subgoal 1.1':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. List.hd (List.tl dws) = 0
                               H5. List.hd dws = 0
                               H6. List.hd (List.tl (List.tl dws)) = 0
                               H7. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C2. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              This simplifies, using the definition of List.for_all to:
                              
                              Subgoal 1.1'':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. List.hd (List.tl dws) = 0
                               H5. List.hd dws = 0
                               H6. List.hd (List.tl (List.tl dws)) = 0
                               H7. List.hd (List.tl (List.tl (List.tl dws))) = 0
                               H8. List.for_all (fun x -> x = 0)
                                   (List.tl (List.tl (List.tl (List.tl dws))))
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C2. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              This simplifies, using the definition of List.for_all to:
                              
                              Subgoal 1.1''':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. List.hd (List.tl dws) = 0
                               H5. List.hd dws = 0
                               H6. List.hd (List.tl (List.tl dws)) = 0
                               H7. List.hd (List.tl (List.tl (List.tl dws))) = 0
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C2. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              This further simplifies to:
                              
                              Subgoal 1.1'''':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. List.hd (List.tl dws) = 0
                               H5. List.hd dws = 0
                               H6. List.hd (List.tl (List.tl dws)) = 0
                               H7. List.hd (List.tl (List.tl (List.tl dws))) = 0
                              |---------------------------------------------------------------------------
                               C0. Is_a([], dws)
                               C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C2. (final_state (next_state 0 s) (List.tl dws)).y = 0
                              
                              But we verify Subgoal 1.1'''' by recursive unrolling.
                              
                               Rules:
                                  (:def List.for_all)
                                  (:def final_state)
                                  (:rw safety_1)
                                  (:fc all_good)
                                  (:induct final_state)
                              
                              
                              Proved
                              proof
                              ground_instances4
                              definitions18
                              inductions1
                              search_time
                              1.970s
                              details
                              Expand
                              smt_stats
                              num checks9
                              arith-assume-eqs8
                              arith-make-feasible338
                              arith-max-columns72
                              arith-conflicts10
                              rlimit count221574
                              arith-gcd-calls1
                              arith-cheap-eqs383
                              mk clause2539
                              datatype occurs check86
                              mk bool var1164
                              arith-lower747
                              arith-diseq1132
                              decisions260
                              arith-propagations978
                              arith-patches-success1
                              propagations3819
                              arith-patches1
                              interface eqs8
                              arith-bound-propagations-cheap978
                              arith-max-rows36
                              conflicts65
                              datatype accessor ax16
                              minimized lits298
                              arith-bound-propagations-lp225
                              datatype constructor ax27
                              final checks12
                              added eqs3430
                              del clause1029
                              arith eq adapter381
                              arith-upper967
                              time0.030000
                              memory48.080000
                              max memory68.470000
                              num allocs12939811291.000000
                              Expand
                              • start[1.970s, "Goal"]
                                  let (_x_0 : int list) = List.tl ( :var_1: ) in
                                  good_state ( :var_0: )
                                  && List.for_all (fun x -> x = 0) ( :var_1: )
                                     && (if ( :var_1: ) <> []
                                         then
                                           if _x_0 <> []
                                           then if (List.tl _x_0) <> [] then … <> [] else false else false
                                         else false)
                                  ==> (final_state ( :var_0: ) ( :var_1: )).y = 0
                              • subproof

                                let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not (_x_0 <> [])) || not (_x_1 <> [])) || not ((List.tl _x_1) <> [])) || (final_state s dws).y = 0
                                • start[1.970s, "1"]
                                    let (_x_0 : int list) = List.tl dws in
                                    let (_x_1 : int list) = List.tl _x_0 in
                                    (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws))
                                        || not (dws <> []))
                                       || not (_x_0 <> []))
                                      || not (_x_1 <> []))
                                     || not ((List.tl _x_1) <> []))
                                    || (final_state s dws).y = 0
                                • induction on (functional final_state)
                                  :scheme (Is_a([], dws) ==> φ dws s)
                                          && (not Is_a([], dws)
                                              && φ (List.tl dws) (next_state (List.hd dws) s) ==> φ dws s)
                                • Split (let (_x_0 : bool) = (final_state s dws).y = 0 in
                                         let (_x_1 : bool) = not Is_a([], dws) in
                                         let (_x_2 : int list) = List.tl dws in
                                         let (_x_3 : bool) = _x_2 <> [] in
                                         let (_x_4 : int list) = List.tl _x_2 in
                                         let (_x_5 : bool) = _x_4 <> [] in
                                         let (_x_6 : int list) = List.tl _x_4 in
                                         let (_x_7 : bool) = _x_6 <> [] in
                                         let (_x_8 : bool)
                                             = not
                                               (((((good_state s && List.for_all (fun x -> x = 0) dws)
                                                   && dws <> [])
                                                  && _x_3)
                                                 && _x_5)
                                                && _x_7)
                                         in
                                         let (_x_9 : state) = next_state (List.hd dws) s in
                                         ((_x_0 || _x_1) || _x_8)
                                         && ((_x_0
                                              || not
                                                 (_x_1
                                                  && (not
                                                      (((((good_state _x_9
                                                           && List.for_all (fun x -> x = 0) _x_2)
                                                          && _x_3)
                                                         && _x_5)
                                                        && _x_7)
                                                       && (List.tl _x_6) <> [])
                                                      || (final_state _x_9 _x_2).y = 0)))
                                             || _x_8)
                                         :cases [let (_x_0 : int list) = List.tl dws in
                                                 let (_x_1 : int list) = List.tl _x_0 in
                                                 ((((((not Is_a([], dws) || not (good_state s))
                                                      || not (List.for_all (fun x -> x = 0) dws))
                                                     || not (dws <> []))
                                                    || not (_x_0 <> []))
                                                   || not (_x_1 <> []))
                                                  || not ((List.tl _x_1) <> []))
                                                 || (final_state s dws).y = 0;
                                                 let (_x_0 : state) = next_state (List.hd dws) s in
                                                 let (_x_1 : int list) = List.tl dws in
                                                 let (_x_2 : bool) = _x_1 <> [] in
                                                 let (_x_3 : int list) = List.tl _x_1 in
                                                 let (_x_4 : bool) = _x_3 <> [] in
                                                 let (_x_5 : int list) = List.tl _x_3 in
                                                 let (_x_6 : bool) = _x_5 <> [] in
                                                 (((((((Is_a([], dws)
                                                        || not
                                                           (((((good_state _x_0
                                                                && List.for_all (fun x -> x = 0) _x_1)
                                                               && _x_2)
                                                              && _x_4)
                                                             && _x_6)
                                                            && (List.tl _x_5) <> []
                                                            ==> (final_state _x_0 _x_1).y = 0))
                                                       || not (good_state s))
                                                      || not (List.for_all (fun x -> x = 0) dws))
                                                     || not (dws <> []))
                                                    || not _x_2)
                                                   || not _x_4)
                                                  || not _x_6)
                                                 || (final_state s dws).y = 0])
                                  • subproof
                                    let (_x_0 : state) = next_state (List.hd dws) s in let (_x_1 : int list) = List.tl dws in let (_x_2 : bool) = _x_1 <> [] in let (_x_3 : int list) = List.tl _x_1 in let (_x_4 : bool) = _x_3 <> [] in let (_x_5 : int list) = List.tl _x_3 in let (_x_6 : bool) = _x_5 <> [] in (((((((Is_a([], dws) || not (((((good_state _x_0 && List.for_all (fun x -> x = 0) _x_1) && _x_2) && _x_4) && _x_6) && (List.tl _x_5) <> [] ==> (final_state _x_0 _x_1).y = 0)) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not _x_2) || not _x_4) || not _x_6) || (final_state s dws).y = 0
                                    • start[1.969s, "1"]
                                        let (_x_0 : state) = next_state (List.hd dws) s in
                                        let (_x_1 : int list) = List.tl dws in
                                        let (_x_2 : bool) = _x_1 <> [] in
                                        let (_x_3 : int list) = List.tl _x_1 in
                                        let (_x_4 : bool) = _x_3 <> [] in
                                        let (_x_5 : int list) = List.tl _x_3 in
                                        let (_x_6 : bool) = _x_5 <> [] in
                                        (((((((Is_a([], dws)
                                               || not
                                                  (((((good_state _x_0 && List.for_all (fun x -> x = 0) _x_1)
                                                      && _x_2)
                                                     && _x_4)
                                                    && _x_6)
                                                   && (List.tl _x_5) <> [] ==> (final_state _x_0 _x_1).y = 0))
                                              || not (good_state s))
                                             || not (List.for_all (fun x -> x = 0) dws))
                                            || not (dws <> []))
                                           || not _x_2)
                                          || not _x_4)
                                         || not _x_6)
                                        || (final_state s dws).y = 0
                                    • simplify
                                      into
                                      let (_x_0 : bool) = Is_a([], dws) in
                                      let (_x_1 : int) = List.hd dws in
                                      let (_x_2 : state) = next_state _x_1 s in
                                      let (_x_3 : bool) = good_state _x_2 in
                                      let (_x_4 : int list) = List.tl dws in
                                      let (_x_5 : bool) = (final_state _x_2 _x_4).y = 0 in
                                      let (_x_6 : bool) = not (good_state s) in
                                      let (_x_7 : int list) = List.tl _x_4 in
                                      let (_x_8 : int list) = List.tl _x_7 in
                                      let (_x_9 : bool) = not (_x_8 <> []) in
                                      let (_x_10 : bool) = not (_x_4 <> []) in
                                      let (_x_11 : bool) = not (_x_7 <> []) in
                                      let (_x_12 : bool) = not (_x_1 = 0) in
                                      let (_x_13 : bool) = not (List.for_all (fun x -> x = 0) _x_4) in
                                      let (_x_14 : bool) = not _x_3 in
                                      let (_x_15 : bool)
                                          = (((((_x_0 || _x_5) || _x_6) || _x_9) || _x_10) || _x_11) || _x_14
                                      in
                                      let (_x_16 : bool) = List.hd _x_4 = 0 in
                                      let (_x_17 : bool) = not _x_16 in
                                      let (_x_18 : bool) = List.for_all (fun x -> x = 0) _x_7 in
                                      ((((((((((_x_0 || _x_3) || _x_5) || _x_6) || _x_9) || _x_10) || _x_11)
                                          || _x_12)
                                         || _x_13)
                                        && (((_x_15 || _x_12) || _x_16) || _x_13))
                                       && ((((_x_15 || _x_17) || _x_12) || _x_18) || _x_13))
                                      && (((((((((((_x_0 || (List.tl _x_8) <> []) || _x_5) || _x_6) || _x_9)
                                                || _x_10)
                                               || _x_11)
                                              || _x_14)
                                             || _x_17)
                                            || _x_12)
                                           || not _x_18)
                                          || _x_13)
                                      expansions
                                      [final_state, List.for_all, final_state, List.for_all, final_state,
                                       List.for_all, final_state, List.for_all, final_state, List.for_all,
                                       List.for_all]
                                      rewrite_steps
                                        forward_chaining
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • Subproof
                                        • Subproof
                                        • Subproof
                                        • Subproof
                                    • subproof
                                      let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in ((((((not Is_a([], dws) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not (_x_0 <> [])) || not (_x_1 <> [])) || not ((List.tl _x_1) <> [])) || (final_state s dws).y = 0
                                      • start[1.969s, "2"]
                                          let (_x_0 : int list) = List.tl dws in
                                          let (_x_1 : int list) = List.tl _x_0 in
                                          ((((((not Is_a([], dws) || not (good_state s))
                                               || not (List.for_all (fun x -> x = 0) dws))
                                              || not (dws <> []))
                                             || not (_x_0 <> []))
                                            || not (_x_1 <> []))
                                           || not ((List.tl _x_1) <> []))
                                          || (final_state s dws).y = 0
                                      • simplify
                                        into
                                        true
                                        expansions
                                        []
                                        rewrite_steps
                                          forward_chaining
                                          • all_good
                                          • all_good
                                          • all_good

                                  You may enjoy reading the above proof! Now, we prove the final part of our main safety theorem.

                                  In [13]:
                                  #enable good_state;;
                                  
                                  theorem good_state_find_and_stay_0_from_origin dws =
                                   steady_wind dws
                                   && at_least_4 dws
                                   ==>
                                   let s' = final_state {y=0;w=0;v=0} dws in
                                   s'.y = 0
                                  [@@simp]
                                  
                                  Out[13]:
                                  val good_state_find_and_stay_0_from_origin : int list -> bool = <fun>
                                  
                                  Proved
                                  proof
                                  ground_instances0
                                  definitions0
                                  inductions0
                                  search_time
                                  0.080s
                                  details
                                  Expand
                                  smt_stats
                                  rlimit count15174
                                  time0.016000
                                  memory50.480000
                                  max memory68.470000
                                  num allocs13243331112.000000
                                  Expand
                                  • start[0.080s]
                                      let (_x_0 : int list) = List.tl ( :var_0: ) in
                                      List.for_all (fun x -> x = 0) ( :var_0: )
                                      && (if ( :var_0: ) <> []
                                          then
                                            if _x_0 <> [] then if (List.tl _x_0) <> [] then … <> [] else false
                                            else false
                                          else false)
                                      ==> (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y = 0
                                  • simplify

                                    into
                                    let (_x_0 : int list) = List.tl ( :var_0: ) in
                                    not
                                    ((((List.for_all (fun x -> x = 0) ( :var_0: ) && ( :var_0: ) <> [])
                                       && _x_0 <> [])
                                      && (List.tl _x_0) <> [])
                                     && … <> [])
                                    || (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y = 0
                                    expansions
                                    []
                                    rewrite_steps
                                      forward_chaining
                                      • simplify

                                        into
                                        true
                                        expansions
                                        []
                                        rewrite_steps
                                          forward_chaining
                                          • all_good
                                          • good_state_find_and_stay_zt_zero
                                        • Unsat

                                        Experiments with a flawed version

                                        Now that we've verified the controller, let us imagine instead that we'd made a mistake in its design and use Imandra to find such a mistake. For example, what if we'd defined the controller as follows?

                                        In [14]:
                                        let bad_controller sgn_y sgn_old_y =
                                          (-4 * sgn_y) + (2 * sgn_old_y)
                                        
                                        Out[14]:
                                        val bad_controller : int -> int -> int = <fun>
                                        
                                        In [15]:
                                        let bad_next_state dw s =
                                          { w = s.w + dw;
                                            y = s.y + s.v + s.w + dw;
                                            v = s.v +
                                                bad_controller
                                                  (sgn (s.y + s.v + s.w + dw))
                                                  (sgn s.y)
                                          }
                                        
                                        Out[15]:
                                        val bad_next_state : int -> state -> state = <fun>
                                        
                                        In [16]:
                                        let rec bad_final_state s dws =
                                          match dws with
                                          | [] -> s
                                          | dw :: dws' ->
                                            let s' = bad_next_state dw s in
                                            bad_final_state s' dws'
                                        [@@adm dws]
                                        
                                        Out[16]:
                                        val bad_final_state : state -> int list -> state = <fun>
                                        
                                        termination proof

                                        Termination proof

                                        call `bad_final_state (bad_next_state (List.hd dws) s) (List.tl dws)` from `bad_final_state s dws`
                                        originalbad_final_state s dws
                                        subbad_final_state (bad_next_state (List.hd dws) s) (List.tl dws)
                                        original ordinalOrdinal.Int (_cnt dws)
                                        sub ordinalOrdinal.Int (_cnt (List.tl dws))
                                        path[not Is_a([], dws)]
                                        proof
                                        detailed proof
                                        ground_instances3
                                        definitions0
                                        inductions0
                                        search_time
                                        0.013s
                                        details
                                        Expand
                                        smt_stats
                                        num checks8
                                        arith-make-feasible18
                                        arith-max-columns16
                                        arith-conflicts2
                                        rlimit count2024
                                        mk clause20
                                        datatype occurs check12
                                        mk bool var56
                                        arith-lower15
                                        arith-diseq1
                                        datatype splits1
                                        decisions15
                                        propagations14
                                        arith-max-rows4
                                        conflicts7
                                        datatype accessor ax7
                                        datatype constructor ax5
                                        final checks4
                                        added eqs38
                                        del clause13
                                        arith eq adapter10
                                        arith-upper12
                                        memory50.240000
                                        max memory68.470000
                                        num allocs13438393252.000000
                                        Expand
                                        • start[0.013s]
                                            let (_x_0 : int) = count.list mk_nat dws in
                                            let (_x_1 : int list) = List.tl dws in
                                            let (_x_2 : int) = count.list mk_nat _x_1 in
                                            not Is_a([], dws) && _x_0 >= 0 && _x_2 >= 0
                                            ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                        • simplify
                                          into
                                          let (_x_0 : int list) = List.tl dws in
                                          let (_x_1 : int) = count.list mk_nat _x_0 in
                                          let (_x_2 : int) = count.list mk_nat dws in
                                          (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                          || not ((not Is_a([], dws) && _x_2 >= 0) && _x_1 >= 0)
                                          expansions
                                          []
                                          rewrite_steps
                                            forward_chaining
                                            • unroll
                                              expr
                                              (|`count.list mk_nat[0]`_4014| dws_4002)
                                              expansions
                                              • unroll
                                                expr
                                                (|`count.list mk_nat[0]`_4014| (|get.::.1_4000| dws_4002))
                                                expansions
                                                • unroll
                                                  expr
                                                  (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                      (|`count.list mk_nat[0]`_4014| (|get.::.1_4…
                                                  expansions
                                                  • Unsat

                                                  Now, let's try one of our main safety theorems:

                                                  In [17]:
                                                  theorem vehicle_stays_within_3_units_of_course dws =
                                                   arbitrary_delta_ws dws
                                                   ==>
                                                   let s' = bad_final_state {y=0;w=0;v=0} dws in
                                                   -3 <= s'.y && s'.y <= 3
                                                  
                                                  Out[17]:
                                                  val vehicle_stays_within_3_units_of_course : int list -> bool = <fun>
                                                  module CX : sig val dws : int list end
                                                  Error: vehicle_stays_within_3_units_of_course is not a theorem.
                                                  
                                                  Counterexample (after 8 steps, 0.027s):
                                                   let (dws : int list) = [1; 1; 1]
                                                  
                                                  Refuted
                                                  proof attempt
                                                  ground_instances8
                                                  definitions0
                                                  inductions0
                                                  search_time
                                                  0.027s
                                                  details
                                                  Expand
                                                  smt_stats
                                                  num checks17
                                                  arith-assume-eqs10
                                                  arith-make-feasible196
                                                  arith-max-columns65
                                                  arith-conflicts3
                                                  rlimit count15724
                                                  arith-cheap-eqs206
                                                  mk clause961
                                                  datatype occurs check101
                                                  mk bool var724
                                                  arith-lower280
                                                  arith-diseq457
                                                  datatype splits7
                                                  decisions148
                                                  arith-propagations355
                                                  propagations1357
                                                  interface eqs10
                                                  arith-bound-propagations-cheap355
                                                  arith-max-rows35
                                                  conflicts46
                                                  datatype accessor ax71
                                                  minimized lits32
                                                  arith-bound-propagations-lp163
                                                  datatype constructor ax73
                                                  final checks26
                                                  added eqs1168
                                                  del clause148
                                                  arith eq adapter180
                                                  arith-upper468
                                                  time0.002000
                                                  memory51.680000
                                                  max memory68.470000
                                                  num allocs13635122829.000000
                                                  Expand
                                                  • start[0.027s]
                                                      let (_x_0 : int) = (bad_final_state {w = 0; y = 0; v = 0} ( :var_0: )).y in
                                                      List.for_all (fun x -> x = -1 || x = 0 || x = 1) ( :var_0: )
                                                      ==> -3 <= _x_0 && _x_0 <= 3
                                                  • simplify

                                                    into
                                                    let (_x_0 : int) = (bad_final_state {w = 0; y = 0; v = 0} ( :var_0: )).y in
                                                    not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) ( :var_0: ))
                                                    || -3 <= _x_0 && _x_0 <= 3
                                                    expansions
                                                    []
                                                    rewrite_steps
                                                      forward_chaining
                                                      • unroll
                                                        expr
                                                        (bad_final_state_114 (|rec_mk.state_4060| 0 0 0) dws_4054)
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4056| dws_4054)
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (bad_final_state_114
                                                              (bad_next_state_111 (|get.::.0_4052| dws_4054) (|rec_mk.state_4060| 0 0 0))
                                                             …
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4056|
                                                                (|get.::.1_4053| dws_4054))
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (bad_final_state_114
                                                                  (bad_next_state_111
                                                                    (|get.::.0_4052| (|get.::.1_4053| dws_4054))
                                                                    (bad…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4056|
                                                                    (|get.::.1_4053| (|get.::.1_4053| dws_4054…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (bad_next_state_111
                                                                                 (|get.::.0_4052| (|get.::.1_4053| (|get.::.1_4053| dws_4…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4056|
                                                                        (|get.::.1_4053| (|get.::.1_4053| (|get.::…
                                                                      expansions
                                                                      • Sat (Some let (dws : int list) = [1; 1; 1] )

                                                                      Imandra shows us that with our flawed controller, this conjecture is not true! In fact, Imandra computes a counterexample consisting of a sequence of three 1-valued wind speed sensor readings.

                                                                      If we plug these in, we can see the counterexample in action:

                                                                      In [18]:
                                                                      bad_final_state {y=0; w=0; v=0} [1;1;1]
                                                                      
                                                                      Out[18]:
                                                                      - : state = {w = 3; y = 4; v = -4}
                                                                      

                                                                      Happy verifying!