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.019s
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 allocs1167033
final checks6
added eqs50
del clause8
arith eq adapter11
memory6.670000
max memory6.670000
Expand
  • start[0.019s]
      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.<<_102| (|Ordinal.Int_93| (|count_`int list`_1114|
                                              (…
        expansions
        • unroll
          expr
          (|count_`int list`_1114| (|get.::.1_1102| dws_1104))
          expansions
          • unroll
            expr
            (|count_`int list`_1114| dws_1104)
            expansions
            • unsat
              (let ((a!1 (>= (ite (>= (|get.::.0_1101| dws_1104) 0)
                                  (|get.::.0_1101| dws_1104)…

            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.033s
            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 allocs8423138
            added eqs815
            del clause452
            arith eq adapter322
            memory7.700000
            max memory8.510000
            Expand
            • start[0.033s]
                (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_16 s_1131) (v_17 s_1131) (w_15 s_1131) dw_1132)))
                        (a!2 (= (+ (y_16 s_11…

                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:
                
                 (dws = [] ==> φ dws s)
                 && (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
                     ==> φ dws s).
                
                2 nontautological subgoals.
                
                Subgoal 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:
                
                 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.
                
                 Rules:
                    (:def List.for_all)
                    (:def final_state)
                    (:rw safety_1)
                    (:induct final_state)
                
                
                Proved
                proof
                ground_instances0
                definitions3
                inductions1
                search_time
                0.132s
                Expand
                • start[0.132s, "Goal"]
                    good_state :var_0:
                    && List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_1:
                    ==> good_state (final_state :var_0: :var_1:)
                • subproof

                  (not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || good_state (final_state s dws)
                  • start[0.132s, "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
                                 && 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)
                                      && 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
                                    && 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.131s, "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.131s, "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.036s
                      details
                      Expand
                      smt_stats
                      rlimit count7379
                      mk bool var5
                      num allocs1205431682
                      memory21.220000
                      max memory32.530000
                      Expand
                      • start[0.036s]
                          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.
                            
                            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 2:
                            
                             H0. dws = []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0) dws
                             H3. dws <> []
                             H4. (List.tl dws) <> []
                             H5. (List.tl (List.tl dws)) <> []
                             H6. (List.tl (List.tl (List.tl dws))) <> []
                            |---------------------------------------------------------------------------
                             (final_state s dws).y = 0
                            
                            But simplification reduces this to true.
                            
                            Subgoal 1:
                            
                             H0. not (dws = [])
                             H1. ((((good_state (next_state (List.hd dws) s)
                                     && List.for_all (fun x -> x = 0) (List.tl dws))
                                    && (List.tl dws) <> [])
                                   && (List.tl (List.tl dws)) <> [])
                                  && (List.tl (List.tl (List.tl dws))) <> [])
                                 && (List.tl (List.tl (List.tl (List.tl dws)))) <> []
                                 ==> (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                             H2. good_state s
                             H3. List.for_all (fun x -> x = 0) dws
                             H4. dws <> []
                             H5. (List.tl dws) <> []
                             H6. (List.tl (List.tl dws)) <> []
                             H7. (List.tl (List.tl (List.tl dws))) <> []
                            |---------------------------------------------------------------------------
                             (final_state s dws).y = 0
                            
                            This simplifies, using the definitions of List.for_all and final_state, and
                            the rewrite rule safety_1 to:
                            
                            Subgoal 1':
                            
                             H0. dws <> []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0) (List.tl dws)
                             H3. List.hd dws = 0
                             H4. (List.tl dws) <> []
                             H5. (List.tl (List.tl dws)) <> []
                             H6. (List.tl (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'':
                            
                             H0. dws <> []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                             H3. List.hd (List.tl dws) = 0
                             H4. List.hd dws = 0
                             H5. (List.tl dws) <> []
                             H6. (List.tl (List.tl dws)) <> []
                             H7. (List.tl (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''':
                            
                             H0. dws <> []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
                             H3. List.hd (List.tl (List.tl dws)) = 0
                             H4. List.hd (List.tl dws) = 0
                             H5. List.hd dws = 0
                             H6. (List.tl dws) <> []
                             H7. (List.tl (List.tl dws)) <> []
                             H8. (List.tl (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'''':
                            
                             H0. dws <> []
                             H1. good_state s
                             H2. List.for_all (fun x -> x = 0)
                                 (List.tl (List.tl (List.tl (List.tl dws))))
                             H3. List.hd (List.tl (List.tl (List.tl dws))) = 0
                             H4. List.hd (List.tl (List.tl dws)) = 0
                             H5. List.hd (List.tl dws) = 0
                             H6. List.hd dws = 0
                             H7. (List.tl dws) <> []
                             H8. (List.tl (List.tl dws)) <> []
                             H9. (List.tl (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''''':
                            
                             H0. dws <> []
                             H1. good_state s
                             H2. List.hd (List.tl (List.tl (List.tl dws))) = 0
                             H3. List.hd (List.tl (List.tl dws)) = 0
                             H4. List.hd (List.tl dws) = 0
                             H5. List.hd dws = 0
                             H6. (List.tl dws) <> []
                             H7. (List.tl (List.tl dws)) <> []
                             H8. (List.tl (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 further simplifies to:
                            
                            Subgoal 1'''''':
                            
                             H0. dws <> []
                             H1. good_state s
                             H2. List.hd (List.tl (List.tl (List.tl dws))) = 0
                             H3. List.hd (List.tl (List.tl dws)) = 0
                             H4. List.hd (List.tl dws) = 0
                             H5. List.hd dws = 0
                             H6. (List.tl dws) <> []
                             H7. (List.tl (List.tl dws)) <> []
                             H8. (List.tl (List.tl (List.tl dws))) <> []
                            |---------------------------------------------------------------------------
                             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'''''' by recursive unrolling.
                            
                             Rules:
                                (:def List.for_all)
                                (:def final_state)
                                (:rw safety_1)
                                (:fc all_good)
                                (:induct final_state)
                            
                            
                            Proved
                            proof
                            ground_instances4
                            definitions6
                            inductions1
                            search_time
                            1.519s
                            details
                            Expand
                            smt_stats
                            arith offset eqs53
                            num checks9
                            arith assert lower739
                            arith pivots108
                            rlimit count133877
                            mk clause805
                            datatype occurs check22
                            mk bool var642
                            arith assert upper743
                            decisions271
                            arith add rows1035
                            arith bound prop133
                            propagations3313
                            interface eqs1
                            conflicts103
                            arith fixed eqs74
                            datatype accessor ax12
                            minimized lits194
                            arith conflicts34
                            arith assert diseq550
                            datatype constructor ax7
                            final checks5
                            added eqs1123
                            del clause413
                            arith eq adapter384
                            memory49.590000
                            max memory60.800000
                            num allocs13665428400.000000
                            Expand
                            • start[1.519s, "Goal"]
                                good_state :var_0:
                                && List.for_all (fun x -> x = 0) :var_1:
                                   && :var_1: <> []
                                      && (List.tl :var_1:) <> []
                                         && (List.tl (List.tl :var_1:)) <> []
                                            && (List.tl (List.tl (List.tl :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 (dws <> [])) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state s dws).y = 0
                              • start[1.519s, "1"]
                                  (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws))
                                      || not (dws <> []))
                                     || not ((List.tl dws) <> []))
                                    || not ((List.tl (List.tl dws)) <> []))
                                   || not ((List.tl (List.tl (List.tl dws))) <> []))
                                  || (final_state s dws).y = 0
                              • 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 && List.for_all (fun x -> x = 0) dws)
                                                && dws <> [])
                                               && (List.tl dws) <> [])
                                              && (List.tl (List.tl dws)) <> [])
                                             && (List.tl (List.tl (List.tl dws))) <> []))
                                        || (final_state s dws).y = 0)
                                       && ((not
                                            (not (dws = [])
                                             && (not
                                                 (((((good_state (next_state (List.hd dws) s)
                                                      && List.for_all (fun x -> x = 0) (List.tl dws))
                                                     && (List.tl dws) <> [])
                                                    && (List.tl (List.tl dws)) <> [])
                                                   && (List.tl (List.tl (List.tl dws))) <> [])
                                                  && (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
                                                 || (final_state (next_state (List.hd dws) s) (List.tl dws)).y
                                                    = 0))
                                            || not
                                               (((((good_state s && List.for_all (fun x -> x = 0) dws)
                                                   && dws <> [])
                                                  && (List.tl dws) <> [])
                                                 && (List.tl (List.tl dws)) <> [])
                                                && (List.tl (List.tl (List.tl dws))) <> []))
                                           || (final_state s dws).y = 0)
                                       :cases [((((((not (dws = []) || not (good_state s))
                                                    || not (List.for_all (fun x -> x = 0) dws))
                                                   || not (dws <> []))
                                                  || not ((List.tl dws) <> []))
                                                 || not ((List.tl (List.tl dws)) <> []))
                                                || not ((List.tl (List.tl (List.tl dws))) <> []))
                                               || (final_state s dws).y = 0;
                                               (((((((dws = []
                                                      || not
                                                         (not
                                                          (((((good_state (next_state (List.hd dws) s)
                                                               && List.for_all (fun x -> x = 0) (List.tl dws))
                                                              && (List.tl dws) <> [])
                                                             && (List.tl (List.tl dws)) <> [])
                                                            && (List.tl (List.tl (List.tl dws))) <> [])
                                                           && (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
                                                          || (final_state (next_state (List.hd dws) s)
                                                              (List.tl dws)).y
                                                             = 0))
                                                     || not (good_state s))
                                                    || not (List.for_all (fun x -> x = 0) dws))
                                                   || not (dws <> []))
                                                  || not ((List.tl dws) <> []))
                                                 || not ((List.tl (List.tl dws)) <> []))
                                                || not ((List.tl (List.tl (List.tl dws))) <> []))
                                               || (final_state s dws).y = 0])
                                • subproof
                                  (((((((dws = [] || not (not (((((good_state (next_state (List.hd dws) s) && List.for_all (fun x -> x = 0) (List.tl dws)) && (List.tl dws) <> []) && (List.tl (List.tl dws)) <> []) && (List.tl (List.tl (List.tl dws))) <> []) && (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0)) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state s dws).y = 0
                                  • start[1.518s, "1"]
                                      (((((((dws = []
                                             || not
                                                (not
                                                 (((((good_state (next_state (List.hd dws) s)
                                                      && List.for_all (fun x -> x = 0) (List.tl dws))
                                                     && (List.tl dws) <> [])
                                                    && (List.tl (List.tl dws)) <> [])
                                                   && (List.tl (List.tl (List.tl dws))) <> [])
                                                  && (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
                                                 || (final_state (next_state (List.hd dws) s) (List.tl dws)).y =
                                                    0))
                                            || not (good_state s))
                                           || not (List.for_all (fun x -> x = 0) dws))
                                          || not (dws <> []))
                                         || not ((List.tl dws) <> []))
                                        || not ((List.tl (List.tl dws)) <> []))
                                       || not ((List.tl (List.tl (List.tl dws))) <> []))
                                      || (final_state s dws).y = 0
                                  • simplify
                                    into
                                    (((((((dws = [] || (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
                                          || not (good_state s))
                                         || not (List.for_all (fun x -> x = 0) (List.tl dws)))
                                        || not (List.hd dws = 0))
                                       || not ((List.tl dws) <> []))
                                      || not ((List.tl (List.tl dws)) <> []))
                                     || not ((List.tl (List.tl (List.tl dws))) <> []))
                                    || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                                    expansions
                                    [List.for_all, final_state]
                                    rewrite_steps
                                    safety_1
                                    forward_chaining
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                  • simplify
                                    into
                                    ((((((((not (dws <> []) || 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 dws) <> []))
                                       || not ((List.tl (List.tl dws)) <> []))
                                      || not ((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
                                    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
                                    • simplify
                                      into
                                      (((((((((not (dws <> []) || 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 dws) <> []))
                                         || not ((List.tl (List.tl dws)) <> []))
                                        || not ((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
                                      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
                                      • simplify
                                        into
                                        ((((((((((not (dws <> []) || not (good_state s))
                                                 || not
                                                    (List.for_all (fun x -> x = 0)
                                                     (List.tl (List.tl (List.tl (List.tl dws))))))
                                                || not (List.hd (List.tl (List.tl (List.tl dws))) = 0))
                                               || not (List.hd (List.tl (List.tl dws)) = 0))
                                              || not (List.hd (List.tl dws) = 0))
                                             || not (List.hd dws = 0))
                                            || not ((List.tl dws) <> []))
                                           || not ((List.tl (List.tl dws)) <> []))
                                          || not ((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
                                        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
                                        • simplify
                                          into
                                          (((((((((not (dws <> []) || not (good_state s))
                                                  || not (List.hd (List.tl (List.tl (List.tl dws))) = 0))
                                                 || not (List.hd (List.tl (List.tl dws)) = 0))
                                                || not (List.hd (List.tl dws) = 0))
                                               || not (List.hd dws = 0))
                                              || not ((List.tl dws) <> []))
                                             || not ((List.tl (List.tl dws)) <> []))
                                            || not ((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
                                          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
                                          • simplify
                                            into
                                            (((((((((not (dws <> []) || not (good_state s))
                                                    || not (List.hd (List.tl (List.tl (List.tl dws))) = 0))
                                                   || not (List.hd (List.tl (List.tl dws)) = 0))
                                                  || not (List.hd (List.tl dws) = 0))
                                                 || not (List.hd dws = 0))
                                                || not ((List.tl dws) <> []))
                                               || not ((List.tl (List.tl dws)) <> []))
                                              || not ((List.tl (List.tl (List.tl dws))) <> []))
                                             || (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
                                            || (final_state (next_state 0 s) (List.tl dws)).y = 0
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • subproof
                                                (((((((((not (:var_2: <> []) || not (if 1 = :var_3:.w + :var_3:.v && -3 = :var_3:.y then true else if 1 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true else if 2 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true else if 2 = :var_3:.w + :var_3:.v && -1 = :var_3:.y then true else …)) || not (List.hd (List.tl (List.tl (List.tl :var_2:))) = 0)) || not (List.hd (List.tl (List.tl :var_2:)) = 0)) || not (List.hd (List.tl :var_2:) = 0)) || not (List.hd :var_2: = 0)) || not ((List.tl :var_2:) <> [])) || not ((List.tl (List.tl :var_2:)) <> [])) || not ((List.tl (List.tl (List.tl :var_2:))) <> [])) || (List.tl (List.tl (List.tl (List.tl :var_2:)))) <> []) || (final_state {w = :var_3:.w + 0; y = ((:var_3:.y + :var_3:.v) + :var_3:.w) + 0; v = :var_3:.v + -3 * (if (((:var_3:.y + :var_3:.v) + :var_3:.w) + 0) < 0 then -1 else …) + 2 * (if :var_3:.y < 0 then -1 else …)} (List.tl :var_2:)).y = 0
                                                Start ((((((((((not (:var_2: <> [])
                                                                || not
                                                                   (if 1 = :var_3:.w + :var_3:.v && -3 = :var_3:.y then true
                                                                    else
                                                                    if 1 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true
                                                                    else
                                                                    if 2 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true
                                                                    else
                                                                    if 2 = :var_3:.w + :var_3:.v && -1 = :var_3:.y then true
                                                                    else …))
                                                               || not (List.hd (List.tl (List.tl (List.tl :var_2:))) = 0))
                                                              || not (List.hd (List.tl (List.tl :var_2:)) = 0))
                                                             || not (List.hd (List.tl :var_2:) = 0))
                                                            || not (List.hd :var_2: = 0))
                                                           || not ((List.tl :var_2:) <> []))
                                                          || not ((List.tl (List.tl :var_2:)) <> []))
                                                         || not ((List.tl (List.tl (List.tl :var_2:))) <> []))
                                                        || (List.tl (List.tl (List.tl (List.tl :var_2:)))) <> [])
                                                       || (final_state
                                                           {w = :var_3:.w + 0; y = ((:var_3:.y + :var_3:.v) + :var_3:.w) + 0;
                                                            v =
                                                            :var_3:.v
                                                            + -3
                                                              * (if (((:var_3:.y + :var_3:.v) + :var_3:.w) + 0) < 0 then -1
                                                                 else …)
                                                              + 2 * (if :var_3:.y < 0 then -1 else …)}
                                                           (List.tl :var_2:)).y
                                                          = 0
                                                       :time 0.031s)
                                            • subproof
                                              ((((((not (dws = []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state s dws).y = 0
                                              • start[1.518s, "2"]
                                                  ((((((not (dws = []) || not (good_state s))
                                                       || not (List.for_all (fun x -> x = 0) dws))
                                                      || not (dws <> []))
                                                     || not ((List.tl dws) <> []))
                                                    || not ((List.tl (List.tl dws)) <> []))
                                                   || not ((List.tl (List.tl (List.tl dws))) <> []))
                                                  || (final_state s dws).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.042s
                                            details
                                            Expand
                                            smt_stats
                                            rlimit count11527
                                            mk bool var5
                                            memory30.060000
                                            max memory60.800000
                                            num allocs15546450194.000000
                                            Expand
                                            • start[0.042s]
                                                List.for_all (fun x -> x = 0) :var_0:
                                                && :var_0: <> []
                                                   && (List.tl :var_0:) <> []
                                                      && (List.tl (List.tl :var_0:)) <> []
                                                         && (List.tl (List.tl (List.tl :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: && :var_0: <> [])
                                                 && (List.tl :var_0:) <> [])
                                                && (List.tl (List.tl :var_0:)) <> [])
                                               && (List.tl (List.tl (List.tl :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.012s
                                                  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
                                                  memory14.910000
                                                  max memory60.800000
                                                  num allocs16588598612.000000
                                                  Expand
                                                  • start[0.012s]
                                                      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.<<_102| (|Ordinal.Int_93| (|count_`int list`_2250|
                                                                                              (…
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (|count_`int list`_2250| (|get.::.1_2238| dws_2240))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|count_`int list`_2250| dws_2240)
                                                            expansions
                                                            • unsat
                                                              (let ((a!1 (>= (ite (>= (|get.::.0_2237| dws_2240) 0)
                                                                                  (|get.::.0_2237| dws_2240)…

                                                            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.022s):
                                                             let (dws : int list) = [1; 1; 1]
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances8
                                                            definitions0
                                                            inductions0
                                                            search_time
                                                            0.022s
                                                            details
                                                            Expand
                                                            smt_stats
                                                            arith offset eqs31
                                                            num checks17
                                                            arith assert lower274
                                                            arith pivots28
                                                            rlimit count12184
                                                            mk clause386
                                                            datatype occurs check181
                                                            mk bool var523
                                                            arith assert upper181
                                                            datatype splits41
                                                            decisions185
                                                            arith add rows92
                                                            arith bound prop52
                                                            propagations988
                                                            interface eqs10
                                                            conflicts40
                                                            arith fixed eqs74
                                                            datatype accessor ax38
                                                            minimized lits8
                                                            arith conflicts5
                                                            arith assert diseq140
                                                            datatype constructor ax46
                                                            final checks37
                                                            added eqs660
                                                            del clause100
                                                            arith eq adapter120
                                                            memory16.000000
                                                            max memory60.800000
                                                            num allocs16920269669.000000
                                                            Expand
                                                            • start[0.022s]
                                                                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_95 (|rec_mk.state_2271| 0 0 0) dws_2265)
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2267| dws_2265)
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (+ (y_16 (|rec_mk.state_2271| 0 0 0))
                                                                                    (v_17 (|rec_mk.state_2271| 0 0 0))
                                                                        …
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2267|
                                                                          (|get.::.1_2264| dws_2265))
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (let ((a!1 (+ (y_16 (|rec_mk.state_2271| 0 0 0))
                                                                                        (v_17 (|rec_mk.state_2271| 0 0 0))
                                                                            …
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2267|
                                                                              (|get.::.1_2264| (|get.::.1_2264| dws_2265…
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (let ((a!1 (+ (y_16 (|rec_mk.state_2271| 0 0 0))
                                                                                            (v_17 (|rec_mk.state_2271| 0 0 0))
                                                                                …
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2267|
                                                                                  (|get.::.1_2264| (|get.::.1_2264| (|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!