# 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 (_cnt dws)
sub ordinalOrdinal.Int (_cnt (List.tl dws))
path[not Is_a([], dws)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 18 arith-max-columns 16 arith-conflicts 2 rlimit count 2024 mk clause 20 datatype occurs check 12 mk bool var 56 arith-lower 15 arith-diseq 1 datatype splits 1 decisions 15 propagations 14 arith-max-rows 4 conflicts 7 datatype accessor ax 7 datatype constructor ax 5 num allocs 864623 final checks 4 added eqs 38 del clause 13 arith eq adapter 10 arith-upper 12 memory 5.9 max memory 5.9
Expand
• start[0.017s]
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
not Is_a([], dws) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], dws) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list mk_nat_1712| dws_1700) expansions
• unroll
 expr (|count.list mk_nat_1712| (|get.::.1_1698| dws_1700)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list mk_nat_1712| (|get.::.1_1… 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.065s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 240 arith-max-columns 17 arith-conflicts 14 rlimit count 20291 arith-cheap-eqs 100 mk clause 2217 mk bool var 209 arith-lower 951 arith-diseq 1559 decisions 156 arith-propagations 1365 propagations 4123 arith-bound-propagations-cheap 1365 arith-max-rows 3 conflicts 96 datatype accessor ax 1 minimized lits 109 arith-bound-propagations-lp 386 datatype constructor ax 1 num allocs 4.7828e+06 added eqs 927 del clause 322 arith eq adapter 99 arith-upper 892 time 0.048 memory 6.93 max memory 7.88
Expand
• start[0.065s]
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:

(Is_a([], dws) ==> φ dws s)
&& (not Is_a([], 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. Is_a([], 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 Is_a([], 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. good_state s
H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
H2. List.hd dws = 1
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
C2. good_state (next_state (List.hd dws) s)
C3. List.hd dws = -1
C4. List.hd dws = 0

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

Subgoal 1.2:

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

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

Subgoal 1.1:

H0. good_state s
H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
H2. List.hd dws = -1
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
C2. 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.696s
Expand
• start[0.696s, "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.696s, "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 (Is_a([], dws) ==> φ dws s)
&& (not Is_a([], 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 Is_a([], 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 Is_a([], 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))
|| Is_a([], 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)) || Is_a([], 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.695s, "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))
|| Is_a([], 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) = (((Is_a([], dws) || good_state (final_state _x_1 _x_2)) || good_state _x_1) || not (good_state s)) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_2) 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 (((_x_5 || _x_6) || not (_x_0 = 1)) && (_x_5 || not _x_6)) && (_x_3 || not _x_4) 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 Is_a([], dws)) || good_state (final_state s dws)
• start[0.695s, "2"]
((not (good_state s)
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| not Is_a([], 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.038s
details
Expand
smt_stats
 rlimit count 8556 num allocs 7.40399e+08 time 0.008 memory 19.77 max memory 37.26
Expand
• start[0.038s]
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:

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

2 nontautological subgoals.

Subgoal 2:

H0. Is_a([], 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, using the forward-chaining rule
all_good.

Subgoal 1:

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

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

Subgoal 1.2:

H0. good_state s
H1. (List.tl (List.tl (List.tl dws))) <> []
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. good_state (next_state (List.hd dws) s)
H5. List.hd (List.tl dws) = 0
H6. List.hd dws = 0
H7. List.for_all (fun x -> x = 0) (List.tl dws)
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
C2. 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. good_state s
H1. (List.tl (List.tl (List.tl dws))) <> []
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. good_state (next_state (List.hd dws) s)
H5. List.hd (List.tl dws) = 0
H6. List.hd dws = 0
H7. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
H8. List.for_all (fun x -> x = 0) (List.tl dws)
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C2. (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. good_state s
H1. (List.tl (List.tl (List.tl dws))) <> []
H2. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C2. (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. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.hd (List.tl (List.tl (List.tl dws))) = 0
H8. List.for_all (fun x -> x = 0)
(List.tl (List.tl (List.tl (List.tl dws))))
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C2. (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. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.hd (List.tl (List.tl (List.tl dws))) = 0
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C2. (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. (List.tl dws) <> []
H3. (List.tl (List.tl dws)) <> []
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. List.hd (List.tl (List.tl dws)) = 0
H7. List.hd (List.tl (List.tl (List.tl dws))) = 0
|---------------------------------------------------------------------------
C0. Is_a([], dws)
C1. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C2. (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.970s
details
Expand
smt_stats
 num checks 9 arith-assume-eqs 8 arith-make-feasible 338 arith-max-columns 72 arith-conflicts 10 rlimit count 221574 arith-gcd-calls 1 arith-cheap-eqs 383 mk clause 2539 datatype occurs check 86 mk bool var 1164 arith-lower 747 arith-diseq 1132 decisions 260 arith-propagations 978 arith-patches-success 1 propagations 3819 arith-patches 1 interface eqs 8 arith-bound-propagations-cheap 978 arith-max-rows 36 conflicts 65 datatype accessor ax 16 minimized lits 298 arith-bound-propagations-lp 225 datatype constructor ax 27 final checks 12 added eqs 3430 del clause 1029 arith eq adapter 381 arith-upper 967 time 0.03 memory 48.08 max memory 68.47 num allocs 1.29398e+10
Expand
• start[1.970s, "Goal"]
let (_x_0 : int list) = List.tl ( :var_1: ) in
good_state ( :var_0: )
&& List.for_all (fun x -> x = 0) ( :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 (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.970s, "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 (Is_a([], dws) ==> φ dws s)
&& (not Is_a([], 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 Is_a([], 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 Is_a([], 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
(((((((Is_a([], 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 (((((((Is_a([], 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.969s, "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
(((((((Is_a([], 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) = Is_a([], 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_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 Is_a([], 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.969s, "2"]
let (_x_0 : int list) = List.tl dws in
let (_x_1 : int list) = List.tl _x_0 in
((((((not Is_a([], 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 all_goodall_goodall_good

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.080s
details
Expand
smt_stats
 rlimit count 15174 time 0.016 memory 50.48 max memory 68.47 num allocs 1.32433e+10
Expand
• start[0.080s]
let (_x_0 : int list) = List.tl ( :var_0: ) in
List.for_all (fun x -> x = 0) ( :var_0: )
&& (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 (fun x -> x = 0) ( :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_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 (_cnt dws)
sub ordinalOrdinal.Int (_cnt (List.tl dws))
path[not Is_a([], dws)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 18 arith-max-columns 16 arith-conflicts 2 rlimit count 2024 mk clause 20 datatype occurs check 12 mk bool var 56 arith-lower 15 arith-diseq 1 datatype splits 1 decisions 15 propagations 14 arith-max-rows 4 conflicts 7 datatype accessor ax 7 datatype constructor ax 5 final checks 4 added eqs 38 del clause 13 arith eq adapter 10 arith-upper 12 memory 50.24 max memory 68.47 num allocs 1.34384e+10
Expand
• start[0.013s]
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
not Is_a([], dws) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], dws) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list mk_nat_4014| dws_4002) expansions
• unroll
 expr (|count.list mk_nat_4014| (|get.::.1_4000| dws_4002)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list mk_nat_4014| (|get.::.1_4… 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.027s):
let (dws : int list) = [1; 1; 1]

Refuted
proof attempt
ground_instances8
definitions0
inductions0
search_time
0.027s
details
Expand
smt_stats
 num checks 17 arith-assume-eqs 10 arith-make-feasible 196 arith-max-columns 65 arith-conflicts 3 rlimit count 15724 arith-cheap-eqs 206 mk clause 961 datatype occurs check 101 mk bool var 724 arith-lower 280 arith-diseq 457 datatype splits 7 decisions 148 arith-propagations 355 propagations 1357 interface eqs 10 arith-bound-propagations-cheap 355 arith-max-rows 35 conflicts 46 datatype accessor ax 71 minimized lits 32 arith-bound-propagations-lp 163 datatype constructor ax 73 final checks 26 added eqs 1168 del clause 148 arith eq adapter 180 arith-upper 468 time 0.002 memory 51.68 max memory 68.47 num allocs 1.36351e+10
Expand
• start[0.027s]
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_114 (|rec_mk.state_4060| 0 0 0) dws_4054) expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4056| dws_4054) expansions
• unroll
 expr (bad_final_state_114 (bad_next_state_111 (|get.::.0_4052| dws_4054) (|rec_mk.state_4060| 0 0 0)) … expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4056| (|get.::.1_4053| dws_4054)) expansions
• unroll
 expr (bad_final_state_114 (bad_next_state_111 (|get.::.0_4052| (|get.::.1_4053| dws_4054)) (bad… expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4056| (|get.::.1_4053| (|get.::.1_4053| dws_4054… expansions
• unroll
 expr (let ((a!1 (bad_next_state_111 (|get.::.0_4052| (|get.::.1_4053| (|get.::.1_4053| dws_4… expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.1_4056| (|get.::.1_4053| (|get.::.1_4053| (|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!