# Verifying a Ripple-Carry Adder in Imandra¶

In this notebook, we'll verify a simple hardware design in Imandra, that of a full (arbitrary width) ripple-carry adder.

We'll express this simple piece of hardware at the gate level.

The correctness theorem we'll prove is as follows:

theorem full_ripple_carry_adder_correct a b cin =
List.length a = List.length b ==>
int_of_bits (ripple_carry_adder a b cin) =
int_of_bits a + int_of_bits b + int_of_bit cin


This theorem expresses that our (arbitrary width) adder circuit is correct for all possible bit sequences.

# Building the circuit in Imandra¶

We begin by defining xor and our basic building blocks adder_sum and adder_carry_out.

In [1]:
let xor (x : bool) (y : bool) : bool = x <> y

Out[1]:
val xor : bool -> bool -> bool = <fun>


We now define the basic sum and carry circuits for our adder.

We'll define two functions: adder_sum and adder_carry_out. Notice these are purely logical ("combinational"), i.e., they're defined using combinations of logic gates like xor, and (&&), and or (||) operating on bool values.

In [2]:
let adder_sum a b cin =
xor (xor a b) cin

Out[2]:
val adder_sum : bool -> bool -> bool -> bool = <fun>

In [3]:
let adder_carry_out a b cin =
((xor a b) && cin) || (a && b)

Out[3]:
val adder_carry_out : bool -> bool -> bool -> bool = <fun>


To help us understand and document how it works, we can use Imandra's Document machinery to produce a truth-table for our one-bit full adder circuit:

In [4]:
let args = CCList.cartesian_product [[true; false]; [true; false]; [true; false]] in
let pb b = Document.s (string_of_bool b) in
Imandra.display @@
List.map (function [a;b;cin] ->
[pb a; pb b; pb cin; pb (adder_sum a b cin); pb (adder_carry_out a b cin)]
| _ -> [])
args)

Out[4]:
- : unit = ()

abcinsumcout
falsefalsefalsefalsefalse
falsefalsetruetruefalse
falsetruefalsetruefalse
falsetruetruefalsetrue
truefalsefalsetruefalse
truefalsetruefalsetrue
truetruefalsefalsetrue
truetruetruetruetrue

We can now define our ripple-carry adder, for arbitrary length bitvector inputs.

In [5]:
let rec ripple_carry_adder (a : bool list) (b : bool list) (cin : bool) : bool list =
match a, b with
| a1 :: a', b1 :: b' ->
| _ -> if cin then [cin] else []

Out[5]:
val ripple_carry_adder : bool list -> bool list -> bool -> bool list = <fun>

termination proof

### Termination proof

call ripple_carry_adder (List.tl a) (List.tl b) (adder_carry_out (List.hd a) (List.hd b) cin) from ripple_carry_adder a b cin
original ordinal:Ordinal.Int (_cnt a)
sub ordinal:Ordinal.Int (_cnt (List.tl a))
path:[a <> [] && b <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.013s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 8 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 4 rlimit count: 2175 mk clause: 29 datatype occurs check: 25 mk bool var: 79 arith assert upper: 5 datatype splits: 6 decisions: 28 arith row summations: 6 propagations: 30 conflicts: 9 arith fixed eqs: 4 datatype accessor ax: 10 arith conflicts: 1 arith num rows: 5 datatype constructor ax: 14 num allocs: 5.80551e+06 final checks: 6 added eqs: 89 del clause: 16 arith eq adapter: 6 memory: 15.81 max memory: 15.81
Expand
• start[0.013s]
let (_x_0 : int) = count.list (const 0) a in
let (_x_1 : bool list) = List.tl a in
let (_x_2 : int) = count.list (const 0) _x_1 in
a <> [] && (b <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> not (_x_1 <> [] && (List.tl b) <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : bool list) = List.tl a in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) a in not (_x_0 <> [] && (List.tl b) <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (a <> [] && b <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_399/server| (|get.::.1_383/server|… expansions:
• unroll
 expr: (|count.list_399/server| (|get.::.1_383/server| a_384/server)) expansions:
• unroll
 expr: (|count.list_399/server| a_384/server) expansions:
• Unsat

Let's now compute with our adder to get a feel for it.

In [6]:
let zero = []
let one = [true]
let two = [false; true]

Out[6]:
val zero : 'a list = []
val one : bool list = [true]
val two : bool list = [false;true]

In [7]:
ripple_carry_adder zero zero false

Out[7]:
- : bool list = []

In [8]:
ripple_carry_adder one one false

Out[8]:
- : bool list = [false;true]

In [9]:
instance (fun a b -> ripple_carry_adder a b false = [false; false; false; true])

Out[9]:
- : bool list -> bool list -> bool = <fun>
module CX : sig val a : bool list val b : bool list end

Instance (after 4 steps, 0.014s):
let a : bool list = [true; true; true]
let b : bool list = [true; false; false]

Instance
proof attempt
ground_instances:4
definitions:0
inductions:0
search_time:
0.014s
details:
Expand
smt_stats:
 num checks: 9 rlimit count: 5367 mk clause: 238 datatype occurs check: 60 mk bool var: 227 datatype splits: 8 decisions: 57 propagations: 275 conflicts: 13 datatype accessor ax: 31 minimized lits: 3 datatype constructor ax: 37 num allocs: 1.1115e+07 final checks: 9 added eqs: 416 del clause: 90 memory: 16.81 max memory: 16.81
Expand
• start[0.014s]
ripple_carry_adder ( :var_0: ) ( :var_1: ) false
= [false; false; false; true]
• unroll
 expr: (ripple_carry_adder_1267/client a_1281/client b_1282/client false) expansions:
• unroll
 expr: (ripple_carry_adder_1267/client (|get.::.1_443/server| a_1281/client) (|get.::.1_443/server| b_1… expansions:
• unroll
 expr: (ripple_carry_adder_1267/client (|get.::.1_443/server| (|get.::.1_443/server| a_1281/client)) (|… expansions:
• unroll
 expr: (let ((a!1 (adder_carry_out_1263/client (|get.::.0_442/server| (|get.::.… expansions:
• Sat (Some let a : bool list = [true; true; true] let b : bool list = [true; false; false] )

# Relating bit sequences to natural numbers¶

Let's now define some functions to relate our bit sequences to natural numbers. These will be useful both in our computations and in our expression of our correctness criteria for the circut.

In [10]:
let int_of_bit (a : bool) : Z.t =
if a then 1 else 0

let rec int_of_bits (a : bool list) : Z.t =
match a with
| [] -> 0
| a :: a' -> int_of_bit a + 2 * (int_of_bits a')

Out[10]:
val int_of_bit : bool -> Z.t = <fun>
val int_of_bits : bool list -> Z.t = <fun>

termination proof

### Termination proof

call int_of_bits (List.tl a) from int_of_bits a
original:int_of_bits a
sub:int_of_bits (List.tl a)
original ordinal:Ordinal.Int (_cnt a)
sub ordinal:Ordinal.Int (_cnt (List.tl a))
path:[a <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 8 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 4 rlimit count: 1906 mk clause: 21 datatype occurs check: 19 mk bool var: 61 arith assert upper: 5 datatype splits: 3 decisions: 18 arith row summations: 6 propagations: 22 conflicts: 9 arith fixed eqs: 4 datatype accessor ax: 8 arith conflicts: 1 arith num rows: 5 datatype constructor ax: 9 num allocs: 1.73968e+07 final checks: 6 added eqs: 53 del clause: 12 arith eq adapter: 6 memory: 17.11 max memory: 17.11
Expand
• start[0.011s]
let (_x_0 : int) = count.list (const 0) a in
let (_x_1 : bool list) = List.tl a in
let (_x_2 : int) = count.list (const 0) _x_1 in
a <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_x_1 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : bool list) = List.tl a in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) a in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (a <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_499/server| (|get.::.1_487/server|… expansions:
• unroll
 expr: (|count.list_499/server| (|get.::.1_487/server| a_488/server)) expansions:
• unroll
 expr: (|count.list_499/server| a_488/server) expansions:
• Unsat

Let's experiment with these a bit, to ensure we understand their endianness (among other things).

In [11]:
int_of_bits [true; false]

Out[11]:
- : Z.t = 1

In [12]:
int_of_bits [false; true]

Out[12]:
- : Z.t = 2

In [13]:
int_of_bits [true; true; true; true;]

Out[13]:
- : Z.t = 15


We can of course use Imandra to obtain some interesting examples by querying for interesting inputs to our functions via instance:

In [14]:
instance (fun a -> int_of_bits a = 256)

Out[14]:
- : bool list -> bool = <fun>
module CX : sig val a : bool list end

Instance (after 10 steps, 0.021s):
let a : bool list =
[false; false; false; false; false; false; false; false; true]

Instance
proof attempt
ground_instances:10
definitions:0
inductions:0
search_time:
0.021s
details:
Expand
smt_stats:
 arith offset eqs: 16 arith assert lower: 226 datatype occurs check: 29 datatype splits: 10 arith bound prop: 18 arith branch var: 1 propagations: 496 arith patches: 1 conflicts: 48 arith fixed eqs: 41 datatype constructor ax: 73 num allocs: 2.54677e+07 final checks: 29 added eqs: 978 del clause: 468 num checks: 21 arith tableau max rows: 18 arith tableau max columns: 43 arith pivots: 74 rlimit count: 12029 mk clause: 501 mk bool var: 804 arith gcd tests: 11 arith assert upper: 165 decisions: 96 arith row summations: 111 datatype accessor ax: 72 minimized lits: 8 arith conflicts: 12 arith num rows: 18 arith assert diseq: 178 arith ineq splits: 1 arith eq adapter: 181 memory: 17.92 max memory: 17.92
Expand
• start[0.021s] int_of_bits ( :var_0: ) = 256
• unroll
 expr: (int_of_bits_1286/client a_1290/client) expansions:
• unroll
 expr: (int_of_bits_1286/client (|get.::.1_530/server| a_1290/client)) expansions:
• unroll
 expr: (int_of_bits_1286/client (|get.::.1_530/server| (|get.::.1_530/server| a_1290/client))) expansions:
• unroll
 expr: (int_of_bits_1286/client (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/server| … expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_530/server| (|get.::.1_530/server| (|get.::.1_530/… expansions:
• Sat (Some let a : bool list = [false; false; false; false; false; false; false; false; true] )
In [15]:
int_of_bits (ripple_carry_adder CX.a CX.a false)

Out[15]:
- : Z.t = 512


# Verifying our circuit: The adder is correct for all possible inputs¶

Let's now prove our main theorem, namely that ripple_carry_adder is correct.

We'll prove this theorem by induction following the recursive definition of ripple_carry_adder.

In [16]:
theorem full_ripple_carry_adder_correct a b cin =
List.length a = List.length b ==>
int_of_bits (ripple_carry_adder a b cin) =
int_of_bits a + int_of_bits b + int_of_bit cin

Out[16]:
val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
<fun>
Goal:

List.length a = List.length b
==> int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin.

1 nontautological subgoal.

We shall induct according to a scheme derived from ripple_carry_adder.

Induction scheme:

(not (a <> [] && b <> []) ==> φ a b cin)
&& (b <> []
&& (a <> []
&& φ (List.tl a) (List.tl b)
(adder_carry_out (List.hd a) (List.hd b) cin))
==> φ a b cin).

2 nontautological subgoals.

Subgoal 2:

H0. List.length a = List.length b
|---------------------------------------------------------------------------
C0. a <> [] && b <> []
C1. int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0)

This simplifies, using the definitions of List.length, int_of_bits and
ripple_carry_adder to the following 4 subgoals:

Subgoal 2.4:

H0. 0 = List.length b
|---------------------------------------------------------------------------
C0. cin
C1. a <> []
C2. 0 = int_of_bits a + int_of_bits b

This simplifies, using the definition of int_of_bits, and the rewrite rule
List.len_zero_is_empty to:

Subgoal 2.4':

H0. b = []
|---------------------------------------------------------------------------
C0. cin
C1. a <> []
C2. 0 = int_of_bits b

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

Subgoal 2.3:

H0. a <> []
H1. List.length a = 0
|---------------------------------------------------------------------------
C0. cin
C1. b <> []
C2. 0 = int_of_bits a + int_of_bits b

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

Subgoal 2.2:

H0. cin
H1. 0 = List.length b
|---------------------------------------------------------------------------
C0. a <> []
C1. 0 = int_of_bits a + int_of_bits b

This simplifies, using the definition of int_of_bits, and the rewrite rule
List.len_zero_is_empty to:

Subgoal 2.2':

H0. cin
H1. b = []
|---------------------------------------------------------------------------
C0. a <> []
C1. 0 = int_of_bits b

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

Subgoal 2.1:

H0. cin
H1. a <> []
H2. List.length a = 0
|---------------------------------------------------------------------------
C0. b <> []
C1. 0 = int_of_bits a + int_of_bits b

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

Subgoal 1:

H0. List.length a = List.length b
H1. b <> []
H2. a <> []
H3. List.length (List.tl a) = List.length (List.tl b)
==> int_of_bits
((List.hd a && List.hd b) || ((not (List.hd a) = List.hd b) && cin)))
= int_of_bits (List.tl a) + int_of_bits (List.tl b)
+ (if (List.hd a && List.hd b)
|| ((not (List.hd a) = List.hd b) && cin)
then 1 else 0)
|---------------------------------------------------------------------------
= int_of_bits a + int_of_bits b + (if cin then 1 else 0)

This simplifies, using the definitions of List.length, int_of_bits and
ripple_carry_adder to the following 4 subgoals:

Subgoal 1.4:

H0. List.length (List.tl a) = List.length (List.tl b)
H1. b <> []
H2. a <> []
H3. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin)
= int_of_bits (List.tl a) + int_of_bits (List.tl b)
|---------------------------------------------------------------------------
C0. cin
C1. List.hd a
C2. List.hd a = List.hd b
C3. int_of_bits (ripple_carry_adder a b false)
= 1 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)

But simplification reduces this to true, using the definitions of int_of_bits

Subgoal 1.3:

H0. List.length (List.tl a) = List.length (List.tl b)
H1. cin
H2. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin)
= 1 + int_of_bits (List.tl a) + int_of_bits (List.tl b)
H3. b <> []
H4. a <> []
|---------------------------------------------------------------------------
C0. List.hd a
C1. List.hd a = List.hd b
C2. int_of_bits (ripple_carry_adder a b true)
= 2 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)

But simplification reduces this to true, using the definitions of int_of_bits

Subgoal 1.2:

H0. List.length (List.tl a) = List.length (List.tl b)
H1. List.hd a
H2. b <> []
H3. a <> []
H4. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin)
= int_of_bits (List.tl a) + int_of_bits (List.tl b)
|---------------------------------------------------------------------------
C0. cin
C1. List.hd b
C2. List.hd a = List.hd b
C3. int_of_bits (ripple_carry_adder a b false)
= 1 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)

But simplification reduces this to true, using the definitions of int_of_bits

Subgoal 1.1:

H0. List.length (List.tl a) = List.length (List.tl b)
H1. cin
H2. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin)
= 1 + int_of_bits (List.tl a) + int_of_bits (List.tl b)
H3. List.hd a
H4. b <> []
H5. a <> []
|---------------------------------------------------------------------------
C0. List.hd b
C1. List.hd a = List.hd b
C2. int_of_bits (ripple_carry_adder a b true)
= 2 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)

But simplification reduces this to true, using the definitions of int_of_bits

ⓘ  Rules:
(:def List.length)
(:def int_of_bits)
(:rw List.len_zero_is_empty)
(:fc List.len_nonnegative)


Proved
proof
 ground_instances: 0 definitions: 105 inductions: 1 search_time: 0.948s
Expand
• start[0.948s, "Goal"]
List.length ( :var_0: ) = List.length ( :var_1: )
==> int_of_bits (ripple_carry_adder ( :var_0: ) ( :var_1: ) ( :var_2: ))
= int_of_bits ( :var_0: ) + int_of_bits ( :var_1: )
+ (if ( :var_2: ) then 1 else 0)
• #### subproof

not (List.length a = List.length b) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0))
• start[0.948s, "1"]
not (List.length a = List.length b)
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0))
• induction on (functional ripple_carry_adder)
:scheme (not (a <> [] && b <> []) ==> φ a b cin)
&& (b <> []
&& (a <> []
&& φ (List.tl a) (List.tl b)
(adder_carry_out (List.hd a) (List.hd b) cin))
==> φ a b cin)
• Split (let (_x_0 : bool) = a <> [] in
let (_x_1 : bool) = b <> [] in
let (_x_2 : bool) = not (List.length a = List.length b) in
let (_x_3 : bool)
= int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0)
in
let (_x_4 : bool list) = List.tl a in
let (_x_5 : bool list) = List.tl b in
let (_x_6 : bool) = List.hd a in
let (_x_7 : bool) = List.hd b in
let (_x_8 : bool) = (_x_6 && _x_7) || ((not _x_6 = _x_7) && cin) in
((_x_0 && _x_1) || _x_2 || _x_3)
&& (_x_2 || _x_3
|| not
(_x_1 && _x_0
&& (not (List.length _x_4 = List.length _x_5)
|| (int_of_bits (ripple_carry_adder _x_4 _x_5 _x_8)
= int_of_bits _x_4 + int_of_bits _x_5
+ (if _x_8 then 1 else 0)))))
:cases [not (List.length a = List.length b) || (a <> [] && b <> [])
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0));
let (_x_0 : bool list) = List.tl a in
let (_x_1 : bool list) = List.tl b in
let (_x_2 : bool) = List.hd a in
let (_x_3 : bool) = List.hd b in
let (_x_4 : bool)
= (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin)
in
not (List.length a = List.length b) || not (b <> [])
|| not (a <> [])
|| not
(List.length _x_0 = List.length _x_1
==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
= int_of_bits _x_0 + int_of_bits _x_1
+ (if _x_4 then 1 else 0))
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0))])
• ##### subproof
let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = List.hd a in let (_x_3 : bool) = List.hd b in let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in not (List.length a = List.length b) || not (b <> []) || not (a <> []) || not (List.length _x_0 = List.length _x_1 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) = int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0)) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0))
• start[0.946s, "1"]
let (_x_0 : bool list) = List.tl a in
let (_x_1 : bool list) = List.tl b in
let (_x_2 : bool) = List.hd a in
let (_x_3 : bool) = List.hd b in
let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in
not (List.length a = List.length b) || not (b <> []) || not (a <> [])
|| not
(List.length _x_0 = List.length _x_1
==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
= int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0))
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0))
• ###### simplify
 into: let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = not (List.length _x_0 = List.length _x_1) in let (_x_3 : bool) = cin || _x_2 in let (_x_4 : bool) = List.hd a in let (_x_5 : bool) = List.hd b in let (_x_6 : bool) = _x_4 = _x_5 in let (_x_7 : bool) = not (b <> []) in let (_x_8 : bool) = not (a <> []) in let (_x_9 : int) = int_of_bits _x_0 in let (_x_10 : int) = 2 * _x_9 in let (_x_11 : int) = int_of_bits _x_1 in let (_x_12 : int) = 2 * _x_11 in let (_x_13 : bool) = int_of_bits (ripple_carry_adder a b false) = 1 + _x_10 + _x_12 in let (_x_14 : int) = int_of_bits (ripple_carry_adder _x_0 _x_1 cin) in let (_x_15 : bool) = not (_x_14 = _x_9 + _x_11) in let (_x_16 : bool) = not cin in let (_x_17 : bool) = not (_x_14 = 1 + _x_9 + _x_11) in let (_x_18 : bool) = int_of_bits (ripple_carry_adder a b true) = 2 + _x_10 + _x_12 in let (_x_19 : bool) = not _x_4 in (_x_3 || _x_4 || _x_6 || _x_7 || _x_8 || _x_13 || _x_15) && (_x_2 || _x_4 || _x_6 || _x_16 || _x_17 || _x_7 || _x_8 || _x_18) && (_x_3 || _x_5 || _x_6 || _x_19 || _x_7 || _x_8 || _x_13 || _x_15) && (_x_2 || _x_5 || _x_6 || _x_16 || _x_17 || _x_19 || _x_7 || _x_8 || _x_18) expansions: [List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, List.length, List.length, int_of_bits, int_of_bits, List.length, List.length, int_of_bits, int_of_bits, List.length, List.length, int_of_bits, int_of_bits, List.length, List.length, int_of_bits, int_of_bits, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• Subproof
• Subproof
• Subproof
• Subproof
• ##### subproof
not (List.length a = List.length b) || (a <> [] && b <> []) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0))
• start[0.946s, "2"]
not (List.length a = List.length b) || (a <> [] && b <> [])
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + (if cin then 1 else 0))
• ###### simplify
 into: let (_x_0 : bool) = a <> [] in let (_x_1 : bool) = not (0 = List.length b) in let (_x_2 : bool) = 0 = int_of_bits a + int_of_bits b in let (_x_3 : bool) = b <> [] in let (_x_4 : bool) = not _x_0 in let (_x_5 : bool) = not (List.length a = 0) in let (_x_6 : bool) = not cin in (cin || _x_0 || _x_1 || _x_2) && (cin || _x_3 || _x_4 || _x_5 || _x_2) && (_x_0 || _x_6 || _x_1 || _x_2) && (_x_3 || _x_6 || _x_4 || _x_5 || _x_2) expansions: [List.length, List.length, List.length, List.length, int_of_bits, int_of_bits, ripple_carry_adder] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• Subproof
• Subproof
• Subproof
• Subproof

Excellent!

Note that we were able to prove this main theorem without introducing any auxiliary lemmas.

Nevertheless, it's almost always useful to prove local lemmas about our functions.

For example, the following is a very useful property to know about our single-step adder, adder_sum. We'll introduce it as a rewrite rule so that we may use it for an alternative proof of our main theorem.

In [17]:
theorem single_adder_circuit_correct a b cin =
= int_of_bit a + int_of_bit b + int_of_bit cin - (2 * (int_of_bit (adder_carry_out a b cin)))
[@@rewrite]

Out[17]:
val single_adder_circuit_correct : bool -> bool -> bool -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.031s
details:
Expand
smt_stats:
 num checks: 1 arith assert lower: 60 arith tableau max rows: 1 arith tableau max columns: 10 arith pivots: 4 rlimit count: 1593 mk clause: 162 mk bool var: 127 arith assert upper: 60 decisions: 17 propagations: 156 conflicts: 18 minimized lits: 12 arith conflicts: 16 arith num rows: 1 arith assert diseq: 1 num allocs: 2.77213e+09 added eqs: 98 del clause: 138 arith eq adapter: 59 time: 0.018 memory: 18.48 max memory: 19.08
Expand
• start[0.031s]
let (_x_0 : bool) = not (( :var_0: ) = ( :var_1: )) in
(if not (_x_0 = ( :var_2: )) then 1 else 0)
= ((if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0)
+ (if ( :var_2: ) then 1 else 0))
- 2
* (if (_x_0 && ( :var_2: )) || (( :var_0: ) && ( :var_1: )) then 1
else 0)
• #### simplify

 into: (if ( :var_0: ) = ( :var_1: ) = ( :var_2: ) then 1 else 0) = (if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0) + (if ( :var_2: ) then 1 else 0) + (-2) * (if (( :var_0: ) && ( :var_1: )) || ((not ( :var_0: ) = ( :var_1: )) && ( :var_2: )) then 1 else 0) expansions: [] rewrite_steps: forward_chaining:
• Unsat

#### Warning

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

#### Warning

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

Notice the above Warnings, in particular about int_of_bit and adder_sum. These are printed because we've specified Imandra to install this theorem as a rewrite rule, and the LHS (left-hand-side) of the rule contains non-recursive functions which will, unless they are disabled, be expanded before rewriting can be applied.

Can you see an alternative proof of our main theorem which makes use of this rule? We just need to follow the advice of the warning!

In [18]:
theorem full_ripple_carry_adder_correct a b cin =
List.length a = List.length b ==>
int_of_bits (ripple_carry_adder a b cin) =
int_of_bits a + int_of_bits b + int_of_bit cin

Out[18]:
val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
<fun>
Goal:

List.length a = List.length b
==> int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin.

1 nontautological subgoal.

We shall induct according to a scheme derived from ripple_carry_adder.

Induction scheme:

(not (a <> [] && b <> []) ==> φ a b cin)
&& (b <> []
&& (a <> []
&& φ (List.tl a) (List.tl b)
(adder_carry_out (List.hd a) (List.hd b) cin))
==> φ a b cin).

2 nontautological subgoals.

Subgoal 2:

H0. List.length a = List.length b
|---------------------------------------------------------------------------
C0. a <> [] && b <> []
C1. int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin

This simplifies, using the definitions of List.length, int_of_bits and
ripple_carry_adder to the following 4 subgoals:

Subgoal 2.4:

H0. 0 = List.length b
|---------------------------------------------------------------------------
C0. cin
C1. a <> []
C2. 0 = int_of_bits a + int_of_bits b + int_of_bit cin

This simplifies, using the definition of int_of_bits, and the rewrite rule
List.len_zero_is_empty to:

Subgoal 2.4':

H0. b = []
|---------------------------------------------------------------------------
C0. cin
C1. a <> []
C2. 0 = int_of_bits b + int_of_bit false

This simplifies, using the definition of int_of_bits to:

Subgoal 2.4'':

|---------------------------------------------------------------------------
C0. cin
C1. a <> []
C2. 0 = int_of_bit false

But we verify Subgoal 2.4'' by recursive unrolling.

Subgoal 2.3:

H0. a <> []
H1. List.length a = 0
|---------------------------------------------------------------------------
C0. cin
C1. b <> []
C2. 0 = int_of_bits a + int_of_bits b + int_of_bit cin

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

Subgoal 2.2:

H0. cin
H1. 0 = List.length b
|---------------------------------------------------------------------------
C0. a <> []
C1. int_of_bit true = int_of_bits a + int_of_bits b + int_of_bit cin

This simplifies, using the definition of int_of_bits, and the rewrite rule
List.len_zero_is_empty to:

Subgoal 2.2':

H0. cin
H1. b = []
|---------------------------------------------------------------------------
C0. a <> []
C1. 0 = int_of_bits b

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

Subgoal 2.1:

H0. cin
H1. a <> []
H2. List.length a = 0
|---------------------------------------------------------------------------
C0. b <> []
C1. int_of_bit true = int_of_bits a + int_of_bits b + int_of_bit cin

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

Subgoal 1:

H0. List.length a = List.length b
H1. b <> []
H2. a <> []
H3. List.length (List.tl a) = List.length (List.tl b)
==> int_of_bits
((List.hd a && List.hd b) || ((not (List.hd a) = List.hd b) && cin)))
= int_of_bits (List.tl a) + int_of_bits (List.tl b)
+ int_of_bit
((List.hd a && List.hd b)
|| ((not (List.hd a) = List.hd b) && cin))
|---------------------------------------------------------------------------
= int_of_bits a + int_of_bits b + int_of_bit cin

But simplification reduces this to true, using the definitions of
List.length, int_of_bits and ripple_carry_adder, and the rewrite rule

ⓘ  Rules:
(:def List.length)
(:def int_of_bits)
(:rw List.len_zero_is_empty)
(:fc List.len_nonnegative)


Proved
proof
ground_instances:0
definitions:49
inductions:1
search_time:
0.801s
details:
Expand
smt_stats:
 rlimit count: 17198 time: 0.009 memory: 19.05 max memory: 19.45 num allocs: 4.497e+09
Expand
• start[0.801s, "Goal"]
List.length ( :var_0: ) = List.length ( :var_1: )
==> int_of_bits (ripple_carry_adder ( :var_0: ) ( :var_1: ) ( :var_2: ))
= int_of_bits ( :var_0: ) + int_of_bits ( :var_1: )
+ int_of_bit ( :var_2: )
• #### subproof

not (List.length a = List.length b) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + int_of_bit cin)
• start[0.801s, "1"]
not (List.length a = List.length b)
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin)
• induction on (functional ripple_carry_adder)
:scheme (not (a <> [] && b <> []) ==> φ a b cin)
&& (b <> []
&& (a <> []
&& φ (List.tl a) (List.tl b)
(adder_carry_out (List.hd a) (List.hd b) cin))
==> φ a b cin)
• Split (let (_x_0 : bool) = a <> [] in
let (_x_1 : bool) = b <> [] in
let (_x_2 : bool) = not (List.length a = List.length b) in
let (_x_3 : bool)
= int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin
in
let (_x_4 : bool list) = List.tl a in
let (_x_5 : bool list) = List.tl b in
let (_x_6 : bool) = List.hd a in
let (_x_7 : bool) = List.hd b in
let (_x_8 : bool) = (_x_6 && _x_7) || ((not _x_6 = _x_7) && cin) in
((_x_0 && _x_1) || _x_2 || _x_3)
&& (_x_2 || _x_3
|| not
(_x_1 && _x_0
&& (not (List.length _x_4 = List.length _x_5)
|| (int_of_bits (ripple_carry_adder _x_4 _x_5 _x_8)
= int_of_bits _x_4 + int_of_bits _x_5
+ int_of_bit _x_8))))
:cases [not (List.length a = List.length b) || (a <> [] && b <> [])
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin);
let (_x_0 : bool list) = List.tl a in
let (_x_1 : bool list) = List.tl b in
let (_x_2 : bool) = List.hd a in
let (_x_3 : bool) = List.hd b in
let (_x_4 : bool)
= (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin)
in
not (List.length a = List.length b) || not (b <> [])
|| not (a <> [])
|| not
(List.length _x_0 = List.length _x_1
==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
= int_of_bits _x_0 + int_of_bits _x_1
+ int_of_bit _x_4)
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin)])
• ##### subproof
let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = List.hd a in let (_x_3 : bool) = List.hd b in let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in not (List.length a = List.length b) || not (b <> []) || not (a <> []) || not (List.length _x_0 = List.length _x_1 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) = int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + int_of_bit cin)
• start[0.800s, "1"]
let (_x_0 : bool list) = List.tl a in
let (_x_1 : bool list) = List.tl b in
let (_x_2 : bool) = List.hd a in
let (_x_3 : bool) = List.hd b in
let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in
not (List.length a = List.length b) || not (b <> []) || not (a <> [])
|| not
(List.length _x_0 = List.length _x_1
==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
= int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4)
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin)
• ###### simplify
 into: true expansions: [List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, List.length, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder] rewrite_steps: single_adder_circuit_correctsingle_adder_circuit_correctsingle_adder_circuit_correctsingle_adder_circuit_correctsingle_adder_circuit_correct forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• ##### subproof
not (List.length a = List.length b) || (a <> [] && b <> []) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + int_of_bit cin)
• start[0.800s, "2"]
not (List.length a = List.length b) || (a <> [] && b <> [])
|| (int_of_bits (ripple_carry_adder a b cin)
= int_of_bits a + int_of_bits b + int_of_bit cin)
• ###### simplify
 into: let (_x_0 : bool) = a <> [] in let (_x_1 : bool) = not (0 = List.length b) in let (_x_2 : int) = int_of_bits a + int_of_bits b + int_of_bit cin in let (_x_3 : bool) = 0 = _x_2 in let (_x_4 : bool) = b <> [] in let (_x_5 : bool) = not _x_0 in let (_x_6 : bool) = not (List.length a = 0) in let (_x_7 : bool) = not cin in let (_x_8 : bool) = int_of_bit true = _x_2 in (cin || _x_0 || _x_1 || _x_3) && (cin || _x_4 || _x_5 || _x_3 || _x_6) && (_x_0 || _x_7 || _x_1 || _x_8) && (_x_4 || _x_7 || _x_5 || _x_8 || _x_6) expansions: [List.length, List.length, List.length, List.length, int_of_bits, int_of_bits, ripple_carry_adder] rewrite_steps: forward_chaining: List.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegativeList.len_nonnegative
• Subproof
• Subproof
• Subproof
• Subproof

If we inspect the proof, we'll find that our rewrite rule single_adder_circuit_correct was used to close our key subgoal under our induction. Beautiful!

# Examining a flawed circuit with Imandra¶

Now that we've verified our adder, let's imagine we'd instead designed a flawed version of our circut and use Imandra to analyse it.

Can you spot the error?

In [19]:
let bad_adder_sum a b cin =
not ((xor a b) || cin)

Out[19]:
val bad_adder_sum : bool -> bool -> bool -> bool = <fun>

In [20]:
let bad_adder_carry_out a b cin =
((xor a b) && cin) || (a && b)

Out[20]:
val bad_adder_carry_out : bool -> bool -> bool -> bool = <fun>

In [21]:
verify (fun a b cin ->
= int_of_bit a + int_of_bit b + int_of_bit cin - (2 * (int_of_bit (bad_adder_carry_out a b cin))))

Out[21]:
- : bool -> bool -> bool -> bool = <fun>
module CX : sig val a : bool val b : bool val cin : bool end

Counterexample (after 0 steps, 0.019s):
let a : bool = true
let b : bool = true
let cin : bool = false

Refuted
proof attempt
ground_instances:0
definitions:0
inductions:0
search_time:
0.019s
details:
Expand
smt_stats:
 num checks: 1 arith assert lower: 11 arith tableau max rows: 1 arith tableau max columns: 10 arith pivots: 3 rlimit count: 948 mk clause: 54 mk bool var: 46 arith assert upper: 13 decisions: 10 propagations: 31 conflicts: 3 arith fixed eqs: 1 arith conflicts: 2 arith num rows: 1 arith assert diseq: 1 final checks: 1 added eqs: 20 del clause: 8 arith eq adapter: 12 time: 0.009 memory: 19.8 max memory: 20.28 num allocs: 8.15252e+09
Expand
• start[0.019s]
let (_x_0 : bool) = not (( :var_0: ) = ( :var_1: )) in
(if not (_x_0 || ( :var_2: )) then 1 else 0)
= ((if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0)
+ (if ( :var_2: ) then 1 else 0))
- 2
* (if (_x_0 && ( :var_2: )) || (( :var_0: ) && ( :var_1: )) then 1
else 0)
• #### simplify

 into: let (_x_0 : bool) = not ( :var_0: ) = ( :var_1: ) in (if _x_0 || ( :var_2: ) then 0 else 1) = (if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0) + (if ( :var_2: ) then 1 else 0) + (-2) * (if (( :var_0: ) && ( :var_1: )) || (_x_0 && ( :var_2: )) then 1 else 0) expansions: [] rewrite_steps: forward_chaining:
• Sat (Some let a : bool = true let b : bool = true let cin : bool = false )
In [22]:
let rec bad_ripple_carry_adder (a : bool list) (b : bool list) (cin : bool) : bool list =
match a, b with
| a1 :: a', b1 :: b' ->
| _ -> if cin then [cin] else []

Out[22]:
val bad_ripple_carry_adder : bool list -> bool list -> bool -> bool list =
<fun>

termination proof

### Termination proof

call bad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin) from bad_ripple_carry_adder a b cin
original ordinal:Ordinal.Int (_cnt a)
sub ordinal:Ordinal.Int (_cnt (List.tl a))
path:[a <> [] && b <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.020s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 8 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 4 rlimit count: 2175 mk clause: 29 datatype occurs check: 25 mk bool var: 79 arith assert upper: 5 datatype splits: 6 decisions: 28 arith row summations: 6 propagations: 30 conflicts: 9 arith fixed eqs: 4 datatype accessor ax: 10 arith conflicts: 1 arith num rows: 5 datatype constructor ax: 14 final checks: 6 added eqs: 89 del clause: 16 arith eq adapter: 6 memory: 20.1 max memory: 20.28 num allocs: 8.28432e+09
Expand
• start[0.020s]
let (_x_0 : int) = count.list (const 0) a in
let (_x_1 : bool list) = List.tl a in
let (_x_2 : int) = count.list (const 0) _x_1 in
a <> [] && (b <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> not (_x_1 <> [] && (List.tl b) <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : bool list) = List.tl a in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) a in not (_x_0 <> [] && (List.tl b) <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (a <> [] && b <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1810/server| (|g… expansions:
• unroll
 expr: (|count.list_1810/server| (|get.::.1_1794/server| a_1795/server)) expansions:
• unroll
 expr: (|count.list_1810/server| a_1795/server) expansions:
• Unsat
In [23]:
instance (fun a b -> int_of_bits (bad_ripple_carry_adder a b false) <> int_of_bits a + int_of_bits b)

Out[23]:
- : bool list -> bool list -> bool = <fun>
module CX : sig val a : bool list val b : bool list end

Instance (after 5 steps, 0.013s):
let a : bool list = []
let b : bool list = [true]

Instance
proof attempt
ground_instances:5
definitions:0
inductions:0
search_time:
0.013s
details:
Expand
smt_stats:
 arith offset eqs: 2 num checks: 11 arith assert lower: 59 arith tableau max rows: 11 arith tableau max columns: 25 arith pivots: 39 rlimit count: 6641 mk clause: 163 datatype occurs check: 25 mk bool var: 306 arith assert upper: 60 datatype splits: 10 decisions: 52 arith row summations: 115 arith bound prop: 9 propagations: 130 conflicts: 10 arith fixed eqs: 30 datatype accessor ax: 15 arith conflicts: 2 arith num rows: 11 arith assert diseq: 12 datatype constructor ax: 27 final checks: 11 added eqs: 366 del clause: 75 arith eq adapter: 60 memory: 20.54 max memory: 20.54 num allocs: 8.42502e+09
Expand
• start[0.013s]
not
= int_of_bits ( :var_0: ) + int_of_bits ( :var_1: ))
• unroll
 expr: (int_of_bits_1286/client b_1327/client) expansions:
• unroll
 expr: (int_of_bits_1286/client a_1326/client) expansions:
• unroll
 expr: (int_of_bits_1286/client (bad_ripple_carry_adder_1316/client a_1326/client b_1327/client false)) expansions:
• unroll
 expr: (bad_ripple_carry_adder_1316/client a_1326/client b_1327/client false) expansions:
• unroll
 expr: (int_of_bits_1286/client (|get.::.1_1842/server| b_1327/client)) expansions:
• Sat (Some let a : bool list = [] let b : bool list = [true] )

Happy verifying!