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 : Z.t; y : Z.t; v : Z.t; }

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 : Z.t -> Z.t -> Z.t = <fun>
In [3]:
let sgn x =
  if x < 0 then -1
  else if x = 0 then 0
  else 1
Out[3]:
val sgn : Z.t -> Z.t = <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 : Z.t -> 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 : Z.t 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 -> Z.t list -> state = <fun>
termination proof

Termination proof

call `final_state (next_state (List.hd dws) s) (List.tl dws)` from `final_state s dws`
original:final_state s dws
sub:final_state (next_state (List.hd dws) s) (List.tl dws)
original ordinal:Ordinal.Int (_cnt dws)
sub ordinal:Ordinal.Int (_cnt (List.tl dws))
path:[dws <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
num checks:8
arith assert lower:11
arith tableau max rows:5
arith tableau max columns:16
arith pivots:9
rlimit count:2210
mk clause:21
datatype occurs check:12
mk bool var:75
arith assert upper:12
datatype splits:1
decisions:18
arith row summations:12
propagations:24
conflicts:10
arith fixed eqs:5
datatype accessor ax:10
arith conflicts:2
arith num rows:5
arith assert diseq:1
datatype constructor ax:9
num allocs:6013213
final checks:4
added eqs:49
del clause:11
arith eq adapter:12
memory:16.040000
max memory:16.040000
Expand
  • start[0.010s]
      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
      dws <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
      ==> not (_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
    not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
    || not (dws <> [] && (_x_2 >= 0) && (_x_1 >= 0))
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|Ordinal.<<| (|Ordinal.Int_79/boot|
                        (|count.list_399/server| (|get.::.1_385/server|…
        expansions:
        • unroll
          expr:
          (|count.list_399/server| (|get.::.1_385/server| dws_387/server))
          expansions:
          • unroll
            expr:
            (|count.list_399/server| dws_387/server)
            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 -> Z.t -> bool = <fun>
            
            Proved
            proof
            ground_instances:0
            definitions:0
            inductions:0
            search_time:
            0.017s
            details:
            Expand
            smt_stats:
            arith offset eqs:14
            num checks:1
            arith assert lower:543
            arith tableau max rows:3
            arith tableau max columns:15
            arith pivots:13
            rlimit count:11535
            mk clause:594
            mk bool var:184
            arith assert upper:469
            decisions:55
            arith row summations:18
            arith bound prop:206
            propagations:1874
            conflicts:46
            arith fixed eqs:26
            datatype accessor ax:1
            minimized lits:98
            arith conflicts:9
            arith num rows:3
            arith assert diseq:433
            datatype constructor ax:1
            num allocs:12465191
            added eqs:331
            del clause:373
            arith eq adapter:68
            time:0.010000
            memory:16.780000
            max memory:17.470000
            Expand
            • start[0.017s]
                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) || ((0 = _x_4) && _x_10)
              || (_x_5 && _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 -> Z.t 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:
                
                 (not (dws <> []) ==> φ dws s)
                 && (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 anon_fun.arbitrary_delta_ws.1 dws
                |---------------------------------------------------------------------------
                 C0. dws <> []
                 C1. 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 anon_fun.arbitrary_delta_ws.1 dws
                 H2. dws <> []
                 H3. good_state (next_state (List.hd dws) s)
                     && List.for_all anon_fun.arbitrary_delta_ws.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. dws <> []
                 H1. good_state s
                 H2. List.hd dws = 1
                 H3. List.for_all anon_fun.arbitrary_delta_ws.1 (List.tl dws)
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. good_state (next_state (List.hd dws) s)
                 C2. List.hd dws = (-1)
                 C3. List.hd dws = 0
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.2:
                
                 H0. dws <> []
                 H1. good_state s
                 H2. List.hd dws = 0
                 H3. List.for_all anon_fun.arbitrary_delta_ws.1 (List.tl dws)
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. good_state (next_state (List.hd dws) s)
                 C2. List.hd dws = (-1)
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.1:
                
                 H0. dws <> []
                 H1. good_state s
                 H2. List.hd dws = (-1)
                 H3. List.for_all anon_fun.arbitrary_delta_ws.1 (List.tl dws)
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. 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_instances:0
                definitions:11
                inductions:1
                search_time:
                0.254s
                Expand
                • start[0.254s, "Goal"]
                    good_state ( :var_0: )
                    && List.for_all anon_fun.arbitrary_delta_ws.1 ( :var_1: )
                    ==> good_state (final_state ( :var_0: ) ( :var_1: ))
                • subproof

                  not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws) || good_state (final_state s dws)
                  • start[0.254s, "1"]
                      not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws)
                      || good_state (final_state s dws)
                  • induction on (functional final_state)
                    :scheme (not (dws <> []) ==> φ dws s)
                            && (dws <> [] && φ (List.tl dws) (next_state (List.hd dws) s)
                                ==> φ dws s)
                  • Split (let (_x_0 : bool) = dws <> [] in
                           let (_x_1 : bool) = good_state (final_state s dws) in
                           let (_x_2 : bool)
                               = not
                                 (good_state s && List.for_all anon_fun.arbitrary_delta_ws.1 dws)
                           in
                           let (_x_3 : state) = next_state (List.hd dws) s in
                           let (_x_4 : int list) = List.tl dws in
                           (_x_0 || _x_1 || _x_2)
                           && (_x_1 || _x_2
                               || not
                                  (_x_0
                                   && (good_state (final_state _x_3 _x_4)
                                       || not
                                          (good_state _x_3
                                           && List.for_all anon_fun.arbitrary_delta_ws.1 _x_4))))
                           :cases [not (good_state s)
                                   || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws)
                                   || 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 anon_fun.arbitrary_delta_ws.1 dws)
                                   || not (dws <> [])
                                   || not
                                      (good_state _x_0
                                       && List.for_all anon_fun.arbitrary_delta_ws.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 anon_fun.arbitrary_delta_ws.1 dws) || not (dws <> []) || not (good_state _x_0 && List.for_all anon_fun.arbitrary_delta_ws.1 _x_1 ==> good_state (final_state _x_0 _x_1)) || good_state (final_state s dws)
                      • start[0.254s, "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 anon_fun.arbitrary_delta_ws.1 dws)
                          || not (dws <> [])
                          || not
                             (good_state _x_0 && List.for_all anon_fun.arbitrary_delta_ws.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)
                            = not (dws <> []) || good_state (final_state _x_1 _x_2)
                              || good_state _x_1 || not (good_state s)
                        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
                        let (_x_7 : bool) = not (List.for_all anon_fun.arbitrary_delta_ws.1 _x_2) in
                        (_x_5 || _x_6 || not (_x_0 = 1) || _x_7) && (_x_5 || not _x_6 || _x_7)
                        && (_x_3 || not _x_4 || _x_7)
                        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 anon_fun.arbitrary_delta_ws.1 dws) || dws <> [] || good_state (final_state s dws)
                          • start[0.254s, "2"]
                              not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws)
                              || 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 : Z.t list -> bool = <fun>
                        
                        Proved
                        proof
                        ground_instances:0
                        definitions:0
                        inductions:0
                        search_time:
                        0.028s
                        details:
                        Expand
                        smt_stats:
                        rlimit count:11177
                        num allocs:770967692
                        time:0.005000
                        memory:17.820000
                        max memory:18.450000
                        Expand
                        • start[0.028s]
                            let (_x_0 : int) = (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y in
                            List.for_all anon_fun.arbitrary_delta_ws.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 anon_fun.arbitrary_delta_ws.1 ( :var_0: ))
                          || (((-3) <= _x_0) && (_x_0 <= 3))
                          expansions:
                          []
                          rewrite_steps:
                            forward_chaining:
                            • simplify

                              into:
                              true
                              expansions:
                              []
                              rewrite_steps:
                                forward_chaining:
                                • all_good
                                • 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 : Z.t 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 -> Z.t 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:
                              
                               (not (dws <> []) ==> φ dws s)
                               && (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 anon_fun.steady_wind.1 dws
                               H2. dws <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. (List.tl (List.tl (List.tl dws))) <> []
                              |---------------------------------------------------------------------------
                               C0. dws <> []
                               C1. (final_state s dws).y = 0
                              
                              But this is immediate by our hypotheses.
                              
                              Subgoal 1:
                              
                               H0. dws <> []
                               H1. good_state (next_state (List.hd dws) s)
                                   && List.for_all anon_fun.steady_wind.1 (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 anon_fun.steady_wind.1 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. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd dws = 0
                               H6. List.for_all anon_fun.steady_wind.1 (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. good_state (next_state (List.hd dws) s)
                               C1. (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. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd dws = 0
                               H6. good_state (next_state (List.hd dws) s)
                               H7. List.for_all anon_fun.steady_wind.1 (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C1. List.hd (List.tl dws) = 0
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.2:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd dws = 0
                               H6. good_state (next_state (List.hd dws) s)
                               H7. List.for_all anon_fun.steady_wind.1 (List.tl dws)
                               H8. List.hd (List.tl dws) = 0
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C1. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl dws))
                              
                              This simplifies, using the definition of List.for_all, and the rewrite rule
                              safety_1 to the following 2 subgoals:
                              
                              Subgoal 1.2.2:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd dws = 0
                               H6. List.hd (List.tl dws) = 0
                               H7. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl dws))
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C1. List.hd (List.tl (List.tl dws)) = 0
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.2.1:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd dws = 0
                               H6. List.hd (List.tl (List.tl dws)) = 0
                               H7. List.hd (List.tl dws) = 0
                               H8. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl dws))
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C1. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl (List.tl dws)))
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.1:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd dws = 0
                               H6. good_state (next_state (List.hd dws) s)
                               H7. List.for_all anon_fun.steady_wind.1 (List.tl dws)
                               H8. List.hd (List.tl dws) = 0
                               H9. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl dws))
                              |---------------------------------------------------------------------------
                               C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C1. (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. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl (List.tl dws)))
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.hd (List.tl dws) = 0
                               H9. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl dws))
                              |---------------------------------------------------------------------------
                               C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C1. (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. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.for_all anon_fun.steady_wind.1
                                   (List.tl (List.tl (List.tl (List.tl dws))))
                               H6. List.hd (List.tl (List.tl (List.tl dws))) = 0
                               H7. List.hd dws = 0
                               H8. List.hd (List.tl (List.tl dws)) = 0
                               H9. List.hd (List.tl dws) = 0
                              |---------------------------------------------------------------------------
                               C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C1. (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. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd (List.tl (List.tl (List.tl dws))) = 0
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.hd (List.tl dws) = 0
                              |---------------------------------------------------------------------------
                               C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              This further simplifies to:
                              
                              Subgoal 1.1'''':
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl dws) <> []
                               H3. (List.tl (List.tl dws)) <> []
                               H4. (List.tl (List.tl (List.tl dws))) <> []
                               H5. List.hd (List.tl (List.tl (List.tl dws))) = 0
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.hd (List.tl dws) = 0
                              |---------------------------------------------------------------------------
                               C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                               C1. (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_instances:4
                              definitions:23
                              inductions:1
                              search_time:
                              1.077s
                              details:
                              Expand
                              smt_stats:
                              num checks:9
                              arith-assume-eqs:2
                              arith-make-feasible:237
                              arith-max-columns:79
                              arith-conflicts:11
                              rlimit count:215646
                              arith-cheap-eqs:376
                              mk clause:2296
                              datatype occurs check:19
                              mk bool var:982
                              arith-lower:653
                              arith-diseq:862
                              decisions:92
                              arith-propagations:793
                              propagations:3125
                              interface eqs:2
                              arith-bound-propagations-cheap:793
                              arith-max-rows:39
                              conflicts:56
                              datatype accessor ax:15
                              minimized lits:165
                              arith-bound-propagations-lp:345
                              datatype constructor ax:10
                              final checks:6
                              added eqs:2362
                              del clause:867
                              arith eq adapter:254
                              arith-upper:695
                              time:0.010000
                              memory:20.320000
                              max memory:20.320000
                              num allocs:12903394324.000000
                              Expand
                              • start[1.077s, "Goal"]
                                  let (_x_0 : int list) = List.tl ( :var_1: ) in
                                  good_state ( :var_0: )
                                  && (List.for_all anon_fun.steady_wind.1 ( :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 anon_fun.steady_wind.1 dws) || not (dws <> []) || not (_x_0 <> []) || not (_x_1 <> []) || not ((List.tl _x_1) <> []) || ((final_state s dws).y = 0)
                                • start[1.077s, "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 anon_fun.steady_wind.1 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 (not (dws <> []) ==> φ dws s)
                                          && (dws <> [] && φ (List.tl dws) (next_state (List.hd dws) s)
                                              ==> φ dws s)
                                • Split (let (_x_0 : bool) = dws <> [] in
                                         let (_x_1 : bool) = (final_state s dws).y = 0 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 anon_fun.steady_wind.1 dws && _x_0
                                                && _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_1
                                             || not
                                                (_x_0
                                                 && (not
                                                     (good_state _x_9
                                                      && List.for_all anon_fun.steady_wind.1 _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 : bool) = dws <> [] in
                                                 let (_x_1 : int list) = List.tl dws in
                                                 let (_x_2 : int list) = List.tl _x_1 in
                                                 not (good_state s)
                                                 || not (List.for_all anon_fun.steady_wind.1 dws) || not _x_0
                                                 || not (_x_1 <> []) || not (_x_2 <> [])
                                                 || not ((List.tl _x_2) <> []) || _x_0
                                                 || ((final_state s dws).y = 0);
                                                 let (_x_0 : bool) = not (dws <> []) in
                                                 let (_x_1 : state) = next_state (List.hd dws) s 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
                                                 _x_0
                                                 || not
                                                    (good_state _x_1
                                                     && List.for_all anon_fun.steady_wind.1 _x_2 && _x_3
                                                     && _x_5 && _x_7 && (List.tl _x_6) <> []
                                                     ==> (final_state _x_1 _x_2).y = 0)
                                                 || not (good_state s)
                                                 || not (List.for_all anon_fun.steady_wind.1 dws) || _x_0
                                                 || not _x_3 || not _x_5 || not _x_7
                                                 || ((final_state s dws).y = 0)])
                                  • subproof
                                    let (_x_0 : bool) = not (dws <> []) in let (_x_1 : state) = next_state (List.hd dws) s 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 _x_0 || not (good_state _x_1 && List.for_all anon_fun.steady_wind.1 _x_2 && _x_3 && _x_5 && _x_7 && (List.tl _x_6) <> [] ==> (final_state _x_1 _x_2).y = 0) || not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws) || _x_0 || not _x_3 || not _x_5 || not _x_7 || ((final_state s dws).y = 0)
                                    • start[1.076s, "1"]
                                        let (_x_0 : bool) = not (dws <> []) in
                                        let (_x_1 : state) = next_state (List.hd dws) s 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
                                        _x_0
                                        || not
                                           (good_state _x_1 && List.for_all anon_fun.steady_wind.1 _x_2 && _x_3
                                            && _x_5 && _x_7 && (List.tl _x_6) <> []
                                            ==> (final_state _x_1 _x_2).y = 0)
                                        || not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws)
                                        || _x_0 || not _x_3 || not _x_5 || not _x_7 || ((final_state s dws).y = 0)
                                    • simplify
                                      into:
                                      let (_x_0 : bool) = not (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 : bool) = not (_x_4 <> []) in
                                      let (_x_8 : int list) = List.tl _x_4 in
                                      let (_x_9 : bool) = not (_x_8 <> []) in
                                      let (_x_10 : int list) = List.tl _x_8 in
                                      let (_x_11 : bool) = not (_x_10 <> []) in
                                      let (_x_12 : bool) = not (_x_1 = 0) in
                                      let (_x_13 : bool) = not (List.for_all anon_fun.steady_wind.1 _x_4) in
                                      let (_x_14 : bool) = not _x_3 in
                                      let (_x_15 : bool)
                                          = _x_0 || _x_5 || _x_6 || _x_7 || _x_9 || _x_11 || _x_12 || _x_14
                                            || _x_13
                                      in
                                      let (_x_16 : bool) = List.hd _x_4 = 0 in
                                      let (_x_17 : bool) = List.for_all anon_fun.steady_wind.1 _x_8 in
                                      let (_x_18 : bool) = not _x_16 in
                                      (_x_0 || _x_3 || _x_5 || _x_6 || _x_7 || _x_9 || _x_11 || _x_12 || _x_13)
                                      && (_x_15 || _x_16) && (_x_15 || _x_17 || _x_18)
                                      && (_x_0 || (List.tl _x_10) <> [] || _x_5 || _x_6 || _x_7 || _x_9 || _x_11
                                          || _x_12 || _x_14 || _x_13 || _x_18 || not _x_17)
                                      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
                                        • Subproof
                                        • Subproof
                                        • Subproof
                                        • Subproof
                                    • subproof
                                      let (_x_0 : bool) = dws <> [] in let (_x_1 : int list) = List.tl dws in let (_x_2 : int list) = List.tl _x_1 in not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws) || not _x_0 || not (_x_1 <> []) || not (_x_2 <> []) || not ((List.tl _x_2) <> []) || _x_0 || ((final_state s dws).y = 0)
                                      start[1.076s, "2"]
                                        let (_x_0 : bool) = dws <> [] in
                                        let (_x_1 : int list) = List.tl dws in
                                        let (_x_2 : int list) = List.tl _x_1 in
                                        not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws)
                                        || not _x_0 || not (_x_1 <> []) || not (_x_2 <> [])
                                        || not ((List.tl _x_2) <> []) || _x_0 || ((final_state s dws).y = 0)

                                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 : Z.t list -> bool = <fun>
                                
                                Proved
                                proof
                                ground_instances:0
                                definitions:0
                                inductions:0
                                search_time:
                                0.048s
                                details:
                                Expand
                                smt_stats:
                                rlimit count:13694
                                time:0.008000
                                memory:19.360000
                                max memory:20.320000
                                num allocs:13310503443.000000
                                Expand
                                • start[0.048s]
                                    let (_x_0 : int list) = List.tl ( :var_0: ) in
                                    List.for_all anon_fun.steady_wind.1 ( :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 anon_fun.steady_wind.1 ( :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
                                        • 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 : Z.t -> Z.t -> Z.t = <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 : Z.t -> 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 -> Z.t 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`
                                      original:bad_final_state s dws
                                      sub:bad_final_state (bad_next_state (List.hd dws) s) (List.tl dws)
                                      original ordinal:Ordinal.Int (_cnt dws)
                                      sub ordinal:Ordinal.Int (_cnt (List.tl dws))
                                      path:[dws <> []]
                                      proof:
                                      detailed proof
                                      ground_instances:3
                                      definitions:0
                                      inductions:0
                                      search_time:
                                      0.008s
                                      details:
                                      Expand
                                      smt_stats:
                                      num checks:8
                                      arith assert lower:11
                                      arith tableau max rows:5
                                      arith tableau max columns:16
                                      arith pivots:9
                                      rlimit count:2218
                                      mk clause:21
                                      datatype occurs check:12
                                      mk bool var:75
                                      arith assert upper:12
                                      datatype splits:1
                                      decisions:18
                                      arith row summations:12
                                      propagations:24
                                      conflicts:10
                                      arith fixed eqs:5
                                      datatype accessor ax:10
                                      arith conflicts:2
                                      arith num rows:5
                                      arith assert diseq:1
                                      datatype constructor ax:9
                                      final checks:4
                                      added eqs:49
                                      del clause:11
                                      arith eq adapter:12
                                      memory:19.980000
                                      max memory:20.320000
                                      num allocs:13481338088.000000
                                      Expand
                                      • start[0.008s]
                                          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
                                          dws <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
                                          ==> not (_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
                                        not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                        || not (dws <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                        expansions:
                                        []
                                        rewrite_steps:
                                          forward_chaining:
                                          • unroll
                                            expr:
                                            (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                            (|count.list_2670/server|
                                                              (|g…
                                            expansions:
                                            • unroll
                                              expr:
                                              (|count.list_2670/server| (|get.::.1_2656/server| dws_2658/server))
                                              expansions:
                                              • unroll
                                                expr:
                                                (|count.list_2670/server| dws_2658/server)
                                                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 : Z.t list -> bool = <fun>
                                                module CX : sig val dws : Z.t list end
                                                Error:
                                                  validation failed
                                                ----------------------------------------------------------------------------
                                                Context: vehicle_stays_within_3_units_of_course is not a theorem.

                                                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!