# 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 :
type state = {
w : int; (* current wind speed *)
y : int; (* y-position of the vehicle *)
v : int; (* accumulated velocity *)
}

Out:
type state = { w : int; y : int; v : int; }


# Our controller and state transitions¶

In :
let controller sgn_y sgn_old_y =
(-3 * sgn_y) + (2 * sgn_old_y)

Out:
val controller : int -> int -> int = <fun>

In :
let sgn x =
if x < 0 then -1
else if x = 0 then 0
else 1

Out:
val sgn : int -> int = <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 :
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:
val next_state : int -> 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 :
let arbitrary_delta_ws = List.for_all (fun x -> x = -1 || x = 0 || x = 1)

Out:
val arbitrary_delta_ws : int 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 :
let rec final_state s dws =
match dws with
| [] -> s
| dw :: dws' ->
let s' = next_state dw s in
final_state s' dws'

Out:
val final_state : state -> int 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.017s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 20 arith-max-columns 18 arith-conflicts 2 rlimit count 2226 mk clause 12 datatype occurs check 22 mk bool var 65 arith-lower 14 arith-diseq 1 datatype splits 3 decisions 18 propagations 13 arith-max-rows 6 conflicts 10 datatype accessor ax 5 datatype constructor ax 8 num allocs 8.54484e+08 final checks 6 added eqs 43 del clause 5 arith eq adapter 10 arith-upper 13 memory 20.3 max memory 20.3
Expand
• start[0.017s]
let (_x_0 : int) = Ordinal.count dws in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : int) = Ordinal.count _x_1 in
not (dws = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : int list) = List.tl dws in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count dws in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (dws = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_int list_2465| dws_2455) expansions
• unroll
 expr (|count_int list_2465| (|get.::.1_2453| dws_2455)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int list_2465| (… expansions
• Unsat

# Verifying our controller¶

We now partition our state-space into a collection of regions, some "good," most "bad," and show that if we start in a "good" state (like (0,0,0)), then we'll (inductively) always end up in a "good" state.

In :
(* 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:
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 :
theorem safety_1 s dw =
good_state s
&& (dw = -1 || dw = 0 || dw = 1)
==>
good_state (next_state dw s)
[@@rewrite]

Out:
val safety_1 : state -> int -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.034s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 226 arith-max-columns 17 arith-conflicts 13 rlimit count 19266 arith-cheap-eqs 32 mk clause 1982 mk bool var 205 arith-lower 856 arith-diseq 1376 decisions 172 arith-propagations 1240 propagations 3776 arith-bound-propagations-cheap 1240 arith-max-rows 8 conflicts 92 datatype accessor ax 1 minimized lits 104 arith-bound-propagations-lp 360 datatype constructor ax 1 num allocs 9.22145e+08 added eqs 835 del clause 147 arith eq adapter 92 arith-upper 778 memory 21.23 max memory 22.14
Expand
• start[0.034s]
let (_x_0 : int) = :var_0:.w in
let (_x_1 : int) = :var_0:.v in
let (_x_2 : int) = _x_0 + _x_1 in
let (_x_3 : bool) = 2 = _x_2 in
let (_x_4 : int) = :var_0:.y in
let (_x_5 : bool) = -2 = _x_4 in
let (_x_6 : bool) = 1 = _x_2 in
let (_x_7 : int) = _x_4 + _x_1 + _x_0 + :var_1: in
let (_x_8 : int)
= _x_0 + :var_1:
+ (_x_1
+ (-3 * (if _x_7 < 0 then -1 else if _x_7 = 0 then 0 else 1)
+ 2 * (if _x_4 < 0 then -1 else if _x_4 = 0 then 0 else 1)))
in
let (_x_9 : bool) = 2 = _x_8 in
let (_x_10 : bool) = -2 = _x_7 in
let (_x_11 : bool) = 1 = _x_8 in
(if _x_6 && -3 = _x_4 then true
else
if _x_6 && _x_5 then true
else
if _x_3 && _x_5 then true else if _x_3 && -1 = _x_4 then true else …)
&& (:var_1: = -1 || :var_1: = 0 || :var_1: = 1)
==> (if _x_11 && -3 = _x_7 then true
else
if _x_11 && _x_10 then true
else
if _x_9 && _x_10 then true
else if _x_9 && -1 = _x_7 then true else …)
• #### simplify

 into let (_x_0 : int) = :var_0:.w in let (_x_1 : int) = :var_0:.v in let (_x_2 : int) = :var_0:.y in let (_x_3 : int) = _x_2 + _x_1 + _x_0 + :var_1: in let (_x_4 : int) = _x_0 + :var_1: + _x_1 + -3 * (if 0 <= _x_3 then if _x_3 = 0 then 0 else 1 else -1) + 2 * (if 0 <= _x_2 then if _x_2 = 0 then 0 else 1 else -1) in let (_x_5 : bool) = 1 = _x_4 in let (_x_6 : bool) = -2 = _x_3 in let (_x_7 : bool) = 2 = _x_4 in let (_x_8 : bool) = -1 = _x_3 in let (_x_9 : bool) = -1 = _x_4 in let (_x_10 : bool) = 0 = _x_3 in let (_x_11 : bool) = -2 = _x_4 in let (_x_12 : bool) = 1 = _x_3 in let (_x_13 : bool) = 2 = _x_3 in let (_x_14 : int) = _x_0 + _x_1 in let (_x_15 : bool) = -1 = _x_14 in let (_x_16 : bool) = -2 = _x_14 in let (_x_17 : bool) = 2 = _x_2 in let (_x_18 : bool) = 1 = _x_2 in let (_x_19 : bool) = 1 = _x_14 in let (_x_20 : bool) = 0 = _x_2 in let (_x_21 : bool) = -1 = _x_2 in let (_x_22 : bool) = 2 = _x_14 in let (_x_23 : bool) = -2 = _x_2 in ((((((((((((_x_5 && -3 = _x_3 || _x_5 && _x_6) || _x_7 && _x_6) || _x_7 && _x_8) || 3 = _x_4 && _x_8) || _x_9 && _x_10) || _x_5 && _x_10) || 0 = _x_4 && _x_10) || _x_11 && _x_12) || -3 = _x_4 && _x_12) || _x_9 && _x_13) || _x_11 && _x_13) || _x_9 && 3 = _x_3) || not (((((((((((((_x_15 && 3 = _x_2 || _x_16 && _x_17) || _x_15 && _x_17) || -3 = _x_14 && _x_18) || _x_16 && _x_18) || _x_19 && _x_20) || 0 = _x_14 && _x_20) || _x_15 && _x_20) || 3 = _x_14 && _x_21) || _x_22 && _x_21) || _x_22 && _x_23) || _x_19 && _x_23) || _x_19 && -3 = _x_2) && ((:var_1: = -1 || :var_1: = 0) || :var_1: = 1)) expansions [] rewrite_steps forward_chaining
• Unsat

#### Warning

Pattern will match only if good_state is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

#### Warning

Pattern will match only if next_state is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

## Theorem: Multistep safety¶

We prove: If we start in a good state and simulate the controller w.r.t. an arbitrary sequence of sensor readings, then we still end up in a good state.

In :
#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:
val all_good : state -> int list -> bool = <fun>
Goal:

good_state s && arbitrary_delta_ws dws ==> good_state (final_state s dws).

1 nontautological subgoal.

We shall induct according to a scheme derived from final_state.

Induction scheme:

(dws = [] ==> φ dws s)
&& (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s).

2 nontautological subgoals.

Subgoal 2:

H0. good_state s
H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
H2. 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:

H0. good_state s
H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
H2. not (dws = [])
H3. good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
==> good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
|---------------------------------------------------------------------------
good_state (final_state s dws)

This simplifies, using the definitions of List.for_all and final_state to the
following 3 subgoals:

Subgoal 1.3:

H0. dws <> []
H1. good_state s
H2. List.hd dws = 1
H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
|---------------------------------------------------------------------------
C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
C1. good_state (next_state (List.hd dws) s)
C2. List.hd dws = -1
C3. List.hd dws = 0

But simplification reduces this to true, using the rewrite rule safety_1.

Subgoal 1.2:

H0. dws <> []
H1. good_state s
H2. List.hd dws = 0
H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
|---------------------------------------------------------------------------
C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
C1. good_state (next_state (List.hd dws) s)
C2. List.hd dws = -1

But simplification reduces this to true, using the rewrite rule safety_1.

Subgoal 1.1:

H0. dws <> []
H1. good_state s
H2. List.hd dws = -1
H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
|---------------------------------------------------------------------------
C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
C1. good_state (next_state (List.hd dws) s)

But simplification reduces this to true, using the rewrite rule safety_1.

ⓘ  Rules:
(:def List.for_all)
(:def final_state)
(:rw safety_1)
(:induct final_state)


Proved
proof
 ground_instances 0 definitions 11 inductions 1 search_time 0.493s
Expand
• start[0.493s, "Goal"]
good_state :var_0:
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_1:
==> good_state (final_state :var_0: :var_1:)
• #### subproof

(not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || good_state (final_state s dws)
• start[0.493s, "1"]
(not (good_state s)
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws)
• induction on (functional final_state)
:scheme (dws = [] ==> φ dws s)
&& (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s)
• Split (let (_x_0 : bool)
= good_state (final_state s dws)
|| not
(good_state s
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)
in
let (_x_1 : bool) = not (dws = []) in
let (_x_2 : state) = next_state (List.hd dws) s in
let (_x_3 : int list) = List.tl dws in
(_x_0 || _x_1)
&& (_x_0
|| not
(_x_1
&& (good_state (final_state _x_2 _x_3)
|| not
(good_state _x_2
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1)
_x_3))))
:cases [((not (good_state s)
|| not
(List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| not (dws = []))
|| good_state (final_state s dws);
let (_x_0 : state) = next_state (List.hd dws) s in
let (_x_1 : int list) = List.tl dws in
(((not (good_state s)
|| not
(List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| dws = [])
|| not
(good_state _x_0
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1
==> good_state (final_state _x_0 _x_1)))
|| good_state (final_state s dws)])
• ##### subproof
let (_x_0 : state) = next_state (List.hd dws) s in let (_x_1 : int list) = List.tl dws in (((not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || dws = []) || not (good_state _x_0 && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1 ==> good_state (final_state _x_0 _x_1))) || good_state (final_state s dws)
• start[0.493s, "1"]
let (_x_0 : state) = next_state (List.hd dws) s in
let (_x_1 : int list) = List.tl dws in
(((not (good_state s)
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| dws = [])
|| not
(good_state _x_0
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1
==> good_state (final_state _x_0 _x_1)))
|| good_state (final_state s dws)
• ###### simplify
 into let (_x_0 : int) = List.hd dws in let (_x_1 : state) = next_state _x_0 s in let (_x_2 : int list) = List.tl dws in let (_x_3 : bool) = ((dws = [] || good_state (final_state _x_1 _x_2)) || good_state _x_1) || not (good_state s) in let (_x_4 : bool) = _x_0 = -1 in let (_x_5 : bool) = _x_3 || _x_4 in let (_x_6 : bool) = _x_0 = 0 in let (_x_7 : bool) = not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_2) in ((((_x_5 || _x_6) || not (_x_0 = 1)) || _x_7) && ((_x_5 || not _x_6) || _x_7)) && ((_x_3 || not _x_4) || _x_7) expansions [final_state, final_state, final_state, List.for_all, List.for_all, final_state, final_state, final_state, List.for_all] rewrite_steps forward_chaining
• Subproof
• Subproof
• Subproof
• ##### subproof
((not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || not (dws = [])) || good_state (final_state s dws)
• start[0.493s, "2"]
((not (good_state s)
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| not (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 :
#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:
val vehicle_stays_within_3_units_of_course : int list -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.041s
details
Expand
smt_stats
 rlimit count 8857 mk bool var 1 num allocs 3.30592e+09 memory 21.11 max memory 49.41
Expand
• start[0.041s]
let (_x_0 : int) = (final_state {w = 0; y = 0; v = 0} :var_0:).y in
List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
==> -3 <= _x_0 && _x_0 <= 3
• #### simplify

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

 into true expansions [] rewrite_steps forward_chaining all_good
• Unsat

# Theorem: If wind is stable for 4 intervals, we get back on course.¶

We prove: If the wind ever becomes constant for at least 4 sampling intervals, then the vehicle returns to the x-axis and stays there as long as the wind remains constant.

In :
let steady_wind = List.for_all (fun x -> x = 0)

let at_least_4 xs = match xs with
_ :: _ :: _ :: _ :: _ -> true
| _ -> false

Out:
val steady_wind : int list -> bool = <fun>
val at_least_4 : 'a list -> bool = <fun>

In :
#disable next_state;;
#disable good_state;;
#max_induct 4;;

theorem good_state_find_and_stay_zt_zero s dws =
good_state s
&& at_least_4 dws
==>
let s' = (final_state s dws) [@trigger] in
s'.y = 0
[@@induct functional final_state]
[@@forward_chaining]
;;

Out:
val good_state_find_and_stay_zt_zero : state -> int list -> bool = <fun>
Goal:

good_state s && steady_wind dws && at_least_4 dws
==> let (s' : state) = final_state s dws in s'.y = 0.

1 nontautological subgoal.

We shall induct according to a scheme derived from final_state.

Induction scheme:

(dws = [] ==> φ dws s)
&& (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s).

2 nontautological subgoals.

Subgoal 2:

H0. dws = []
H1. good_state s
H2. List.for_all (fun x -> x = 0) dws
H3. dws <> []
H4. (List.tl dws) <> []
H5. (List.tl (List.tl dws)) <> []
H6. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
(final_state s dws).y = 0

But simplification reduces this to true.

Subgoal 1:

H0. not (dws = [])
H1. ((((good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = 0) (List.tl dws))
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> [])
&& (List.tl (List.tl (List.tl (List.tl dws)))) <> []
==> (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
H2. good_state s
H3. List.for_all (fun x -> x = 0) dws
H4. dws <> []
H5. (List.tl dws) <> []
H6. (List.tl (List.tl dws)) <> []
H7. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
(final_state s dws).y = 0

This simplifies, using the definitions of List.for_all and final_state to the
following 4 subgoals:

Subgoal 1.4:

H0. dws <> []
H1. good_state s
H2. (List.tl (List.tl (List.tl dws))) <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. List.hd dws = 0
H6. List.for_all (fun x -> x = 0) (List.tl dws)
|---------------------------------------------------------------------------
C0. good_state (next_state (List.hd dws) s)
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

But simplification reduces this to true, using the definition of
List.for_all, and the rewrite rule safety_1.

Subgoal 1.3:

H0. dws <> []
H1. good_state s
H2. (List.tl (List.tl (List.tl dws))) <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. good_state (next_state (List.hd dws) s)
H6. List.hd dws = 0
H7. List.for_all (fun x -> x = 0) (List.tl dws)
|---------------------------------------------------------------------------
C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
C1. List.hd (List.tl dws) = 0

But simplification reduces this to true, using the definition of
List.for_all.

Subgoal 1.2:

H0. dws <> []
H1. good_state s
H2. (List.tl (List.tl (List.tl dws))) <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. good_state (next_state (List.hd dws) s)
H6. List.hd (List.tl dws) = 0
H7. List.hd dws = 0
H8. List.for_all (fun x -> x = 0) (List.tl dws)
|---------------------------------------------------------------------------
C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
C1. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))

But simplification reduces this to true, using the definition of
List.for_all.

Subgoal 1.1:

H0. dws <> []
H1. good_state s
H2. (List.tl (List.tl (List.tl dws))) <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. good_state (next_state (List.hd dws) s)
H6. List.hd (List.tl dws) = 0
H7. List.hd dws = 0
H8. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
H9. List.for_all (fun x -> x = 0) (List.tl dws)
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all, and the rewrite rule
safety_1 to:

Subgoal 1.1':

H0. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
H1. good_state s
H2. (List.tl (List.tl (List.tl dws))) <> []
H3. dws <> []
H4. (List.tl dws) <> []
H5. (List.tl (List.tl dws)) <> []
H6. List.hd (List.tl dws) = 0
H7. List.hd dws = 0
H8. List.hd (List.tl (List.tl dws)) = 0
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all to:

Subgoal 1.1'':

H0. good_state s
H1. (List.tl (List.tl (List.tl dws))) <> []
H2. dws <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. List.hd (List.tl dws) = 0
H6. List.hd dws = 0
H7. List.hd (List.tl (List.tl dws)) = 0
H8. List.for_all (fun x -> x = 0)
(List.tl (List.tl (List.tl (List.tl dws))))
H9. List.hd (List.tl (List.tl (List.tl dws))) = 0
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all to:

Subgoal 1.1''':

H0. good_state s
H1. (List.tl (List.tl (List.tl dws))) <> []
H2. dws <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. List.hd (List.tl dws) = 0
H6. List.hd dws = 0
H7. List.hd (List.tl (List.tl dws)) = 0
H8. List.hd (List.tl (List.tl (List.tl dws))) = 0
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This further simplifies to:

Subgoal 1.1'''':

H0. good_state s
H1. (List.tl (List.tl (List.tl dws))) <> []
H2. dws <> []
H3. (List.tl dws) <> []
H4. (List.tl (List.tl dws)) <> []
H5. List.hd (List.tl dws) = 0
H6. List.hd dws = 0
H7. List.hd (List.tl (List.tl dws)) = 0
H8. List.hd (List.tl (List.tl (List.tl dws))) = 0
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state 0 s) (List.tl dws)).y = 0

But we verify Subgoal 1.1'''' by recursive unrolling.

ⓘ  Rules:
(:def List.for_all)
(:def final_state)
(:rw safety_1)
(:fc all_good)
(:induct final_state)


Proved
proof
ground_instances4
definitions18
inductions1
search_time
1.901s
details
Expand
smt_stats
 num checks 9 arith-assume-eqs 7 arith-make-feasible 342 arith-max-columns 73 arith-conflicts 23 rlimit count 217680 arith-cheap-eqs 337 mk clause 2735 datatype occurs check 61 mk bool var 1142 arith-lower 812 arith-diseq 1362 decisions 210 arith-propagations 1012 propagations 4146 interface eqs 7 arith-bound-propagations-cheap 1012 arith-max-rows 42 conflicts 78 datatype accessor ax 16 minimized lits 193 arith-bound-propagations-lp 346 datatype constructor ax 10 final checks 11 added eqs 3511 del clause 1097 arith eq adapter 347 arith-upper 1074 memory 60.6 max memory 68.1 num allocs 1.89963e+10
Expand
• start[1.901s, "Goal"]
let (_x_0 : int list) = List.tl :var_1: in
let (_x_1 : int list) = List.tl _x_0 in
good_state :var_0:
&& List.for_all (fun x -> x = 0) :var_1:
&& :var_1: <> [] && _x_0 <> [] && _x_1 <> [] && (List.tl _x_1) <> []
==> (final_state :var_0: :var_1:).y = 0
• #### subproof

let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not (_x_0 <> [])) || not (_x_1 <> [])) || not ((List.tl _x_1) <> [])) || (final_state s dws).y = 0
• start[1.901s, "1"]
let (_x_0 : int list) = List.tl dws in
let (_x_1 : int list) = List.tl _x_0 in
(((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not (_x_0 <> []))
|| not (_x_1 <> []))
|| not ((List.tl _x_1) <> []))
|| (final_state s dws).y = 0
• induction on (functional final_state)
:scheme (dws = [] ==> φ dws s)
&& (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s)
• Split (let (_x_0 : bool) = (final_state s dws).y = 0 in
let (_x_1 : bool) = not (dws = []) in
let (_x_2 : int list) = List.tl dws in
let (_x_3 : bool) = _x_2 <> [] in
let (_x_4 : int list) = List.tl _x_2 in
let (_x_5 : bool) = _x_4 <> [] in
let (_x_6 : int list) = List.tl _x_4 in
let (_x_7 : bool) = _x_6 <> [] in
let (_x_8 : bool)
= not
(((((good_state s && List.for_all (fun x -> x = 0) dws)
&& dws <> [])
&& _x_3)
&& _x_5)
&& _x_7)
in
let (_x_9 : state) = next_state (List.hd dws) s in
((_x_0 || _x_1) || _x_8)
&& ((_x_0
|| not
(_x_1
&& (not
(((((good_state _x_9
&& List.for_all (fun x -> x = 0) _x_2)
&& _x_3)
&& _x_5)
&& _x_7)
&& (List.tl _x_6) <> [])
|| (final_state _x_9 _x_2).y = 0)))
|| _x_8)
:cases [let (_x_0 : int list) = List.tl dws in
let (_x_1 : int list) = List.tl _x_0 in
((((((not (dws = []) || not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not (_x_0 <> []))
|| not (_x_1 <> []))
|| not ((List.tl _x_1) <> []))
|| (final_state s dws).y = 0;
let (_x_0 : state) = next_state (List.hd dws) s in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : bool) = _x_1 <> [] in
let (_x_3 : int list) = List.tl _x_1 in
let (_x_4 : bool) = _x_3 <> [] in
let (_x_5 : int list) = List.tl _x_3 in
let (_x_6 : bool) = _x_5 <> [] in
(((((((dws = []
|| not
(((((good_state _x_0
&& List.for_all (fun x -> x = 0) _x_1)
&& _x_2)
&& _x_4)
&& _x_6)
&& (List.tl _x_5) <> []
==> (final_state _x_0 _x_1).y = 0))
|| not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not _x_2)
|| not _x_4)
|| not _x_6)
|| (final_state s dws).y = 0])
• ##### subproof
let (_x_0 : state) = next_state (List.hd dws) s in let (_x_1 : int list) = List.tl dws in let (_x_2 : bool) = _x_1 <> [] in let (_x_3 : int list) = List.tl _x_1 in let (_x_4 : bool) = _x_3 <> [] in let (_x_5 : int list) = List.tl _x_3 in let (_x_6 : bool) = _x_5 <> [] in (((((((dws = [] || not (((((good_state _x_0 && List.for_all (fun x -> x = 0) _x_1) && _x_2) && _x_4) && _x_6) && (List.tl _x_5) <> [] ==> (final_state _x_0 _x_1).y = 0)) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not _x_2) || not _x_4) || not _x_6) || (final_state s dws).y = 0
• start[1.899s, "1"]
let (_x_0 : state) = next_state (List.hd dws) s in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : bool) = _x_1 <> [] in
let (_x_3 : int list) = List.tl _x_1 in
let (_x_4 : bool) = _x_3 <> [] in
let (_x_5 : int list) = List.tl _x_3 in
let (_x_6 : bool) = _x_5 <> [] in
(((((((dws = []
|| not
(((((good_state _x_0 && List.for_all (fun x -> x = 0) _x_1)
&& _x_2)
&& _x_4)
&& _x_6)
&& (List.tl _x_5) <> [] ==> (final_state _x_0 _x_1).y = 0))
|| not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not _x_2)
|| not _x_4)
|| not _x_6)
|| (final_state s dws).y = 0
• ###### simplify
 into let (_x_0 : bool) = dws = [] in let (_x_1 : int) = List.hd dws in let (_x_2 : state) = next_state _x_1 s in let (_x_3 : bool) = good_state _x_2 in let (_x_4 : int list) = List.tl dws in let (_x_5 : bool) = (final_state _x_2 _x_4).y = 0 in let (_x_6 : bool) = not (good_state s) in let (_x_7 : int list) = List.tl _x_4 in let (_x_8 : int list) = List.tl _x_7 in let (_x_9 : bool) = not (_x_8 <> []) in let (_x_10 : bool) = not (_x_4 <> []) in let (_x_11 : bool) = not (_x_7 <> []) in let (_x_12 : bool) = not (_x_1 = 0) in let (_x_13 : bool) = not (List.for_all (fun x -> x = 0) _x_4) in let (_x_14 : bool) = not _x_3 in let (_x_15 : bool) = (((((_x_0 || _x_5) || _x_6) || _x_9) || _x_10) || _x_11) || _x_14 in let (_x_16 : bool) = List.hd _x_4 = 0 in let (_x_17 : bool) = not _x_16 in let (_x_18 : bool) = List.for_all (fun x -> x = 0) _x_7 in ((((((((((_x_0 || _x_3) || _x_5) || _x_6) || _x_9) || _x_10) || _x_11) || _x_12) || _x_13) && (((_x_15 || _x_12) || _x_16) || _x_13)) && ((((_x_15 || _x_17) || _x_12) || _x_18) || _x_13)) && (((((((((((_x_0 || (List.tl _x_8) <> []) || _x_5) || _x_6) || _x_9) || _x_10) || _x_11) || _x_14) || _x_17) || _x_12) || not _x_18) || _x_13) expansions [final_state, List.for_all, final_state, List.for_all, final_state, List.for_all, final_state, List.for_all, final_state, List.for_all, List.for_all] rewrite_steps forward_chaining all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• Subproof
• Subproof
• Subproof
• Subproof
• ##### subproof
let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in ((((((not (dws = []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not (_x_0 <> [])) || not (_x_1 <> [])) || not ((List.tl _x_1) <> [])) || (final_state s dws).y = 0
• start[1.899s, "2"]
let (_x_0 : int list) = List.tl dws in
let (_x_1 : int list) = List.tl _x_0 in
((((((not (dws = []) || not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not (_x_0 <> []))
|| not (_x_1 <> []))
|| not ((List.tl _x_1) <> []))
|| (final_state s dws).y = 0
• ###### simplify
 into true expansions [] rewrite_steps forward_chaining

You may enjoy reading the above proof! Now, we prove the final part of our main safety theorem.

In :
#enable good_state;;

theorem good_state_find_and_stay_0_from_origin dws =
&& at_least_4 dws
==>
let s' = final_state {y=0;w=0;v=0} dws in
s'.y = 0
[@@simp]

Out:
val good_state_find_and_stay_0_from_origin : int list -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.048s
details
Expand
smt_stats
 rlimit count 16175 mk bool var 1 memory 42.44 max memory 68.1 num allocs 2.01406e+10
Expand
• start[0.048s]
let (_x_0 : int list) = List.tl :var_0: in
let (_x_1 : int list) = List.tl _x_0 in
List.for_all (fun x -> x = 0) :var_0:
&& :var_0: <> [] && _x_0 <> [] && _x_1 <> [] && (List.tl _x_1) <> []
==> (final_state {w = 0; y = 0; v = 0} :var_0:).y = 0
• #### simplify

 into let (_x_0 : int list) = List.tl :var_0: in let (_x_1 : int list) = List.tl _x_0 in not ((((List.for_all (fun x -> x = 0) :var_0: && :var_0: <> []) && _x_0 <> []) && _x_1 <> []) && (List.tl _x_1) <> []) || (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_goodgood_state_find_and_stay_zt_zero
• Unsat

# Experiments with a flawed version¶

Now that we've verified the controller, let us imagine instead that we'd made a mistake in its design and use Imandra to find such a mistake. For example, what if we'd defined the controller as follows?

In :
let bad_controller sgn_y sgn_old_y =
(-4 * sgn_y) + (2 * sgn_old_y)

Out:
val bad_controller : int -> int -> int = <fun>

In :
let bad_next_state dw s =
{ w = s.w + dw;
y = s.y + s.v + s.w + dw;
v = s.v +
(sgn (s.y + s.v + s.w + dw))
(sgn s.y)
}

Out:
val bad_next_state : int -> state -> state = <fun>

In :
let rec bad_final_state s dws =
match dws with
| [] -> s
| dw :: dws' ->
let s' = bad_next_state dw s in

Out:
val bad_final_state : state -> int list -> state = <fun>

termination proof

### Termination proof

call bad_final_state (bad_next_state (List.hd dws) s) (List.tl dws) from bad_final_state s dws
original 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.013s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 20 arith-max-columns 18 arith-conflicts 2 rlimit count 2226 mk clause 12 datatype occurs check 22 mk bool var 65 arith-lower 14 arith-diseq 1 datatype splits 3 decisions 18 propagations 13 arith-max-rows 6 conflicts 10 datatype accessor ax 5 datatype constructor ax 8 final checks 6 added eqs 43 del clause 5 arith eq adapter 10 arith-upper 13 memory 39.92 max memory 68.1 num allocs 2.04781e+10
Expand
• start[0.013s]
let (_x_0 : int) = Ordinal.count dws in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : int) = Ordinal.count _x_1 in
not (dws = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : int list) = List.tl dws in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count dws in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (dws = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_int list_4715| dws_4705) expansions
• unroll
 expr (|count_int list_4715| (|get.::.1_4703| dws_4705)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int list_4715| (… expansions
• Unsat

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

In :
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:
val vehicle_stays_within_3_units_of_course : int list -> bool = <fun>
module CX : sig val dws : int list end
Error: vehicle_stays_within_3_units_of_course is not a theorem.

Counterexample (after 8 steps, 0.032s):
let (dws : int list) = [1; 1; 1]

Refuted
proof attempt
ground_instances8
definitions0
inductions0
search_time
0.032s
details
Expand
smt_stats
 num checks 17 arith-assume-eqs 12 arith-make-feasible 227 arith-max-columns 61 arith-conflicts 3 rlimit count 17439 arith-cheap-eqs 200 mk clause 1041 datatype occurs check 183 mk bool var 730 arith-lower 307 arith-diseq 521 datatype splits 41 decisions 176 arith-propagations 421 propagations 1707 interface eqs 12 arith-bound-propagations-cheap 421 arith-max-rows 32 conflicts 53 datatype accessor ax 41 minimized lits 23 arith-bound-propagations-lp 139 datatype constructor ax 49 final checks 39 added eqs 1244 del clause 178 arith eq adapter 198 arith-upper 535 memory 41.3 max memory 68.1 num allocs 2.07177e+10
Expand
• start[0.032s]
let (_x_0 : int) = (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y in
List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
==> -3 <= _x_0 && _x_0 <= 3
• #### simplify

 into let (_x_0 : int) = (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y in not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:) || -3 <= _x_0 && _x_0 <= 3 expansions [] rewrite_steps forward_chaining
• unroll
 expr (bad_final_state_94 (|rec_mk.state_4754| 0 0 0) dws_4748) expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4750| dws_4748) expansions
• unroll
 expr (bad_final_state_94 (bad_next_state_91 (|get.::.0_4746| dws_4748) (|rec_mk.state_4754| 0 0 0)) (… expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4750| (|get.::.1_4747| dws_4748)) expansions
• unroll
 expr (bad_final_state_94 (bad_next_state_91 (|get.::.0_4746| (|get.::.1_4747| dws_4748)) (bad_n… expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4750| (|get.::.1_4747| (|get.::.1_4747| dws_4748… expansions
• unroll
 expr (let ((a!1 (bad_next_state_91 (|get.::.0_4746| (|get.::.1_4747| (|get.::.1_4747| dws_47… expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4750| (|get.::.1_4747| (|get.::.1_4747| (|get.::… expansions
• Sat (Some let (dws : int list) = [1; 1; 1] )

Imandra shows us that with our flawed controller, this conjecture is not true! In fact, Imandra computes a counterexample consisting of a sequence of three 1-valued wind speed sensor readings.

If we plug these in, we can see the counterexample in action:

In :
bad_final_state {y=0; w=0; v=0} [1;1;1]

Out:
- : state = {w = 3; y = 4; v = -4}


Happy verifying!