# 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 :
let xor (x : bool) (y : bool) : bool = x <> y

Out:
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 :
let adder_sum a b cin =
xor (xor a b) cin

Out:
val adder_sum : bool -> bool -> bool -> bool = <fun>

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

Out:
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 :
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:
- : unit = ()

abcinsumcout
falsefalsefalsefalsefalse
falsefalsetruetruefalse
falsetruefalsetruefalse
falsetruetruefalsetrue
truefalsefalsetruefalse
truefalsetruefalsetrue
truetruefalsefalsetrue
truetruetruetruetrue

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

In :
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:
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 ordinalOrdinal.Int (_cnt a)
sub ordinalOrdinal.Int (_cnt (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 13 arith-conflicts 1 rlimit count 2072 mk clause 29 datatype occurs check 26 mk bool var 75 arith-lower 4 datatype splits 6 decisions 30 propagations 28 arith-max-rows 5 conflicts 8 datatype accessor ax 9 datatype constructor ax 14 num allocs 792930 final checks 6 added eqs 86 del clause 14 arith eq adapter 5 arith-upper 6 memory 5.66 max memory 5.66
Expand
• start[0.016s]
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 (|count.list (const 0)_1703| a_1688) expansions
• unroll
 expr (|count.list (const 0)_1703| (|get.::.1_1687| a_1688)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_1703| (|get.::.… expansions
• Unsat

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

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

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

In :
ripple_carry_adder zero zero false

Out:
- : bool list = []

In :
ripple_carry_adder one one false

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

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

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

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

Instance
proof attempt
ground_instances4
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 9 arith-make-feasible 6 arith-max-columns 4 rlimit count 5515 mk clause 246 datatype occurs check 61 mk bool var 240 datatype splits 8 decisions 65 propagations 290 conflicts 19 datatype accessor ax 32 minimized lits 4 datatype constructor ax 42 num allocs 3.23935e+06 final checks 9 added eqs 435 del clause 90 time 0.001 memory 6.65 max memory 6.65
Expand
• start[0.015s]
ripple_carry_adder ( :var_0: ) ( :var_1: ) false =
[false; false; false; true]
• unroll
 expr (ripple_carry_adder_25 a_43 b_44 false) expansions
• unroll
 expr (ripple_carry_adder_25 (|get.::.1_1746| a_43) (|get.::.1_1746| b_44) (adder_carry_out_21 (|get… expansions
• unroll
 expr (ripple_carry_adder_25 (|get.::.1_1746| (|get.::.1_1746| a_43)) (|get.::.1_1746| (|get.::.1_1746… expansions
• unroll
 expr (let ((a!1 (adder_carry_out_21 (|get.::.0_1745| (|get.::.1_1746| (|get.::.1_1746| a_43)… expansions
• Sat (Some let (a : bool list) = [true; true; true] let (b : bool list) = [true; false; 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 :
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:
val int_of_bit : bool -> int = <fun>
val int_of_bits : bool list -> int = <fun>

termination proof

### Termination proof

call int_of_bits (List.tl a) from int_of_bits a
originalint_of_bits a
subint_of_bits (List.tl a)
original ordinalOrdinal.Int (_cnt a)
sub ordinalOrdinal.Int (_cnt (List.tl a))
path[not Is_a([], a)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 11 rlimit count 1647 mk clause 19 datatype occurs check 18 mk bool var 42 arith-lower 3 datatype splits 3 decisions 10 propagations 12 arith-max-rows 3 conflicts 3 datatype accessor ax 7 datatype constructor ax 5 num allocs 5.32498e+06 final checks 6 added eqs 38 del clause 13 arith eq adapter 3 arith-upper 6 memory 9.59 max memory 9.59
Expand
• start[0.014s]
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
not Is_a([], a) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], a) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list (const 0)_1803| a_1792) expansions
• unroll
 expr (|count.list (const 0)_1803| (|get.::.1_1791| a_1792)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_1803| (|get.::.… expansions
• Unsat

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

In :
int_of_bits [true; false]

Out:
- : int = 1

In :
int_of_bits [false; true]

Out:
- : int = 2

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

Out:
- : int = 15


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

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

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

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

Instance
proof attempt
ground_instances10
definitions0
inductions0
search_time
0.026s
details
Expand
smt_stats
 num checks 21 arith-make-feasible 121 arith-max-columns 43 arith-conflicts 14 rlimit count 8248 arith-gcd-calls 8 arith-cheap-eqs 9 mk clause 359 datatype occurs check 29 mk bool var 518 arith-lower 95 arith-diseq 109 datatype splits 10 decisions 66 arith-propagations 81 propagations 315 arith-bound-propagations-cheap 81 arith-max-rows 18 conflicts 43 datatype accessor ax 44 arith-bound-propagations-lp 24 datatype constructor ax 44 num allocs 8.39573e+06 final checks 29 added eqs 598 del clause 337 arith eq adapter 135 arith-upper 140 arith-gcd-conflict 8 memory 12.95 max memory 12.95
Expand
• start[0.026s] int_of_bits ( :var_0: ) = 256
• unroll
 expr (int_of_bits_48 a_54) expansions
• unroll
 expr (int_of_bits_48 (|get.::.1_1834| a_54)) expansions
• unroll
 expr (int_of_bits_48 (|get.::.1_1834| (|get.::.1_1834| a_54))) expansions
• unroll
 expr (int_of_bits_48 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))))) (let ((a!2… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54)))))) (let ((a!2… expansions
• Sat (Some let (a : bool list) = [false; false; false; false; false; false; false; false; true] )
In :
int_of_bits (ripple_carry_adder CX.a CX.a false)

Out:
- : int = 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 :
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:
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 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 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 (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 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. b <> []
H3. a <> []
H4. 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)
|---------------------------------------------------------------------------
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. List.hd a
H3. b <> []
H4. a <> []
H5. 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)
|---------------------------------------------------------------------------
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 63 inductions 1 search_time 1.776s
Expand
• start[1.776s, "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[1.776s, "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[1.775s, "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 : int) = int_of_bits _x_0 in let (_x_8 : int) = 2 * _x_7 in let (_x_9 : int) = int_of_bits _x_1 in let (_x_10 : int) = 2 * _x_9 in let (_x_11 : bool) = int_of_bits (ripple_carry_adder a b false) = 1 + _x_8 + _x_10 in let (_x_12 : bool) = not (b <> []) in let (_x_13 : bool) = not (a <> []) 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_7 + _x_9) in let (_x_16 : bool) = not cin in let (_x_17 : bool) = int_of_bits (ripple_carry_adder a b true) = 2 + _x_8 + _x_10 in let (_x_18 : bool) = not (_x_14 = 1 + _x_7 + _x_9) in let (_x_19 : bool) = not _x_4 in ((((((((_x_3 || _x_4) || _x_6) || _x_11) || _x_12) || _x_13) || _x_15) && (((((((_x_2 || _x_4) || _x_6) || _x_16) || _x_12) || _x_13) || _x_17) || _x_18)) && (((((((_x_3 || _x_5) || _x_6) || _x_11) || _x_19) || _x_12) || _x_13) || _x_15)) && ((((((((_x_2 || _x_5) || _x_6) || _x_16) || _x_19) || _x_12) || _x_13) || _x_17) || _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, 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[1.775s, "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_2) || _x_5)) && (((_x_0 || _x_6) || _x_1) || _x_2)) && ((((_x_3 || _x_6) || _x_4) || _x_2) || _x_5) 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 :
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:
val single_adder_circuit_correct : bool -> bool -> bool -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.041s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 31 arith-max-columns 11 arith-conflicts 16 rlimit count 1683 mk clause 115 mk bool var 138 arith-lower 60 arith-diseq 2 decisions 15 arith-propagations 4 propagations 142 arith-bound-propagations-cheap 4 arith-max-rows 1 conflicts 16 minimized lits 22 added eqs 157 del clause 81 arith eq adapter 59 arith-upper 60 time 0.023 memory 48.97 max memory 66.44 num allocs 5.83316e+09
Expand
• start[0.041s]
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 :
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:
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_bit false

This simplifies 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

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

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 (ripple_carry_adder a 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_instances0
definitions39
inductions1
search_time
1.064s
details
Expand
smt_stats
 rlimit count 17651 time 0.018 memory 79.1 max memory 79.1 num allocs 7.53348e+09
Expand
• start[1.064s, "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[1.064s, "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[1.063s, "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, 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[1.063s, "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 : int) = int_of_bits a + int_of_bits b + int_of_bit cin in let (_x_2 : bool) = 0 = _x_1 in let (_x_3 : bool) = not (0 = List.length b) 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_1 in (((((cin || _x_0) || _x_2) || _x_3) && ((((cin || _x_4) || _x_5) || _x_2) || _x_6)) && (((_x_0 || _x_7) || _x_8) || _x_3)) && ((((_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 :
let bad_adder_sum a b cin =
not ((xor a b) || cin)

Out:
val bad_adder_sum : bool -> bool -> bool -> bool = <fun>

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

Out:
val bad_adder_carry_out : bool -> bool -> bool -> bool = <fun>

In :
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:
- : bool -> bool -> bool -> bool = <fun>
module CX : sig val a : bool val b : bool val cin : bool end

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

Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.035s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 14 arith-max-columns 11 arith-conflicts 6 rlimit count 1219 mk clause 88 mk bool var 80 arith-lower 29 arith-diseq 2 decisions 13 arith-propagations 5 propagations 72 arith-bound-propagations-cheap 5 arith-max-rows 1 conflicts 6 minimized lits 3 final checks 1 added eqs 75 del clause 32 arith eq adapter 28 arith-upper 27 time 0.019 memory 72.41 max memory 81.95 num allocs 1.37377e+10
Expand
• start[0.035s]
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) = false let (b : bool) = false let (cin : bool) = false )
In :
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:
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 ordinalOrdinal.Int (_cnt a)
sub ordinalOrdinal.Int (_cnt (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.170s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 13 arith-conflicts 1 rlimit count 2072 mk clause 29 datatype occurs check 26 mk bool var 75 arith-lower 4 datatype splits 6 decisions 30 propagations 28 arith-max-rows 5 conflicts 8 datatype accessor ax 9 datatype constructor ax 14 final checks 6 added eqs 86 del clause 14 arith eq adapter 5 arith-upper 6 memory 69.71 max memory 81.95 num allocs 1.40031e+10
Expand
• start[0.170s]
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 (|count.list (const 0)_3637| a_3622) expansions
• unroll
 expr (|count.list (const 0)_3637| (|get.::.1_3621| a_3622)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_3637| (|get.::.… expansions
• Unsat

In :
instance (fun a b -> int_of_bits (bad_ripple_carry_adder a b false) <> int_of_bits a + int_of_bits b)

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

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

Instance
proof attempt
ground_instances5
definitions0
inductions0
search_time
0.062s
details
Expand
smt_stats
 num checks 11 arith-make-feasible 54 arith-max-columns 30 arith-conflicts 3 rlimit count 5203 arith-gcd-calls 1 arith-cheap-eqs 33 mk clause 231 datatype occurs check 71 mk bool var 359 arith-lower 68 arith-diseq 28 datatype splits 26 decisions 108 arith-propagations 20 arith-patches-success 1 propagations 167 arith-patches 1 arith-bound-propagations-cheap 20 arith-max-rows 15 conflicts 19 datatype accessor ax 15 minimized lits 2 arith-bound-propagations-lp 17 datatype constructor ax 44 final checks 17 added eqs 429 del clause 88 arith eq adapter 65 arith-upper 60 time 0.001 memory 54.47 max memory 81.95 num allocs 1.47051e+10
Expand
• start[0.062s]
not
int_of_bits ( :var_0: ) + int_of_bits ( :var_1: ))
• unroll
 expr (int_of_bits_48 b_95) expansions
• unroll
 expr (int_of_bits_48 a_94) expansions
• unroll
 expr (bad_ripple_carry_adder_80 a_94 b_95 false) expansions
• unroll
 expr (int_of_bits_48 (bad_ripple_carry_adder_80 a_94 b_95 false)) expansions
• unroll
 expr (int_of_bits_48 (|get.::.1_3669| b_95)) expansions
• Sat (Some let (a : bool list) = [] let (b : bool list) = [true] )

Happy verifying!