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.021s
details
Expand
smt_stats
num checks8
arith assert lower18
arith pivots10
rlimit count2296
mk clause19
datatype occurs check43
mk bool var82
arith assert upper14
datatype splits3
decisions14
arith add rows19
propagations14
conflicts9
arith fixed eqs8
datatype accessor ax5
arith conflicts2
datatype constructor ax8
num allocs852060124
final checks6
added eqs52
del clause8
arith eq adapter12
memory20.490000
max memory20.490000
Expand
  • start[0.021s]
      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`_2345\|| (|\|get.::.1_2321\||…
        expansions
        • unroll
          expr
          (|\|count_`int list`_2345\|| (|\|get.::.1_2321\|| dws_2335))
          expansions
          • unroll
            expr
            (|\|count_`int list`_2345\|| dws_2335)
            expansions
            • unsat
              (let ((a!1 (>= (ite (>= (|\|get.::.0_2320\|| dws_2335) 0)
                                  (|\|get.::.0_2320\|| d…

            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.028s
            details
            Expand
            smt_stats
            arith offset eqs8
            arith assert lower939
            arith pivots38
            rlimit count10365
            mk clause989
            mk bool var332
            restarts1
            arith assert upper942
            decisions263
            arith add rows28
            arith bound prop321
            propagations4062
            conflicts118
            arith fixed eqs40
            datatype accessor ax1
            minimized lits140
            arith conflicts17
            arith assert diseq865
            datatype constructor ax1
            num allocs927934149
            added eqs978
            del clause235
            arith eq adapter336
            memory20.920000
            max memory21.890000
            Expand
            • start[0.028s]
                (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 (not (= (+ (w_2293 s_2381) (v_2295 s_2381)) (- 1))))
                        (a!4 (and (= 1 (+ (w_2293 s_23…

                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 anon_fun.arbitrary_delta_ws.0 dws
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                Verified up to bound 10 (after 0.324s).
                
                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 anon_fun.arbitrary_delta_ws.0 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 anon_fun.arbitrary_delta_ws.0 (List.tl dws)
                     ==> good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 H2. good_state s
                 H3. List.for_all anon_fun.arbitrary_delta_ws.0 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 anon_fun.arbitrary_delta_ws.0 (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 anon_fun.arbitrary_delta_ws.0 (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 anon_fun.arbitrary_delta_ws.0 (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.962s
                Expand
                • start[0.962s, "Goal"]
                    good_state :var_0: && List.for_all anon_fun.arbitrary_delta_ws.0 :var_1:
                    ==> good_state (final_state :var_0: :var_1:)
                • subproof

                  (not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.0 dws)) || good_state (final_state s dws)
                  • start[0.962s, "1"]
                      (not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.0 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 anon_fun.arbitrary_delta_ws.0 dws))
                            || good_state (final_state s dws))
                           && (((not
                                 (not (dws = [])
                                  && ((not (good_state (next_state (List.hd dws) s))
                                       || not
                                          (List.for_all anon_fun.arbitrary_delta_ws.0
                                           (List.tl dws)))
                                      || good_state
                                         (final_state (next_state (List.hd dws) s) (List.tl dws))))
                                 || not (good_state s))
                                || not (List.for_all anon_fun.arbitrary_delta_ws.0 dws))
                               || good_state (final_state s dws))
                           :cases [((not (dws = []) || not (good_state s))
                                    || not (List.for_all anon_fun.arbitrary_delta_ws.0 dws))
                                   || good_state (final_state s dws);
                                   (((dws = []
                                      || not
                                         (not
                                          (good_state (next_state (List.hd dws) s)
                                           && List.for_all anon_fun.arbitrary_delta_ws.0
                                              (List.tl dws))
                                          || good_state
                                             (final_state (next_state (List.hd dws) s)
                                              (List.tl dws))))
                                     || not (good_state s))
                                    || not (List.for_all anon_fun.arbitrary_delta_ws.0 dws))
                                   || good_state (final_state s dws)])
                    • subproof
                      (((dws = [] || not (not (good_state (next_state (List.hd dws) s) && List.for_all anon_fun.arbitrary_delta_ws.0 (List.tl dws)) || good_state (final_state (next_state (List.hd dws) s) (List.tl dws)))) || not (good_state s)) || not (List.for_all anon_fun.arbitrary_delta_ws.0 dws)) || good_state (final_state s dws)
                      • start[0.567s, "1.1"]
                          (((dws = []
                             || not
                                (not
                                 (good_state (next_state (List.hd dws) s)
                                  && List.for_all anon_fun.arbitrary_delta_ws.0 (List.tl dws))
                                 || good_state
                                    (final_state (next_state (List.hd dws) s) (List.tl dws))))
                            || not (good_state s))
                           || not (List.for_all anon_fun.arbitrary_delta_ws.0 dws))
                          || good_state (final_state s dws)
                      • simplify
                        into
                        ((((((((good_state (final_state (next_state (List.hd …) s) (List.tl …))
                                || not (List.for_all anon_fun.arbitrary_delta_ws.0 (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 anon_fun.arbitrary_delta_ws.0 (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 anon_fun.arbitrary_delta_ws.0 (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 anon_fun.arbitrary_delta_ws.0 dws)) || good_state (final_state s dws)
                          • start[0.567s, "1.2"]
                              ((not (dws = []) || not (good_state s))
                               || not (List.for_all anon_fun.arbitrary_delta_ws.0 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.105s
                        details
                        Expand
                        smt_stats
                        rlimit count8404
                        mk bool var5
                        memory40.110000
                        max memory55.180000
                        num allocs8487151024.000000
                        Expand
                        • start[0.105s]
                            List.for_all anon_fun.arbitrary_delta_ws.0 :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 anon_fun.arbitrary_delta_ws.0 :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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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.073s).
                              
                              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 anon_fun.steady_wind.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 anon_fun.steady_wind.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.080s).
                              
                              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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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
                              
                              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 anon_fun.steady_wind.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_instances13
                              definitions52
                              inductions1
                              search_time
                              1.445s
                              details
                              Expand
                              smt_stats
                              arith offset eqs34
                              num checks9
                              arith assert lower624
                              arith pivots75
                              rlimit count294352
                              mk clause830
                              datatype occurs check56
                              mk bool var612
                              arith assert upper605
                              decisions239
                              arith add rows456
                              arith bound prop118
                              propagations2105
                              conflicts79
                              arith fixed eqs59
                              datatype accessor ax11
                              minimized lits152
                              arith conflicts28
                              arith assert diseq467
                              datatype constructor ax6
                              final checks4
                              added eqs1002
                              del clause478
                              arith eq adapter336
                              memory49.310000
                              max memory58.010000
                              num allocs19485484900.000000
                              Expand
                              • start[1.445s, "Goal"]
                                  good_state :var_0:
                                  && List.for_all anon_fun.steady_wind.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 anon_fun.steady_wind.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.445s, "1"]
                                    (((((not (good_state s) || not (List.for_all anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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.719s, "1'''''.1"]
                                                ((((((((dws2 = []
                                                        || not
                                                           (not
                                                            ((((((good_state s && List.hd (List.tl (List.tl dws2)) = 0)
                                                                 && List.for_all anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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 anon_fun.steady_wind.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.719s, "1'''''.2"]
                                                  (((((((not (dws2 = []) || not (good_state s))
                                                        || not (List.hd (List.tl dws2) = 0))
                                                       || not (List.for_all anon_fun.steady_wind.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.130s
                                            details
                                            Expand
                                            smt_stats
                                            rlimit count13318
                                            mk bool var5
                                            memory58.380000
                                            max memory58.570000
                                            num allocs22015862947.000000
                                            Expand
                                            • start[0.130s]
                                                List.for_all anon_fun.steady_wind.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 anon_fun.steady_wind.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.022s
                                                  details
                                                  Expand
                                                  smt_stats
                                                  num checks8
                                                  arith assert lower19
                                                  arith pivots11
                                                  rlimit count15592
                                                  mk clause19
                                                  datatype occurs check43
                                                  mk bool var83
                                                  arith assert upper12
                                                  datatype splits3
                                                  decisions13
                                                  arith add rows17
                                                  arith bound prop1
                                                  propagations13
                                                  conflicts9
                                                  arith fixed eqs8
                                                  datatype accessor ax5
                                                  arith conflicts2
                                                  datatype constructor ax8
                                                  final checks6
                                                  added eqs49
                                                  del clause7
                                                  arith eq adapter11
                                                  memory47.450000
                                                  max memory58.570000
                                                  num allocs22699209757.000000
                                                  Expand
                                                  • start[0.022s]
                                                      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`_2635\|| (|\|get.::.1_2587\||…
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (|\|count_`int list`_2635\|| (|\|get.::.1_2587\|| dws_2625))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|\|count_`int list`_2635\|| dws_2625)
                                                            expansions
                                                            • unsat
                                                              (let ((a!1 (>= (ite (>= (|\|get.::.0_2586\|| dws_2625) 0)
                                                                                  (|\|get.::.0_2586\|| d…

                                                            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.041s):
                                                             let dws = [1; 1; 1]
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances8
                                                            definitions12
                                                            inductions0
                                                            search_time
                                                            0.041s
                                                            details
                                                            Expand
                                                            smt_stats
                                                            arith offset eqs36
                                                            num checks17
                                                            arith assert lower257
                                                            arith pivots29
                                                            rlimit count10281
                                                            mk clause402
                                                            datatype occurs check263
                                                            mk bool var505
                                                            arith assert upper208
                                                            datatype splits41
                                                            decisions194
                                                            arith add rows101
                                                            arith bound prop57
                                                            propagations1009
                                                            interface eqs12
                                                            conflicts44
                                                            arith fixed eqs66
                                                            datatype accessor ax38
                                                            minimized lits30
                                                            arith conflicts4
                                                            arith assert diseq145
                                                            datatype constructor ax46
                                                            final checks39
                                                            added eqs672
                                                            del clause104
                                                            arith eq adapter117
                                                            memory45.060000
                                                            max memory58.570000
                                                            num allocs23081532002.000000
                                                            Expand
                                                            • start[0.041s]
                                                                List.for_all anon_fun.arbitrary_delta_ws.0 :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 anon_fun.arbitrary_delta_ws.0 :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_2616 (|\|rec_mk.state_2650\|| 0 0 0) dws_2644)
                                                                  expansions
                                                                  • sgn
                                                                  • sgnbad_controller
                                                                  • sgnbad_controllerbad_next_state
                                                                • unroll
                                                                  expr
                                                                  (|\|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2646\|| dws_2644)
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (+ (y_2294 (|\|rec_mk.state_2650\|| 0 0 0))
                                                                                  (v_2295 (|\|rec_mk.state_2650\|…
                                                                    expansions
                                                                    • sgn
                                                                    • sgnbad_controller
                                                                    • sgnbad_controllerbad_next_state
                                                                  • unroll
                                                                    expr
                                                                    (|\|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2646\||
                                                                      (|\|get.::.1_2643\|| dws_2644))
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (+ (y_2294 (|\|rec_mk.state_2650\|| 0 0 0))
                                                                                    (v_2295 (|\|rec_mk.state_2650\|…
                                                                      expansions
                                                                      • sgn
                                                                      • sgnbad_controller
                                                                      • sgnbad_controllerbad_next_state
                                                                    • unroll
                                                                      expr
                                                                      (|\|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2646\||
                                                                        (|\|get.::.1_2643\|| (|\|get.::.1_2643…
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (let ((a!1 (+ (y_2294 (|\|rec_mk.state_2650\|| 0 0 0))
                                                                                      (v_2295 (|\|rec_mk.state_2650\|…
                                                                        expansions
                                                                        • sgn
                                                                        • sgnbad_controller
                                                                        • sgnbad_controllerbad_next_state
                                                                      • unroll
                                                                        expr
                                                                        (|\|`List.for_all anon_fun.arbitrary_delta_ws.0[0]`_2646\||
                                                                          (|\|get.::.1_2643\|| (|\|get.::.1_2643…
                                                                        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!