# 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 : Z.t; y : Z.t; v : Z.t; }


# Our controller and state transitions¶

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

Out:
val controller : Z.t -> Z.t -> Z.t = <fun>

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

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

Out:
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 :
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 -> 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
original:final_state s dws
sub:final_state (next_state (List.hd dws) s) (List.tl dws)
original ordinal:Ordinal.Int (_cnt dws)
sub ordinal:Ordinal.Int (_cnt (List.tl dws))
path:[dws <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.016s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 6 arith tableau max columns: 17 arith pivots: 6 rlimit count: 2306 mk clause: 21 datatype occurs check: 12 mk bool var: 69 arith assert upper: 14 datatype splits: 1 decisions: 16 arith row summations: 16 propagations: 22 conflicts: 10 arith fixed eqs: 5 datatype accessor ax: 8 arith conflicts: 2 arith num rows: 6 datatype constructor ax: 9 num allocs: 6.01318e+06 final checks: 4 added eqs: 44 del clause: 14 arith eq adapter: 10 memory: 16.04 max memory: 16.04
Expand
• start[0.016s]
let (_x_0 : int) = count.list mk_nat dws in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : int) = count.list mk_nat _x_1 in
dws <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_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) = count.list mk_nat _x_0 in let (_x_2 : int) = count.list mk_nat dws in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (dws <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_404/server| (|get.::.1_390/server|… expansions:
• unroll
 expr: (|count.list_404/server| (|get.::.1_390/server| dws_392/server)) expansions:
• unroll
 expr: (|count.list_404/server| dws_392/server) 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 -> Z.t -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.026s
details:
Expand
smt_stats:
 arith offset eqs: 16 num checks: 1 arith assert lower: 636 arith tableau max rows: 3 arith tableau max columns: 15 arith pivots: 40 rlimit count: 14585 mk clause: 665 mk bool var: 177 arith assert upper: 703 decisions: 80 arith row summations: 44 arith bound prop: 232 propagations: 3080 conflicts: 67 arith fixed eqs: 37 datatype accessor ax: 1 minimized lits: 88 arith conflicts: 18 arith num rows: 3 arith assert diseq: 535 datatype constructor ax: 1 num allocs: 1.25921e+07 added eqs: 479 del clause: 464 arith eq adapter: 82 time: 0.015 memory: 16.82 max memory: 17.53
Expand
• start[0.026s]
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) || ((0 = _x_4) && _x_10) || (_x_5 && _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 -> Z.t list -> bool = <fun>
Goal:

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

1 nontautological subgoal.

We shall induct according to a scheme derived from final_state.

Induction scheme:

(not (dws <> []) ==> φ dws s)
&& (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 anon_fun.arbitrary_delta_ws.1 dws
|---------------------------------------------------------------------------
C0. dws <> []
C1. 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 anon_fun.arbitrary_delta_ws.1 dws
H2. dws <> []
H3. good_state (next_state (List.hd dws) s)
&& List.for_all anon_fun.arbitrary_delta_ws.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. List.hd dws = 1
H2. good_state s
H3. List.for_all anon_fun.arbitrary_delta_ws.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 anon_fun.arbitrary_delta_ws.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 anon_fun.arbitrary_delta_ws.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.390s
Expand
• start[0.390s, "Goal"]
good_state ( :var_0: )
&& List.for_all anon_fun.arbitrary_delta_ws.1 ( :var_1: )
==> good_state (final_state ( :var_0: ) ( :var_1: ))
• #### subproof

not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws) || good_state (final_state s dws)
• start[0.390s, "1"]
not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws)
|| good_state (final_state s dws)
• induction on (functional final_state)
:scheme (not (dws <> []) ==> φ dws s)
&& (dws <> [] && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s)
• Split (let (_x_0 : bool) = dws <> [] in
let (_x_1 : bool) = good_state (final_state s dws) in
let (_x_2 : bool)
= not
(good_state s && List.for_all anon_fun.arbitrary_delta_ws.1 dws)
in
let (_x_3 : state) = next_state (List.hd dws) s in
let (_x_4 : int list) = List.tl dws in
(_x_0 || _x_1 || _x_2)
&& (_x_1 || _x_2
|| not
(_x_0
&& (good_state (final_state _x_3 _x_4)
|| not
(good_state _x_3
&& List.for_all anon_fun.arbitrary_delta_ws.1 _x_4))))
:cases [not (good_state s)
|| not (List.for_all anon_fun.arbitrary_delta_ws.1 dws)
|| 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 anon_fun.arbitrary_delta_ws.1 dws)
|| not (dws <> [])
|| not
(good_state _x_0
&& List.for_all anon_fun.arbitrary_delta_ws.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 anon_fun.arbitrary_delta_ws.1 dws) || not (dws <> []) || not (good_state _x_0 && List.for_all anon_fun.arbitrary_delta_ws.1 _x_1 ==> good_state (final_state _x_0 _x_1)) || good_state (final_state s dws)
• start[0.389s, "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 anon_fun.arbitrary_delta_ws.1 dws)
|| not (dws <> [])
|| not
(good_state _x_0 && List.for_all anon_fun.arbitrary_delta_ws.1 _x_1
==> good_state (final_state _x_0 _x_1))
|| good_state (final_state s dws)
• ###### simplify
 into: let (_x_0 : bool) = not (dws <> []) in let (_x_1 : int) = List.hd dws in let (_x_2 : state) = next_state _x_1 s in let (_x_3 : int list) = List.tl dws in let (_x_4 : bool) = good_state (final_state _x_2 _x_3) in let (_x_5 : bool) = good_state _x_2 in let (_x_6 : bool) = not (good_state s) in let (_x_7 : bool) = _x_1 = (-1) in let (_x_8 : bool) = _x_1 = 0 in let (_x_9 : bool) = not (List.for_all anon_fun.arbitrary_delta_ws.1 _x_3) in let (_x_10 : bool) = _x_0 || _x_4 || _x_5 || _x_6 in (_x_0 || not (_x_1 = 1) || _x_4 || _x_5 || _x_6 || _x_7 || _x_8 || _x_9) && (_x_10 || _x_7 || not _x_8 || _x_9) && (_x_10 || not _x_7 || _x_9) 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 anon_fun.arbitrary_delta_ws.1 dws) || dws <> [] || good_state (final_state s dws)
• start[0.389s, "2"]
not (good_state s) || not (List.for_all anon_fun.arbitrary_delta_ws.1 dws)
|| 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 : Z.t list -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.040s
details:
Expand
smt_stats:
 rlimit count: 11112 num allocs: 7.2978e+08 time: 0.007 memory: 18 max memory: 18.63
Expand
• start[0.040s]
let (_x_0 : int) = (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y in
List.for_all anon_fun.arbitrary_delta_ws.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 anon_fun.arbitrary_delta_ws.1 ( :var_0: )) || (((-3) <= _x_0) && (_x_0 <= 3)) expansions: [] rewrite_steps: forward_chaining:
• #### simplify

 into: true expansions: [] rewrite_steps: forward_chaining: all_goodall_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 : Z.t 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 -> Z.t list -> bool = <fun>
Goal:

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

1 nontautological subgoal.

We shall induct according to a scheme derived from final_state.

Induction scheme:

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

2 nontautological subgoals.

Subgoal 2:

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

But this is immediate by our hypotheses.

Subgoal 1:

H0. dws <> []
H1. good_state (next_state (List.hd dws) s)
&& (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
H4. dws <> []
H5. (List.tl dws) <> []
H6. (List.tl (List.tl dws)) <> []
H7. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
(final_state s dws).y = 0

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

Subgoal 1':

H0. dws <> []
H1. good_state s
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. (List.tl (List.tl (List.tl dws))) <> []
H6. List.hd 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'':

H0. dws <> []
H1. good_state s
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. (List.tl (List.tl (List.tl dws))) <> []
H5. List.hd (List.tl dws) = 0
H6. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl dws))
H7. List.hd 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''':

H0. dws <> []
H1. good_state s
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. (List.tl (List.tl (List.tl dws))) <> []
H5. List.for_all anon_fun.steady_wind.1 (List.tl (List.tl (List.tl dws)))
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.hd (List.tl dws) = 0
H8. List.hd 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'''':

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

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

Subgoal 1''''':

H0. dws <> []
H1. good_state s
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. (List.tl (List.tl (List.tl dws))) <> []
H5. List.hd (List.tl (List.tl (List.tl dws))) = 0
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.hd (List.tl dws) = 0
H8. List.hd 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'''''':

H0. dws <> []
H1. good_state s
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. (List.tl (List.tl (List.tl dws))) <> []
H5. List.hd (List.tl (List.tl (List.tl dws))) = 0
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.hd (List.tl dws) = 0
H8. List.hd 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'''''' by recursive unrolling.

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


Proved
proof
ground_instances:4
definitions:6
inductions:1
search_time:
1.150s
details:
Expand
smt_stats:
 num checks: 9 arith-assume-eqs: 2 arith-make-feasible: 264 arith-max-columns: 78 arith-conflicts: 12 rlimit count: 142020 arith-cheap-eqs: 348 mk clause: 2094 datatype occurs check: 19 mk bool var: 944 arith-lower: 627 arith-diseq: 906 decisions: 103 arith-propagations: 736 propagations: 2653 interface eqs: 2 arith-bound-propagations-cheap: 736 arith-max-rows: 38 conflicts: 50 datatype accessor ax: 15 minimized lits: 100 arith-bound-propagations-lp: 300 datatype constructor ax: 10 final checks: 6 added eqs: 2365 del clause: 758 arith eq adapter: 264 arith-upper: 691 time: 0.01 memory: 20.25 max memory: 20.25 num allocs: 7.00207e+09
Expand
• start[1.150s, "Goal"]
let (_x_0 : int list) = List.tl ( :var_1: ) in
good_state ( :var_0: )
&& (List.for_all anon_fun.steady_wind.1 ( :var_1: )
&& (if ( :var_1: ) <> []
then
if _x_0 <> []
then if (List.tl _x_0) <> [] then … <> [] else false else false
else false))
==> (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 anon_fun.steady_wind.1 dws) || not (dws <> []) || not (_x_0 <> []) || not (_x_1 <> []) || not ((List.tl _x_1) <> []) || ((final_state s dws).y = 0)
• start[1.150s, "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 anon_fun.steady_wind.1 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 (not (dws <> []) ==> φ dws s)
&& (dws <> [] && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s)
• Split (let (_x_0 : bool) = dws <> [] in
let (_x_1 : bool) = (final_state s dws).y = 0 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 anon_fun.steady_wind.1 dws && _x_0
&& _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_1
|| not
(_x_0
&& (not
(good_state _x_9
&& List.for_all anon_fun.steady_wind.1 _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 : bool) = dws <> [] in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : int list) = List.tl _x_1 in
not (good_state s)
|| not (List.for_all anon_fun.steady_wind.1 dws) || not _x_0
|| not (_x_1 <> []) || not (_x_2 <> [])
|| not ((List.tl _x_2) <> []) || _x_0
|| ((final_state s dws).y = 0);
let (_x_0 : bool) = not (dws <> []) in
let (_x_1 : state) = next_state (List.hd dws) s 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
_x_0
|| not
(good_state _x_1
&& List.for_all anon_fun.steady_wind.1 _x_2 && _x_3
&& _x_5 && _x_7 && (List.tl _x_6) <> []
==> (final_state _x_1 _x_2).y = 0)
|| not (good_state s)
|| not (List.for_all anon_fun.steady_wind.1 dws) || _x_0
|| not _x_3 || not _x_5 || not _x_7
|| ((final_state s dws).y = 0)])
• ##### subproof
let (_x_0 : bool) = not (dws <> []) in let (_x_1 : state) = next_state (List.hd dws) s 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 _x_0 || not (good_state _x_1 && List.for_all anon_fun.steady_wind.1 _x_2 && _x_3 && _x_5 && _x_7 && (List.tl _x_6) <> [] ==> (final_state _x_1 _x_2).y = 0) || not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws) || _x_0 || not _x_3 || not _x_5 || not _x_7 || ((final_state s dws).y = 0)
• start[1.149s, "1"]
let (_x_0 : bool) = not (dws <> []) in
let (_x_1 : state) = next_state (List.hd dws) s 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
_x_0
|| not
(good_state _x_1 && List.for_all anon_fun.steady_wind.1 _x_2 && _x_3
&& _x_5 && _x_7 && (List.tl _x_6) <> []
==> (final_state _x_1 _x_2).y = 0)
|| not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws)
|| _x_0 || not _x_3 || not _x_5 || not _x_7 || ((final_state s dws).y = 0)
• ###### simplify
 into: let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in let (_x_3 : int) = List.hd dws in not (dws <> []) || (List.tl _x_2) <> [] || ((final_state (next_state _x_3 s) _x_0).y = 0) || not (good_state s) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.for_all anon_fun.steady_wind.1 _x_0) || not (_x_3 = 0) expansions: [final_state, List.for_all] rewrite_steps: safety_1 forward_chaining: all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into: let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in let (_x_3 : int) = List.hd dws in not (dws <> []) || (List.tl _x_2) <> [] || ((final_state (next_state _x_3 s) _x_0).y = 0) || not (good_state s) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.hd _x_0 = 0) || not (List.for_all anon_fun.steady_wind.1 _x_1) || not (_x_3 = 0) expansions: List.for_all rewrite_steps: forward_chaining: all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into: let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in let (_x_3 : int) = List.hd dws in not (dws <> []) || (List.tl _x_2) <> [] || ((final_state (next_state _x_3 s) _x_0).y = 0) || not (good_state s) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.for_all anon_fun.steady_wind.1 _x_2) || not (List.hd _x_1 = 0) || not (List.hd _x_0 = 0) || not (_x_3 = 0) expansions: List.for_all rewrite_steps: forward_chaining: all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into: let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in let (_x_3 : int list) = List.tl _x_2 in let (_x_4 : int) = List.hd dws in not (dws <> []) || _x_3 <> [] || ((final_state (next_state _x_4 s) _x_0).y = 0) || not (good_state s) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.hd _x_2 = 0) || not (List.hd _x_1 = 0) || not (List.hd _x_0 = 0) || not (_x_4 = 0) || not (List.for_all anon_fun.steady_wind.1 _x_3) expansions: List.for_all rewrite_steps: forward_chaining: all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into: let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in let (_x_3 : int) = List.hd dws in not (dws <> []) || (List.tl _x_2) <> [] || ((final_state (next_state _x_3 s) _x_0).y = 0) || not (good_state s) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.hd _x_2 = 0) || not (List.hd _x_1 = 0) || not (List.hd _x_0 = 0) || not (_x_3 = 0) expansions: List.for_all rewrite_steps: forward_chaining: all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into: let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in not (dws <> []) || (List.tl _x_2) <> [] || not (good_state s) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.hd _x_2 = 0) || not (List.hd _x_1 = 0) || not (List.hd _x_0 = 0) || not (List.hd dws = 0) || ((final_state (next_state 0 s) _x_0).y = 0) expansions: [] rewrite_steps: forward_chaining:
• ###### subproof
let (_x_0 : int list) = List.tl ( :var_2: ) in let (_x_1 : int list) = List.tl _x_0 in let (_x_2 : int list) = List.tl _x_1 in not (( :var_2: ) <> []) || not (good_state ( :var_3: )) || not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> []) || not (List.hd _x_2 = 0) || not (List.hd _x_1 = 0) || not (List.hd _x_0 = 0) || not (List.hd ( :var_2: ) = 0) || (List.tl _x_2) <> [] || ((final_state (next_state 0 ( :var_3: )) _x_0).y = 0)
Start (let (_x_0 : int list) = List.tl ( :var_2: ) in
let (_x_1 : int list) = List.tl _x_0 in
let (_x_2 : int list) = List.tl _x_1 in
not (( :var_2: ) <> []) || not (good_state ( :var_3: ))
|| not (_x_0 <> []) || not (_x_1 <> []) || not (_x_2 <> [])
|| not (List.hd _x_2 = 0) || not (List.hd _x_1 = 0)
|| not (List.hd _x_0 = 0) || not (List.hd ( :var_2: ) = 0)
|| (List.tl _x_2) <> []
|| ((final_state (next_state 0 ( :var_3: )) _x_0).y = 0) :time 0.029s)
• ##### subproof
let (_x_0 : bool) = dws <> [] in let (_x_1 : int list) = List.tl dws in let (_x_2 : int list) = List.tl _x_1 in not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws) || not _x_0 || not (_x_1 <> []) || not (_x_2 <> []) || not ((List.tl _x_2) <> []) || _x_0 || ((final_state s dws).y = 0)
start[1.151s, "2"]
let (_x_0 : bool) = dws <> [] in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : int list) = List.tl _x_1 in
not (good_state s) || not (List.for_all anon_fun.steady_wind.1 dws)
|| not _x_0 || not (_x_1 <> []) || not (_x_2 <> [])
|| not ((List.tl _x_2) <> []) || _x_0 || ((final_state s dws).y = 0)

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 : Z.t list -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.044s
details:
Expand
smt_stats:
 rlimit count: 13676 time: 0.01 memory: 19.42 max memory: 20.25 num allocs: 7.29042e+09
Expand
• start[0.044s]
let (_x_0 : int list) = List.tl ( :var_0: ) in
&& (if ( :var_0: ) <> []
then
if _x_0 <> [] then if (List.tl _x_0) <> [] then … <> [] else false
else false
else false)
==> (final_state {w = 0; y = 0; v = 0} ( :var_0: )).y = 0
• #### simplify

 into: let (_x_0 : int list) = List.tl ( :var_0: ) in not (List.for_all anon_fun.steady_wind.1 ( :var_0: ) && ( :var_0: ) <> [] && _x_0 <> [] && (List.tl _x_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_goodgood_state_find_and_stay_zt_zeroall_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 : Z.t -> Z.t -> Z.t = <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 : Z.t -> 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 -> 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
original ordinal:Ordinal.Int (_cnt dws)
sub ordinal:Ordinal.Int (_cnt (List.tl dws))
path:[dws <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.012s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 5 arith tableau max columns: 16 arith pivots: 9 rlimit count: 2210 mk clause: 21 datatype occurs check: 12 mk bool var: 75 arith assert upper: 12 datatype splits: 1 decisions: 18 arith row summations: 12 propagations: 24 conflicts: 10 arith fixed eqs: 5 datatype accessor ax: 10 arith conflicts: 2 arith num rows: 5 arith assert diseq: 1 datatype constructor ax: 9 final checks: 4 added eqs: 49 del clause: 11 arith eq adapter: 12 memory: 20.01 max memory: 20.25 num allocs: 7.4227e+09
Expand
• start[0.012s]
let (_x_0 : int) = count.list mk_nat dws in
let (_x_1 : int list) = List.tl dws in
let (_x_2 : int) = count.list mk_nat _x_1 in
dws <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_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) = count.list mk_nat _x_0 in let (_x_2 : int) = count.list mk_nat dws in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (dws <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_2115/server| (|g… expansions:
• unroll
 expr: (|count.list_2115/server| (|get.::.1_2101/server| dws_2103/server)) expansions:
• unroll
 expr: (|count.list_2115/server| dws_2103/server) 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 : Z.t list -> bool = <fun>
module CX : sig val dws : Z.t list end
Error:
validation failed
----------------------------------------------------------------------------
Context: vehicle_stays_within_3_units_of_course is not a theorem.

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!