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 : 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 : int -> 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`
originalfinal_state s dws
subfinal_state (next_state (List.hd dws) s) (List.tl dws)
original ordinalOrdinal.Int (Ordinal.count dws)
sub ordinalOrdinal.Int (Ordinal.count (List.tl dws))
path[not (dws = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.024s
details
Expand
smt_stats
num checks8
arith assert lower16
arith pivots9
rlimit count2429
mk clause19
datatype occurs check21
mk bool var78
arith assert upper14
datatype splits3
decisions14
arith add rows18
propagations14
conflicts9
arith fixed eqs7
datatype accessor ax5
arith conflicts2
datatype constructor ax8
num allocs1290128507
final checks6
added eqs50
del clause8
arith eq adapter11
memory22.150000
max memory26.990000
Expand
  • start[0.024s]
      not (dws = [])
      && Ordinal.count dws >= 0 && Ordinal.count (List.tl dws) >= 0
      ==> List.tl dws = []
          || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl dws)))
             (Ordinal.Int (Ordinal.count dws))
  • simplify
    into
    (not
     ((not (dws = []) && Ordinal.count dws >= 0)
      && Ordinal.count (List.tl dws) >= 0)
     || List.tl dws = [])
    || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl dws)))
       (Ordinal.Int (Ordinal.count dws))
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_114| (|Ordinal.Int_105|
                            (|count_`int list`_1509| (|get.::.1_1497| d…
        expansions
        • unroll
          expr
          (|count_`int list`_1509| (|get.::.1_1497| dws_1499))
          expansions
          • unroll
            expr
            (|count_`int list`_1509| dws_1499)
            expansions
            • unsat
              (let ((a!1 (>= (ite (>= (|get.::.0_1496| dws_1499) 0)
                                  (|get.::.0_1496| dws_1499)…

            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_instances0
            definitions0
            inductions0
            search_time
            0.037s
            details
            Expand
            smt_stats
            arith offset eqs8
            num checks1
            arith assert lower759
            arith pivots37
            rlimit count13795
            mk clause948
            mk bool var352
            arith assert upper812
            decisions222
            arith add rows20
            arith bound prop316
            propagations3464
            conflicts104
            arith fixed eqs35
            datatype accessor ax1
            minimized lits133
            arith conflicts17
            arith assert diseq675
            datatype constructor ax1
            num allocs1412763637
            added eqs815
            del clause452
            arith eq adapter322
            memory22.300000
            max memory26.990000
            Expand
            • start[0.037s]
                (if 1 = :var_0:.w + :var_0:.v && -3 = :var_0:.y then true
                 else
                 if 1 = :var_0:.w + :var_0:.v && -2 = :var_0:.y then true
                 else
                 if 2 = :var_0:.w + :var_0:.v && -2 = :var_0:.y then true
                 else if 2 = :var_0:.w + :var_0:.v && -1 = :var_0:.y then true else …)
                && (:var_1: = -1 || :var_1: = 0 || :var_1: = 1)
                ==> (if 1 =
                        (:var_0:.w + :var_1:)
                        + :var_0:.v
                          + -3
                            * (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
                               then -1
                               else
                               if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                               then 0 else 1)
                            + 2
                              * (if :var_0:.y < 0 then -1
                                 else if :var_0:.y = 0 then 0 else 1)
                        && -3 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
                     then true
                     else
                     if 1 =
                        (:var_0:.w + :var_1:)
                        + :var_0:.v
                          + -3
                            * (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
                               then -1
                               else
                               if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                               then 0 else 1)
                            + 2
                              * (if :var_0:.y < 0 then -1
                                 else if :var_0:.y = 0 then 0 else 1)
                        && -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
                     then true
                     else
                     if 2 =
                        (:var_0:.w + :var_1:)
                        + :var_0:.v
                          + -3
                            * (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
                               then -1
                               else
                               if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                               then 0 else 1)
                            + 2
                              * (if :var_0:.y < 0 then -1
                                 else if :var_0:.y = 0 then 0 else 1)
                        && -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
                     then true
                     else
                     if 2 =
                        (:var_0:.w + :var_1:)
                        + :var_0:.v
                          + -3
                            * (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
                               then -1
                               else
                               if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                               then 0 else 1)
                            + 2
                              * (if :var_0:.y < 0 then -1
                                 else if :var_0:.y = 0 then 0 else 1)
                        && -1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
                     then true else …)
            • simplify

              into
              ((((((((((((not
                          (((((((((((((1 = :var_0:.w + :var_0:.v && -3 = :var_0:.y
                                       || 1 = :var_0:.w + :var_0:.v && -2 = :var_0:.y)
                                      || 2 = :var_0:.w + :var_0:.v && -2 = :var_0:.y)
                                     || 2 = :var_0:.w + :var_0:.v && -1 = :var_0:.y)
                                    || 3 = :var_0:.w + :var_0:.v && -1 = :var_0:.y)
                                   || -1 = :var_0:.w + :var_0:.v && 0 = :var_0:.y)
                                  || 0 = :var_0:.w + :var_0:.v && 0 = :var_0:.y)
                                 || 1 = :var_0:.w + :var_0:.v && 0 = :var_0:.y)
                                || -2 = :var_0:.w + :var_0:.v && 1 = :var_0:.y)
                               || -3 = :var_0:.w + :var_0:.v && 1 = :var_0:.y)
                              || -1 = :var_0:.w + :var_0:.v && 2 = :var_0:.y)
                             || -2 = :var_0:.w + :var_0:.v && 2 = :var_0:.y)
                            || -1 = :var_0:.w + :var_0:.v && 3 = :var_0:.y)
                           && ((:var_1: = -1 || :var_1: = 0) || :var_1: = 1))
                          || 1 =
                             (((:var_0:.w + :var_1:) + :var_0:.v)
                              + -3
                                * (if 0 <=
                                      (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                                   then
                                     if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                                     then 0 else 1
                                   else -1))
                             + 2
                               * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1
                                  else -1)
                             && -3 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                         || 1 =
                            (((:var_0:.w + :var_1:) + :var_0:.v)
                             + -3
                               * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                                  then
                                    if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                                    then 0 else 1
                                  else -1))
                            + 2
                              * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1
                                 else -1)
                            && -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                        || 2 =
                           (((:var_0:.w + :var_1:) + :var_0:.v)
                            + -3
                              * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                                 then
                                   if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                                   then 0 else 1
                                 else -1))
                           + 2
                             * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1
                                else -1)
                           && -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                       || 2 =
                          (((:var_0:.w + :var_1:) + :var_0:.v)
                           + -3
                             * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                                then
                                  if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                                  then 0 else 1
                                else -1))
                          + 2
                            * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1
                               else -1)
                          && -1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                      || 3 =
                         (((:var_0:.w + :var_1:) + :var_0:.v)
                          + -3
                            * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                               then
                                 if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                                 then 0 else 1
                               else -1))
                         + 2
                           * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                         && -1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                     || -1 =
                        (((:var_0:.w + :var_1:) + :var_0:.v)
                         + -3
                           * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                              then
                                if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                                then 0 else 1
                              else -1))
                        + 2
                          * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                        && 0 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                    || 0 =
                       (((:var_0:.w + :var_1:) + :var_0:.v)
                        + -3
                          * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                             then
                               if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
                               then 0 else 1
                             else -1))
                       + 2
                         * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                       && 0 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                   || 1 =
                      (((:var_0:.w + :var_1:) + :var_0:.v)
                       + -3
                         * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                            then
                              if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 
                              then 0 else 1
                            else -1))
                      + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                      && 0 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                  || -2 =
                     (((:var_0:.w + :var_1:) + :var_0:.v)
                      + -3
                        * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                           then
                             if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 
                             then 0 else 1
                           else -1))
                     + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                     && 1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                 || -3 =
                    (((:var_0:.w + :var_1:) + :var_0:.v)
                     + -3
                       * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                          then
                            if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 
                            then 0 else 1
                          else -1))
                    + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                    && 1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                || -1 =
                   (((:var_0:.w + :var_1:) + :var_0:.v)
                    + -3
                      * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                         then
                           if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0
                           else 1
                         else -1))
                   + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                   && 2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
               || -2 =
                  (((:var_0:.w + :var_1:) + :var_0:.v)
                   + -3
                     * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                        then
                          if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0
                          else 1
                        else -1))
                  + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                  && 2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
              || -1 =
                 (((:var_0:.w + :var_1:) + :var_0:.v)
                  + -3
                    * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:)
                       then
                         if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0
                         else 1
                       else -1))
                 + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1)
                 && 3 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
              expansions
              []
              rewrite_steps
                forward_chaining
                • unsat

                  (let ((a!1 (<= 0 (+ (y_984 s_1526) (v_985 s_1526) (w_983 s_1526) dw_1527)))
                        (a!2 (= (+ (y_984 …

                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.
                
                Subgoal 1:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                
                Must try induction.
                
                We shall induct according to a scheme derived from final_state.
                
                Induction scheme:
                
                 (dws = [] ==> φ dws s)
                 && (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
                     ==> φ dws s).
                
                2 nontautological subgoals.
                
                Subgoal 1.2:
                
                 H0. dws = []
                 H1. good_state s
                 H2. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                But simplification reduces this to true, using the definition of final_state.
                
                Subgoal 1.1:
                
                 H0. not (dws = [])
                 H1. 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))
                 H2. good_state s
                 H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                But simplification reduces this to true, using the definitions of
                List.for_all and final_state, and the rewrite rule safety_1.
                
                
                Proved
                proof
                ground_instances0
                definitions3
                inductions1
                search_time
                1.118s
                Expand
                • start[1.118s, "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[1.117s, "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 (dws = [] ==> φ dws s)
                            && (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
                                ==> φ dws s)
                  • Split ((((not (dws = []) || not (good_state s))
                             || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                            || good_state (final_state s dws))
                           && (((not
                                 (not (dws = [])
                                  && ((not (good_state (next_state (List.hd dws) s))
                                       || not
                                          (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))))
                                 || not (good_state s))
                                || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                               || good_state (final_state s dws))
                           :cases [((not (dws = []) || not (good_state s))
                                    || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                                   || good_state (final_state s dws);
                                   (((dws = []
                                      || not
                                         (not
                                          (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))))
                                     || not (good_state s))
                                    || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                                   || good_state (final_state s dws)])
                    • subproof
                      (((dws = [] || not (not (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)))) || 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.287s, "1.1"]
                          (((dws = []
                             || not
                                (not
                                 (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))))
                            || not (good_state s))
                           || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                          || good_state (final_state s dws)
                      • simplify
                        into
                        true
                        expansions
                        [List.for_all, final_state]
                        rewrite_steps
                        • safety_1
                        • safety_1
                        • safety_1
                        forward_chaining
                      • subproof
                        ((not (dws = []) || 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.287s, "1.2"]
                            ((not (dws = []) || not (good_state s))
                             || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                            || good_state (final_state s dws)
                        • simplify
                          into
                          true
                          expansions
                          final_state
                          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_instances0
                      definitions0
                      inductions0
                      search_time
                      0.165s
                      details
                      Expand
                      smt_stats
                      rlimit count10055
                      mk bool var5
                      memory31.190000
                      max memory56.530000
                      num allocs5380127495.000000
                      Expand
                      • start[0.165s]
                          List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
                          ==> -3 <= (final_state {w = 0; y = 0; v = 0} :var_0:).y
                              && (final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3
                      • simplify

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

                            into
                            true
                            expansions
                            []
                            rewrite_steps
                              forward_chaining
                              all_good
                            • unsat

                              (mp (asserted (not true)) (rewrite (= (not true) false)) false)

                            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.
                            
                            Subgoal 1:
                            
                             H0. good_state s
                             H1. List.for_all (fun x -> x = 0) dws
                             H2. (List.tl (List.tl (List.tl dws))) <> []
                             H3. (List.tl (List.tl dws)) <> []
                             H4. (List.tl dws) <> []
                             H5. dws <> []
                            |---------------------------------------------------------------------------
                             (final_state s dws).y = 0
                            
                            This simplifies, using the definition of List.for_all to:
                            
                            Subgoal 1':
                            
                             H0. good_state s
                             H1. List.for_all (fun x -> x = 0) (List.tl dws)
                             H2. List.hd dws = 0
                             H3. (List.tl (List.tl (List.tl dws))) <> []
                             H4. (List.tl (List.tl dws)) <> []
                             H5. (List.tl dws) <> []
                             H6. dws <> []
                            |---------------------------------------------------------------------------
                             (final_state s dws).y = 0
                            
                            This simplifies, using the definition of List.for_all to:
                            
                            Subgoal 1'':
                            
                             H0. good_state s
                             H1. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                             H2. List.hd (List.tl dws) = 0
                             H3. List.hd dws = 0
                             H4. (List.tl (List.tl (List.tl dws))) <> []
                             H5. (List.tl (List.tl dws)) <> []
                             H6. (List.tl dws) <> []
                             H7. dws <> []
                            |---------------------------------------------------------------------------
                             (final_state s dws).y = 0
                            
                            This simplifies, using the definition of List.for_all to:
                            
                            Subgoal 1''':
                            
                             H0. good_state s
                             H1. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
                             H2. List.hd (List.tl (List.tl dws)) = 0
                             H3. List.hd (List.tl dws) = 0
                             H4. List.hd dws = 0
                             H5. (List.tl (List.tl (List.tl dws))) <> []
                             H6. (List.tl (List.tl dws)) <> []
                             H7. (List.tl dws) <> []
                             H8. dws <> []
                            |---------------------------------------------------------------------------
                             (final_state s dws).y = 0
                            
                            
                            We can eliminate destructors by the following
                            substitution:
                             dws -> dws1 :: dws2
                            
                            This produces the modified subgoal:
                            
                            Subgoal 1'''':
                            
                             H0. good_state s
                             H1. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                             H2. List.hd (List.tl dws2) = 0
                             H3. List.hd dws2 = 0
                             H4. dws1 = 0
                             H5. (List.tl (List.tl dws2)) <> []
                             H6. (List.tl dws2) <> []
                             H7. dws2 <> []
                            |---------------------------------------------------------------------------
                             (final_state s (dws1 :: dws2)).y = 0
                            
                            This simplifies, using the definition of final_state to:
                            
                            Subgoal 1''''':
                            
                             H0. good_state s
                             H1. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                             H2. List.hd (List.tl dws2) = 0
                             H3. List.hd dws2 = 0
                             H4. (List.tl (List.tl dws2)) <> []
                             H5. (List.tl dws2) <> []
                             H6. dws2 <> []
                            |---------------------------------------------------------------------------
                             (final_state (next_state 0 s) dws2).y = 0
                            
                            
                            Must try induction.
                            
                            We shall induct according to a scheme derived from final_state.
                            
                            Induction scheme:
                            
                             (dws2 = [] ==> φ dws2 s)
                             && (not (dws2 = []) && φ (List.tl dws2) s ==> φ dws2 s).
                            
                            2 nontautological subgoals.
                            
                            Subgoal 1'''''.2:
                            
                             H0. dws2 = []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                             H3. List.hd (List.tl dws2) = 0
                             H4. List.hd dws2 = 0
                             H5. (List.tl (List.tl dws2)) <> []
                             H6. (List.tl dws2) <> []
                             H7. dws2 <> []
                            |---------------------------------------------------------------------------
                             (final_state (next_state 0 s) dws2).y = 0
                            
                            But simplification reduces this to true.
                            
                            Subgoal 1'''''.1:
                            
                             H0. not (dws2 = [])
                             H1. (((((good_state s
                                      && List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2))))
                                     && List.hd (List.tl (List.tl dws2)) = 0)
                                    && List.hd (List.tl dws2) = 0)
                                   && (List.tl (List.tl (List.tl dws2))) <> [])
                                  && (List.tl (List.tl dws2)) <> [])
                                 && (List.tl dws2) <> []
                                 ==> (final_state (next_state 0 s) (List.tl dws2)).y = 0
                             H2. good_state s
                             H3. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                             H4. List.hd (List.tl dws2) = 0
                             H5. List.hd dws2 = 0
                             H6. (List.tl (List.tl dws2)) <> []
                             H7. (List.tl dws2) <> []
                             H8. dws2 <> []
                            |---------------------------------------------------------------------------
                             (final_state (next_state 0 s) dws2).y = 0
                            
                            This simplifies, using the definition of List.for_all to the following 2
                            subgoals:
                            
                            Subgoal 1'''''.1.2:
                            
                             H0. dws2 <> []
                             H1. (final_state (next_state 0 s) (List.tl dws2)).y = 0
                             H2. (List.tl (List.tl (List.tl dws2))) <> []
                             H3. good_state s
                             H4. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))
                             H5. List.hd (List.tl (List.tl dws2)) = 0
                             H6. List.hd (List.tl dws2) = 0
                             H7. List.hd dws2 = 0
                             H8. (List.tl (List.tl dws2)) <> []
                             H9. (List.tl dws2) <> []
                            |---------------------------------------------------------------------------
                             (final_state (next_state 0 s) dws2).y = 0
                            
                            But we verify Subgoal 1'''''.1.2 by recursive unrolling.
                            
                            Subgoal 1'''''.1.1:
                            
                             H0. dws2 <> []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))
                             H3. List.hd (List.tl (List.tl dws2)) = 0
                             H4. List.hd (List.tl dws2) = 0
                             H5. List.hd dws2 = 0
                             H6. (List.tl (List.tl dws2)) <> []
                             H7. (List.tl dws2) <> []
                            |---------------------------------------------------------------------------
                             C0. (List.tl (List.tl (List.tl dws2))) <> []
                             C1. (final_state (next_state 0 s) dws2).y = 0
                            
                            This simplifies, using the definition of List.for_all to:
                            
                            Subgoal 1'''''.1.1':
                            
                             H0. dws2 <> []
                             H1. good_state s
                             H2. List.hd (List.tl (List.tl dws2)) = 0
                             H3. List.hd (List.tl dws2) = 0
                             H4. List.hd dws2 = 0
                             H5. (List.tl (List.tl dws2)) <> []
                             H6. (List.tl dws2) <> []
                            |---------------------------------------------------------------------------
                             C0. (List.tl (List.tl (List.tl dws2))) <> []
                             C1. (final_state (next_state 0 s) dws2).y = 0
                            
                            But we verify Subgoal 1'''''.1.1' by recursive unrolling.
                            
                            
                            Proved
                            proof
                            ground_instances13
                            definitions6
                            inductions1
                            search_time
                            2.856s
                            details
                            Expand
                            smt_stats
                            arith offset eqs56
                            num checks9
                            arith assert lower620
                            arith pivots96
                            rlimit count356942
                            mk clause827
                            datatype occurs check24
                            mk bool var625
                            arith assert upper599
                            decisions261
                            arith add rows815
                            arith bound prop149
                            propagations2042
                            conflicts83
                            arith fixed eqs70
                            datatype accessor ax11
                            minimized lits186
                            arith conflicts30
                            arith assert diseq426
                            datatype constructor ax6
                            final checks4
                            added eqs980
                            del clause434
                            arith eq adapter348
                            memory41.550000
                            max memory61.620000
                            num allocs34037587341.000000
                            Expand
                            • start[2.856s, "Goal"]
                                good_state :var_0:
                                && List.for_all (fun x -> x = 0) :var_1:
                                   && (List.tl (List.tl (List.tl :var_1:))) <> []
                                      && (List.tl (List.tl :var_1:)) <> []
                                         && (List.tl :var_1:) <> [] && :var_1: <> []
                                ==> (final_state :var_0: :var_1:).y = 0
                            • subproof

                              (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws)) || not ((List.tl (List.tl (List.tl dws))) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl dws) <> [])) || not (dws <> [])) || (final_state s dws).y = 0
                              • start[2.856s, "1"]
                                  (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws))
                                      || not ((List.tl (List.tl (List.tl dws))) <> []))
                                     || not ((List.tl (List.tl dws)) <> []))
                                    || not ((List.tl dws) <> []))
                                   || not (dws <> []))
                                  || (final_state s dws).y = 0
                              • simplify
                                into
                                ((((((not (good_state s) || not (List.for_all (fun x -> x = 0) (List.tl dws)))
                                     || not (List.hd dws = 0))
                                    || not ((List.tl (List.tl (List.tl dws))) <> []))
                                   || not ((List.tl (List.tl dws)) <> []))
                                  || not ((List.tl dws) <> []))
                                 || not (dws <> []))
                                || (final_state s dws).y = 0
                                expansions
                                List.for_all
                                rewrite_steps
                                  forward_chaining
                                  • all_good
                                  • all_good
                                  • all_good
                                  • all_good
                                  • all_good
                                  • all_good
                                  • all_good
                                • simplify
                                  into
                                  (((((((not (good_state s)
                                         || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws))))
                                        || not (List.hd (List.tl dws) = 0))
                                       || not (List.hd dws = 0))
                                      || not ((List.tl (List.tl (List.tl dws))) <> []))
                                     || not ((List.tl (List.tl dws)) <> []))
                                    || not ((List.tl dws) <> []))
                                   || not (dws <> []))
                                  || (final_state s dws).y = 0
                                  expansions
                                  List.for_all
                                  rewrite_steps
                                    forward_chaining
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                  • simplify
                                    into
                                    ((((((((not (good_state s)
                                            || not
                                               (List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))))
                                           || not (List.hd (List.tl (List.tl dws)) = 0))
                                          || not (List.hd (List.tl dws) = 0))
                                         || not (List.hd dws = 0))
                                        || not ((List.tl (List.tl (List.tl dws))) <> []))
                                       || not ((List.tl (List.tl dws)) <> []))
                                      || not ((List.tl dws) <> []))
                                     || not (dws <> []))
                                    || (final_state s dws).y = 0
                                    expansions
                                    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
                                    • Elim_destructor (:cstor :: :replace dws1 :: dws2 :context [])
                                    • simplify
                                      into
                                      ((((((not (good_state s)
                                            || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                           || not (List.hd (List.tl dws2) = 0))
                                          || not (List.hd dws2 = 0))
                                         || not ((List.tl (List.tl dws2)) <> []))
                                        || not ((List.tl dws2) <> []))
                                       || not (dws2 <> []))
                                      || (final_state (next_state 0 s) dws2).y = 0
                                      expansions
                                      final_state
                                      rewrite_steps
                                        forward_chaining
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                      • induction on (functional final_state)
                                        :scheme (dws2 = [] ==> φ dws2 s)
                                                && (not (dws2 = []) && φ (List.tl dws2) s ==> φ dws2 s)
                                      • Split (((((((((not (dws2 = []) || not (good_state s))
                                                      || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                     || not (List.hd (List.tl dws2) = 0))
                                                    || not (List.hd dws2 = 0))
                                                   || not ((List.tl (List.tl dws2)) <> []))
                                                  || not ((List.tl dws2) <> []))
                                                 || not (dws2 <> []))
                                                || (final_state (next_state 0 s) dws2).y = 0)
                                               && ((((((((not
                                                          (not (dws2 = [])
                                                           && (((((((not (good_state s)
                                                                     || not
                                                                        (List.for_all (fun x -> x = 0)
                                                                         (List.tl (List.tl (List.tl dws2)))))
                                                                    || not (List.hd (List.tl (List.tl dws2)) = 0))
                                                                   || not (List.hd (List.tl dws2) = 0))
                                                                  || not ((List.tl (List.tl (List.tl dws2))) <> []))
                                                                 || not ((List.tl (List.tl dws2)) <> []))
                                                                || not ((List.tl dws2) <> []))
                                                               || (final_state (next_state 0 s) (List.tl dws2)).y = 0))
                                                          || not (good_state s))
                                                         || not
                                                            (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                        || not (List.hd (List.tl dws2) = 0))
                                                       || not (List.hd dws2 = 0))
                                                      || not ((List.tl (List.tl dws2)) <> []))
                                                     || not ((List.tl dws2) <> []))
                                                    || not (dws2 <> []))
                                                   || (final_state (next_state 0 s) dws2).y = 0)
                                               :cases [(((((((not (dws2 = []) || not (good_state s))
                                                             || not
                                                                (List.for_all (fun x -> x = 0)
                                                                 (List.tl (List.tl dws2))))
                                                            || not (List.hd (List.tl dws2) = 0))
                                                           || not (List.hd dws2 = 0))
                                                          || not ((List.tl (List.tl dws2)) <> []))
                                                         || not ((List.tl dws2) <> []))
                                                        || not (dws2 <> []))
                                                       || (final_state (next_state 0 s) dws2).y = 0;
                                                       ((((((((dws2 = []
                                                               || not
                                                                  (not
                                                                   ((((((good_state s
                                                                         && List.for_all (fun x -> x = 0)
                                                                            (List.tl (List.tl (List.tl dws2))))
                                                                        && List.hd (List.tl (List.tl dws2)) = 0)
                                                                       && List.hd (List.tl dws2) = 0)
                                                                      && (List.tl (List.tl (List.tl dws2))) <> [])
                                                                     && (List.tl (List.tl dws2)) <> [])
                                                                    && (List.tl dws2) <> [])
                                                                   || (final_state (next_state 0 s) (List.tl dws2)).y
                                                                      = 0))
                                                              || not (good_state s))
                                                             || not
                                                                (List.for_all (fun x -> x = 0)
                                                                 (List.tl (List.tl dws2))))
                                                            || not (List.hd (List.tl dws2) = 0))
                                                           || not (List.hd dws2 = 0))
                                                          || not ((List.tl (List.tl dws2)) <> []))
                                                         || not ((List.tl dws2) <> []))
                                                        || not (dws2 <> []))
                                                       || (final_state (next_state 0 s) dws2).y = 0])
                                        • subproof
                                          ((((((((dws2 = [] || not (not ((((((good_state s && List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))) && List.hd (List.tl (List.tl dws2)) = 0) && List.hd (List.tl dws2) = 0) && (List.tl (List.tl (List.tl dws2))) <> []) && (List.tl (List.tl dws2)) <> []) && (List.tl dws2) <> []) || (final_state (next_state 0 s) (List.tl dws2)).y = 0)) || not (good_state s)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2)))) || not (List.hd (List.tl dws2) = 0)) || not (List.hd dws2 = 0)) || not ((List.tl (List.tl dws2)) <> [])) || not ((List.tl dws2) <> [])) || not (dws2 <> [])) || (final_state (next_state 0 s) dws2).y = 0
                                          • start[1.146s, "1'''''.1"]
                                              ((((((((dws2 = []
                                                      || not
                                                         (not
                                                          ((((((good_state s
                                                                && List.for_all (fun x -> x = 0)
                                                                   (List.tl (List.tl (List.tl dws2))))
                                                               && List.hd (List.tl (List.tl dws2)) = 0)
                                                              && List.hd (List.tl dws2) = 0)
                                                             && (List.tl (List.tl (List.tl dws2))) <> [])
                                                            && (List.tl (List.tl dws2)) <> [])
                                                           && (List.tl dws2) <> [])
                                                          || (final_state (next_state 0 s) (List.tl dws2)).y = 0))
                                                     || not (good_state s))
                                                    || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                   || not (List.hd (List.tl dws2) = 0))
                                                  || not (List.hd dws2 = 0))
                                                 || not ((List.tl (List.tl dws2)) <> []))
                                                || not ((List.tl dws2) <> []))
                                               || not (dws2 <> []))
                                              || (final_state (next_state 0 s) dws2).y = 0
                                          • simplify
                                            into
                                            ((((((((((dws2 = []
                                                      || not ((final_state (next_state 0 s) (List.tl dws2)).y = 0))
                                                     || not ((List.tl (List.tl (List.tl dws2))) <> []))
                                                    || not (good_state s))
                                                   || not
                                                      (List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))))
                                                  || not (List.hd (List.tl (List.tl dws2)) = 0))
                                                 || not (List.hd (List.tl dws2) = 0))
                                                || not (List.hd dws2 = 0))
                                               || not ((List.tl (List.tl dws2)) <> []))
                                              || not ((List.tl dws2) <> []))
                                             || (final_state (next_state 0 s) dws2).y = 0)
                                            && (((((((((dws2 = [] || (List.tl (List.tl (List.tl dws2))) <> [])
                                                       || not (good_state s))
                                                      || not
                                                         (List.for_all (fun x -> x = 0)
                                                          (List.tl (List.tl (List.tl dws2)))))
                                                     || not (List.hd (List.tl (List.tl dws2)) = 0))
                                                    || not (List.hd (List.tl dws2) = 0))
                                                   || not (List.hd dws2 = 0))
                                                  || not ((List.tl (List.tl dws2)) <> []))
                                                 || not ((List.tl dws2) <> []))
                                                || (final_state (next_state 0 s) dws2).y = 0)
                                            expansions
                                            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
                                              • Subproof
                                              • Subproof
                                          • subproof
                                            (((((((not (dws2 = []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2)))) || not (List.hd (List.tl dws2) = 0)) || not (List.hd dws2 = 0)) || not ((List.tl (List.tl dws2)) <> [])) || not ((List.tl dws2) <> [])) || not (dws2 <> [])) || (final_state (next_state 0 s) dws2).y = 0
                                            • start[1.146s, "1'''''.2"]
                                                (((((((not (dws2 = []) || not (good_state s))
                                                      || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                     || not (List.hd (List.tl dws2) = 0))
                                                    || not (List.hd dws2 = 0))
                                                   || not ((List.tl (List.tl dws2)) <> []))
                                                  || not ((List.tl dws2) <> []))
                                                 || not (dws2 <> []))
                                                || (final_state (next_state 0 s) dws2).y = 0
                                            • simplify
                                              into
                                              true
                                              expansions
                                              []
                                              rewrite_steps
                                                forward_chaining

                                          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_instances0
                                          definitions0
                                          inductions0
                                          search_time
                                          0.090s
                                          details
                                          Expand
                                          smt_stats
                                          rlimit count15862
                                          mk bool var5
                                          memory41.230000
                                          max memory61.620000
                                          num allocs36366306194.000000
                                          Expand
                                          • start[0.090s]
                                              List.for_all (fun x -> x = 0) :var_0:
                                              && (List.tl (List.tl (List.tl :var_0:))) <> []
                                                 && (List.tl (List.tl :var_0:)) <> []
                                                    && (List.tl :var_0:) <> [] && :var_0: <> []
                                              ==> (final_state {w = 0; y = 0; v = 0} :var_0:).y = 0
                                          • simplify

                                            into
                                            not
                                            ((((List.for_all (fun x -> x = 0) :var_0:
                                                && (List.tl (List.tl (List.tl :var_0:))) <> [])
                                               && (List.tl (List.tl :var_0:)) <> [])
                                              && (List.tl :var_0:) <> [])
                                             && :var_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

                                                  (mp (asserted (not true)) (rewrite (= (not true) false)) false)

                                                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`
                                                originalbad_final_state s dws
                                                subbad_final_state (bad_next_state (List.hd dws) s) (List.tl dws)
                                                original ordinalOrdinal.Int (Ordinal.count dws)
                                                sub ordinalOrdinal.Int (Ordinal.count (List.tl dws))
                                                path[not (dws = [])]
                                                proof
                                                detailed proof
                                                ground_instances3
                                                definitions0
                                                inductions0
                                                search_time
                                                0.027s
                                                details
                                                Expand
                                                smt_stats
                                                num checks8
                                                arith assert lower16
                                                arith pivots9
                                                rlimit count2429
                                                mk clause19
                                                datatype occurs check21
                                                mk bool var78
                                                arith assert upper14
                                                datatype splits3
                                                decisions14
                                                arith add rows18
                                                propagations14
                                                conflicts9
                                                arith fixed eqs7
                                                datatype accessor ax5
                                                arith conflicts2
                                                datatype constructor ax8
                                                final checks6
                                                added eqs50
                                                del clause8
                                                arith eq adapter11
                                                memory41.730000
                                                max memory61.620000
                                                num allocs36876662536.000000
                                                Expand
                                                • start[0.027s]
                                                    not (dws = [])
                                                    && Ordinal.count dws >= 0 && Ordinal.count (List.tl dws) >= 0
                                                    ==> List.tl dws = []
                                                        || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl dws)))
                                                           (Ordinal.Int (Ordinal.count dws))
                                                • simplify
                                                  into
                                                  (not
                                                   ((not (dws = []) && Ordinal.count dws >= 0)
                                                    && Ordinal.count (List.tl dws) >= 0)
                                                   || List.tl dws = [])
                                                  || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl dws)))
                                                     (Ordinal.Int (Ordinal.count dws))
                                                  expansions
                                                  []
                                                  rewrite_steps
                                                    forward_chaining
                                                    • unroll
                                                      expr
                                                      (|Ordinal.<<_114| (|Ordinal.Int_105|
                                                                          (|count_`int list`_2821| (|get.::.1_2809| d…
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (|count_`int list`_2821| (|get.::.1_2809| dws_2811))
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (|count_`int list`_2821| dws_2811)
                                                          expansions
                                                          • unsat
                                                            (let ((a!1 (>= (ite (>= (|get.::.0_2808| dws_2811) 0)
                                                                                (|get.::.0_2808| dws_2811)…

                                                          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 : int list end
                                                          Error: vehicle_stays_within_3_units_of_course is not a theorem.
                                                          
                                                          Counterexample (after 8 steps, 0.038s):
                                                           let (dws : int list) = [1; 1; 1]
                                                          
                                                          Refuted
                                                          proof attempt
                                                          ground_instances8
                                                          definitions0
                                                          inductions0
                                                          search_time
                                                          0.040s
                                                          details
                                                          Expand
                                                          smt_stats
                                                          arith offset eqs29
                                                          num checks17
                                                          arith assert lower273
                                                          arith pivots32
                                                          rlimit count12397
                                                          mk clause393
                                                          datatype occurs check181
                                                          mk bool var527
                                                          arith assert upper175
                                                          datatype splits41
                                                          decisions182
                                                          arith add rows101
                                                          arith bound prop58
                                                          propagations976
                                                          interface eqs10
                                                          conflicts41
                                                          arith fixed eqs68
                                                          datatype accessor ax38
                                                          minimized lits8
                                                          arith conflicts5
                                                          arith assert diseq142
                                                          datatype constructor ax46
                                                          final checks37
                                                          added eqs646
                                                          del clause100
                                                          arith eq adapter120
                                                          memory45.690000
                                                          max memory61.620000
                                                          num allocs37216081044.000000
                                                          Expand
                                                          • start[0.040s]
                                                              List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
                                                              ==> -3 <= (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y
                                                                  && (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3
                                                          • simplify

                                                            into
                                                            not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:)
                                                            || -3 <= (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y
                                                               && (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3
                                                            expansions
                                                            []
                                                            rewrite_steps
                                                              forward_chaining
                                                              • unroll
                                                                expr
                                                                (bad_final_state_1063 (|rec_mk.state_2842| 0 0 0) dws_2836)
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2838| dws_2836)
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (+ (y_984 (|rec_mk.state_2842| 0 0 0))
                                                                                  (v_985 (|rec_mk.state_2842| 0 0 0))
                                                                    …
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2838|
                                                                        (|get.::.1_2835| dws_2836))
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (let ((a!1 (+ (y_984 (|rec_mk.state_2842| 0 0 0))
                                                                                      (v_985 (|rec_mk.state_2842| 0 0 0))
                                                                        …
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2838|
                                                                            (|get.::.1_2835| (|get.::.1_2835| dws_2836…
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (let ((a!1 (+ (y_984 (|rec_mk.state_2842| 0 0 0))
                                                                                          (v_985 (|rec_mk.state_2842| 0 0 0))
                                                                            …
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2838|
                                                                                (|get.::.1_2835| (|get.::.1_2835| (|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!