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.018s
details
Expand
smt_stats
num checks8
arith assert lower16
arith pivots9
rlimit count2433
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 allocs1366281420
final checks6
added eqs50
del clause8
arith eq adapter11
memory16.210000
max memory18.750000
Expand
  • start[0.018s]
      not (dws = [])
      && Ordinal.count dws >= 0 && Ordinal.count (List.tl dws) >= 0
      ==> List.tl dws = []
          || Ordinal.Int (Ordinal.count (List.tl dws)) Ordinal.<<
             Ordinal.Int (Ordinal.count dws)
  • simplify
    into
    (not
     ((not (dws = []) && Ordinal.count dws >= 0)
      && Ordinal.count (List.tl dws) >= 0)
     || List.tl dws = [])
    || Ordinal.Int (Ordinal.count (List.tl dws)) Ordinal.<<
       Ordinal.Int (Ordinal.count dws)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_121| (|Ordinal.Int_112|
                            (|count_`int list`_2479| (|get.::.1_2455| d…
        expansions
        • unroll
          expr
          (|count_`int list`_2479| (|get.::.1_2455| dws_2469))
          expansions
          • unroll
            expr
            (|count_`int list`_2479| dws_2469)
            expansions
            • unsat
              (let ((a!1 (>= (ite (>= (|get.::.0_2454| dws_2469) 0)
                                  (|get.::.0_2454| dws_2469)…

            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 allocs1461827419
            added eqs815
            del clause452
            arith eq adapter322
            memory17.010000
            max memory18.750000
            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_2428 s_2518) (v_2429 s_2518) (w_2427 s_2518) dw_2519)))
                        (a!2 (= (+ (y_2…

                Warning

                Pattern will match only if `good_state` is disabled
                (non-recursive function)

                Warning

                Pattern will match only if `next_state` is disabled
                (non-recursive function)

                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)
                
                Verified up to bound 10 (after 0.340s).
                
                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 definitions of
                List.for_all and 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)
                
                This simplifies, using the definitions of List.for_all and final_state to the
                following 3 subgoals:
                
                Subgoal 1.1.3:
                
                 H0. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                 H1. List.hd dws = 1
                 H2. good_state s
                 H3. dws <> []
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. List.hd dws = -1
                 C2. List.hd dws = 0
                 C3. good_state (next_state (List.hd dws) s)
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.1.2:
                
                 H0. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                 H1. List.hd dws = 0
                 H2. good_state s
                 H3. dws <> []
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. List.hd dws = -1
                 C2. good_state (next_state (List.hd dws) s)
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.1.1:
                
                 H0. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                 H1. List.hd dws = -1
                 H2. good_state s
                 H3. dws <> []
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. good_state (next_state (List.hd dws) s)
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                
                Proved
                proof
                ground_instances0
                definitions11
                inductions1
                search_time
                0.749s
                Expand
                • start[0.749s, "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.749s, "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.375s, "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
                        ((((((((good_state (final_state (next_state (List.hd …) s) (List.tl …))
                                || not
                                   (List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl …)))
                               || List.hd … = -1)
                              || List.hd … = 0)
                             || not (List.hd … = 1))
                            || not (good_state s))
                           || good_state (next_state (List.hd …) s))
                          || … = [])
                         && ((((((good_state (final_state (next_state (List.hd …) s) (List.tl …))
                                  || not
                                     (List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl …)))
                                 || List.hd … = -1)
                                || not (List.hd … = 0))
                               || not (good_state s))
                              || good_state (next_state (List.hd …) s))
                             || … = []))
                        && (((((good_state (final_state (next_state (List.hd …) s) (List.tl …))
                                || not
                                   (List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl …)))
                               || not (List.hd … = -1))
                              || not (good_state s))
                             || good_state (next_state (List.hd …) s))
                            || … = [])
                        expansions
                        [List.for_all, final_state, final_state, final_state, List.for_all,
                         final_state, final_state, final_state, List.for_all]
                        rewrite_steps
                          forward_chaining
                            • Subproof
                            • Subproof
                            • Subproof
                        • 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.375s, "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, List.for_all]
                            rewrite_steps
                              forward_chaining

                        Theorem: Cannot get more than 3 units off course.

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

                        In [10]:
                        #enable next_state;;
                        #enable good_state;;
                        
                        theorem vehicle_stays_within_3_units_of_course dws =
                         arbitrary_delta_ws dws
                         ==>
                         let s' = final_state {y=0;w=0;v=0} dws in
                         -3 <= s'.y && s'.y <= 3
                         [@@simp]
                        
                        Out[10]:
                        val vehicle_stays_within_3_units_of_course : Z.t list -> bool = <fun>
                        
                        Proved
                        proof
                        ground_instances0
                        definitions0
                        inductions0
                        search_time
                        0.148s
                        details
                        Expand
                        smt_stats
                        rlimit count10953
                        mk bool var5
                        memory39.530000
                        max memory46.810000
                        num allocs10578967086.000000
                        Expand
                        • start[0.148s]
                            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. dws <> []
                               H1. (List.tl dws) <> []
                               H2. (List.tl (List.tl dws)) <> []
                               H3. (List.tl (List.tl (List.tl dws))) <> []
                               H4. List.for_all (fun x -> x = 0) (List.tl dws)
                               H5. List.hd dws = 0
                               H6. good_state s
                              |---------------------------------------------------------------------------
                               (final_state s dws).y = 0
                              
                              This simplifies, using the definition of List.for_all to:
                              
                              Subgoal 1'':
                              
                               H0. good_state s
                               H1. List.hd dws = 0
                               H2. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                               H3. List.hd (List.tl 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. dws <> []
                               H1. (List.tl dws) <> []
                               H2. (List.tl (List.tl dws)) <> []
                               H3. (List.tl (List.tl (List.tl dws))) <> []
                               H4. List.hd (List.tl dws) = 0
                               H5. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
                               H6. List.hd (List.tl (List.tl dws)) = 0
                               H7. List.hd dws = 0
                               H8. good_state s
                              |---------------------------------------------------------------------------
                               (final_state s dws).y = 0
                              
                              Verified up to bound 10 (after 0.075s).
                              
                              We can eliminate destructors by the following
                              substitution:
                               dws -> dws1 :: dws2
                              
                              This produces the modified subgoal:
                              
                              Subgoal 1'''':
                              
                               H0. dws2 <> []
                               H1. (List.tl dws2) <> []
                               H2. (List.tl (List.tl dws2)) <> []
                               H3. List.hd dws2 = 0
                               H4. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                               H5. List.hd (List.tl dws2) = 0
                               H6. dws1 = 0
                               H7. good_state s
                              |---------------------------------------------------------------------------
                               (final_state s (dws1 :: dws2)).y = 0
                              
                              This simplifies, using the definition of final_state to:
                              
                              Subgoal 1''''':
                              
                               H0. good_state s
                               H1. List.hd (List.tl dws2) = 0
                               H2. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                               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
                              
                              Verified up to bound 10 (after 0.067s).
                              
                              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.hd (List.tl dws2) = 0
                               H3. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                               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.hd (List.tl (List.tl dws2)) = 0)
                                       && List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2))))
                                      && 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.hd (List.tl dws2) = 0
                               H4. List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))
                               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. (List.tl dws2) <> []
                               H2. (List.tl (List.tl dws2)) <> []
                               H3. List.hd dws2 = 0
                               H4. List.hd (List.tl dws2) = 0
                               H5. good_state s
                               H6. (final_state (next_state 0 s) (List.tl dws2)).y = 0
                               H7. List.hd (List.tl (List.tl dws2)) = 0
                               H8. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))
                               H9. (List.tl (List.tl (List.tl dws2))) <> []
                              |---------------------------------------------------------------------------
                               (final_state (next_state 0 s) dws2).y = 0
                              
                              Verified up to bound 10 (after 0.044s).
                              
                              We can eliminate destructors by the following
                              substitution:
                               dws2 -> dws21 :: dws22
                              
                              This produces the modified subgoal:
                              
                              Subgoal 1'''''.1.2':
                              
                               H0. dws22 <> []
                               H1. (List.tl dws22) <> []
                               H2. dws21 = 0
                               H3. List.hd dws22 = 0
                               H4. good_state s
                               H5. (final_state (next_state 0 s) dws22).y = 0
                               H6. List.hd (List.tl dws22) = 0
                               H7. List.for_all (fun x -> x = 0) (List.tl (List.tl dws22))
                               H8. (List.tl (List.tl dws22)) <> []
                              |---------------------------------------------------------------------------
                               (final_state (next_state 0 s) (dws21 :: dws22)).y = 0
                              
                              This simplifies, using the definition of final_state to:
                              
                              Subgoal 1'''''.1.2'':
                              
                               H0. (List.tl (List.tl dws22)) <> []
                               H1. List.for_all (fun x -> x = 0) (List.tl (List.tl dws22))
                               H2. List.hd (List.tl dws22) = 0
                               H3. (final_state (next_state 0 s) dws22).y = 0
                               H4. good_state s
                               H5. List.hd dws22 = 0
                               H6. (List.tl dws22) <> []
                               H7. dws22 <> []
                              |---------------------------------------------------------------------------
                               (final_state (next_state 0 (next_state 0 s)) dws22).y = 0
                              
                              But we verify Subgoal 1'''''.1.2'' by recursive unrolling.
                              
                              Subgoal 1'''''.1.1:
                              
                               H0. dws2 <> []
                               H1. (List.tl dws2) <> []
                               H2. (List.tl (List.tl dws2)) <> []
                               H3. List.hd dws2 = 0
                               H4. List.hd (List.tl dws2) = 0
                               H5. good_state s
                               H6. List.hd (List.tl (List.tl dws2)) = 0
                               H7. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state 0 s) dws2).y = 0
                               C1. (List.tl (List.tl (List.tl dws2))) <> []
                              
                              This simplifies, using the definition of List.for_all to:
                              
                              Subgoal 1'''''.1.1':
                              
                               H0. List.hd (List.tl (List.tl dws2)) = 0
                               H1. good_state s
                               H2. List.hd (List.tl dws2) = 0
                               H3. List.hd dws2 = 0
                               H4. (List.tl (List.tl dws2)) <> []
                               H5. (List.tl dws2) <> []
                               H6. 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_instances12
                              definitions54
                              inductions1
                              search_time
                              1.301s
                              details
                              Expand
                              smt_stats
                              arith offset eqs50
                              num checks9
                              arith assert lower652
                              arith pivots82
                              rlimit count437565
                              mk clause841
                              datatype occurs check18
                              mk bool var647
                              arith assert upper677
                              decisions235
                              arith add rows754
                              arith bound prop161
                              propagations2455
                              conflicts88
                              arith fixed eqs72
                              datatype accessor ax11
                              minimized lits200
                              arith conflicts30
                              arith assert diseq526
                              datatype constructor ax6
                              final checks4
                              added eqs1023
                              del clause432
                              arith eq adapter386
                              memory48.780000
                              max memory52.140000
                              num allocs22637067455.000000
                              Expand
                              • start[1.301s, "Goal"]
                                  good_state :var_0:
                                  && List.for_all (fun x -> x = 0) :var_1:
                                     && (if (List.tl (List.tl (List.tl :var_1:))) <> []
                                            && (List.tl (List.tl :var_1:)) <> []
                                               && (List.tl :var_1:) <> [] && :var_1: <> []
                                         then true else false)
                                  ==> (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[1.301s, "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
                                  (((((((final_state s dws).y = 0 || not (dws <> []))
                                       || not ((List.tl dws) <> []))
                                      || not ((List.tl (List.tl dws)) <> []))
                                     || not ((List.tl (List.tl (List.tl dws))) <> []))
                                    || not (List.for_all (fun x -> x = 0) (List.tl dws)))
                                   || not (List.hd dws = 0))
                                  || not (good_state s)
                                  expansions
                                  List.for_all
                                  rewrite_steps
                                    forward_chaining
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                    • all_good
                                  • simplify
                                    into
                                    ((((((((final_state s dws).y = 0 || not (good_state s))
                                          || not (List.hd dws = 0))
                                         || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws))))
                                        || not (List.hd (List.tl dws) = 0))
                                       || not ((List.tl (List.tl (List.tl dws))) <> []))
                                      || not ((List.tl (List.tl dws)) <> []))
                                     || not ((List.tl dws) <> []))
                                    || not (dws <> [])
                                    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
                                      (((((((((final_state s dws).y = 0 || not (dws <> []))
                                             || not ((List.tl dws) <> []))
                                            || not ((List.tl (List.tl dws)) <> []))
                                           || not ((List.tl (List.tl (List.tl dws))) <> []))
                                          || not (List.hd (List.tl dws) = 0))
                                         || 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 dws = 0))
                                      || not (good_state s)
                                      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
                                        (((((((final_state (next_state 0 s) dws2).y = 0 || not (good_state s))
                                             || not (List.hd (List.tl dws2) = 0))
                                            || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                           || not (List.hd dws2 = 0))
                                          || not ((List.tl (List.tl dws2)) <> []))
                                         || not ((List.tl dws2) <> []))
                                        || not (dws2 <> [])
                                        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.hd (List.tl dws2) = 0))
                                                       || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                      || 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.hd (List.tl (List.tl dws2)) = 0))
                                                                      || not
                                                                         (List.for_all (fun x -> x = 0)
                                                                          (List.tl (List.tl (List.tl dws2)))))
                                                                     || 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.hd (List.tl dws2) = 0))
                                                          || not
                                                             (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                         || 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.hd (List.tl dws2) = 0))
                                                              || not
                                                                 (List.for_all (fun x -> x = 0)
                                                                  (List.tl (List.tl dws2))))
                                                             || 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.hd (List.tl (List.tl dws2)) = 0)
                                                                          && List.for_all (fun x -> x = 0)
                                                                             (List.tl (List.tl (List.tl dws2))))
                                                                         && 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.hd (List.tl dws2) = 0))
                                                              || not
                                                                 (List.for_all (fun x -> x = 0)
                                                                  (List.tl (List.tl dws2))))
                                                             || 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.hd (List.tl (List.tl dws2)) = 0) && List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))) && 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.hd (List.tl dws2) = 0)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2)))) || 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[0.773s, "1'''''.1"]
                                                ((((((((dws2 = []
                                                        || not
                                                           (not
                                                            ((((((good_state s && List.hd (List.tl (List.tl dws2)) = 0)
                                                                 && List.for_all (fun x -> x = 0)
                                                                    (List.tl (List.tl (List.tl dws2))))
                                                                && 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.hd (List.tl dws2) = 0))
                                                     || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                    || 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
                                              (((((((((((final_state (next_state 0 s) dws2).y = 0 || not (dws2 <> []))
                                                       || not ((List.tl dws2) <> []))
                                                      || not ((List.tl (List.tl dws2)) <> []))
                                                     || not (List.hd dws2 = 0))
                                                    || not (List.hd (List.tl dws2) = 0))
                                                   || not (good_state s))
                                                  || not ((final_state (next_state 0 s) (List.tl dws2)).y = 0))
                                                 || not (List.hd (List.tl (List.tl dws2)) = 0))
                                                || not (List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))))
                                               || not ((List.tl (List.tl (List.tl dws2))) <> []))
                                              && ((((((((((final_state (next_state 0 s) dws2).y = 0 || not (dws2 <> []))
                                                         || not ((List.tl dws2) <> []))
                                                        || not ((List.tl (List.tl dws2)) <> []))
                                                       || not (List.hd dws2 = 0))
                                                      || not (List.hd (List.tl dws2) = 0))
                                                     || not (good_state s))
                                                    || not (List.hd (List.tl (List.tl dws2)) = 0))
                                                   || not
                                                      (List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws2)))))
                                                  || (List.tl (List.tl (List.tl dws2))) <> [])
                                              expansions
                                              [List.for_all, List.for_all, List.for_all, List.for_all]
                                              rewrite_steps
                                                forward_chaining
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • all_good
                                                • Subproof
                                                • Subproof
                                            • subproof
                                              (((((((not (dws2 = []) || not (good_state s)) || not (List.hd (List.tl dws2) = 0)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2)))) || 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[0.773s, "1'''''.2"]
                                                  (((((((not (dws2 = []) || not (good_state s))
                                                        || not (List.hd (List.tl dws2) = 0))
                                                       || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws2))))
                                                      || 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.182s
                                            details
                                            Expand
                                            smt_stats
                                            rlimit count16898
                                            mk bool var5
                                            memory47.420000
                                            max memory52.140000
                                            num allocs30750058543.000000
                                            Expand
                                            • start[0.182s]
                                                List.for_all (fun x -> x = 0) :var_0:
                                                && (if (List.tl (List.tl (List.tl :var_0:))) <> []
                                                       && (List.tl (List.tl :var_0:)) <> []
                                                          && (List.tl :var_0:) <> [] && :var_0: <> []
                                                    then true else false)
                                                ==> (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.017s
                                                  details
                                                  Expand
                                                  smt_stats
                                                  num checks8
                                                  arith assert lower17
                                                  arith pivots9
                                                  rlimit count19327
                                                  mk clause19
                                                  datatype occurs check22
                                                  mk bool var78
                                                  arith assert upper13
                                                  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
                                                  memory44.630000
                                                  max memory52.140000
                                                  num allocs31541045069.000000
                                                  Expand
                                                  • start[0.017s]
                                                      not (dws = [])
                                                      && Ordinal.count dws >= 0 && Ordinal.count (List.tl dws) >= 0
                                                      ==> List.tl dws = []
                                                          || Ordinal.Int (Ordinal.count (List.tl dws)) Ordinal.<<
                                                             Ordinal.Int (Ordinal.count dws)
                                                  • simplify
                                                    into
                                                    (not
                                                     ((not (dws = []) && Ordinal.count dws >= 0)
                                                      && Ordinal.count (List.tl dws) >= 0)
                                                     || List.tl dws = [])
                                                    || Ordinal.Int (Ordinal.count (List.tl dws)) Ordinal.<<
                                                       Ordinal.Int (Ordinal.count dws)
                                                    expansions
                                                    []
                                                    rewrite_steps
                                                      forward_chaining
                                                      • unroll
                                                        expr
                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                            (|count_`int list`_2888| (|get.::.1_2838| d…
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (|count_`int list`_2888| (|get.::.1_2838| dws_2878))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|count_`int list`_2888| dws_2878)
                                                            expansions
                                                            • unsat
                                                              (let ((a!1 (>= (ite (>= (|get.::.0_2837| dws_2878) 0)
                                                                                  (|get.::.0_2837| dws_2878)…

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

                                                            In [17]:
                                                            theorem vehicle_stays_within_3_units_of_course dws =
                                                             arbitrary_delta_ws dws
                                                             ==>
                                                             let s' = bad_final_state {y=0;w=0;v=0} dws in
                                                             -3 <= s'.y && s'.y <= 3
                                                            
                                                            Out[17]:
                                                            val vehicle_stays_within_3_units_of_course : Z.t list -> bool = <fun>
                                                            module CX : sig val dws : Z.t list end
                                                            Error: vehicle_stays_within_3_units_of_course is not a theorem.
                                                            
                                                            Counterexample (after 8 steps, 0.034s):
                                                             let dws = [1; 1; 1]
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances8
                                                            definitions12
                                                            inductions0
                                                            search_time
                                                            0.034s
                                                            details
                                                            Expand
                                                            smt_stats
                                                            arith offset eqs55
                                                            num checks17
                                                            arith assert lower293
                                                            arith pivots24
                                                            rlimit count12496
                                                            mk clause428
                                                            datatype occurs check176
                                                            mk bool var514
                                                            arith assert upper218
                                                            datatype splits41
                                                            decisions182
                                                            arith add rows84
                                                            arith bound prop80
                                                            propagations1105
                                                            interface eqs11
                                                            conflicts47
                                                            arith fixed eqs68
                                                            datatype accessor ax38
                                                            minimized lits27
                                                            arith conflicts7
                                                            arith assert diseq162
                                                            datatype constructor ax46
                                                            final checks38
                                                            added eqs713
                                                            del clause103
                                                            arith eq adapter126
                                                            memory22.620000
                                                            max memory52.140000
                                                            num allocs32186401513.000000
                                                            Expand
                                                            • start[0.034s]
                                                                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_2869 (|rec_mk.state_2912| 0 0 0) dws_2906)
                                                                  expansions
                                                                  • sgn
                                                                  • sgnbad_controller
                                                                  • sgnbad_controllerbad_next_state
                                                                • unroll
                                                                  expr
                                                                  (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2908| dws_2906)
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (+ (y_2428 (|rec_mk.state_2912| 0 0 0))
                                                                                  (v_2429 (|rec_mk.state_2912| 0 0 0)…
                                                                    expansions
                                                                    • sgn
                                                                    • sgnbad_controller
                                                                    • sgnbad_controllerbad_next_state
                                                                  • unroll
                                                                    expr
                                                                    (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2908|
                                                                      (|get.::.1_2905| dws_2906))
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (+ (y_2428 (|rec_mk.state_2912| 0 0 0))
                                                                                    (v_2429 (|rec_mk.state_2912| 0 0 0)…
                                                                      expansions
                                                                      • sgn
                                                                      • sgnbad_controller
                                                                      • sgnbad_controllerbad_next_state
                                                                    • unroll
                                                                      expr
                                                                      (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2908|
                                                                        (|get.::.1_2905| (|get.::.1_2905| dws_2906…
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (let ((a!1 (+ (y_2428 (|rec_mk.state_2912| 0 0 0))
                                                                                      (v_2429 (|rec_mk.state_2912| 0 0 0)…
                                                                        expansions
                                                                        • sgn
                                                                        • sgnbad_controller
                                                                        • sgnbad_controllerbad_next_state
                                                                      • unroll
                                                                        expr
                                                                        (|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2908|
                                                                          (|get.::.1_2905| (|get.::.1_2905| (|get.::…
                                                                        expansions
                                                                        • Sat (Some let dws = [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!