# 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 (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.031s
details
Expand
smt_stats
 num checks 8 arith assert lower 8 arith pivots 4 rlimit count 2128 mk clause 30 datatype occurs check 22 mk bool var 84 arith assert upper 5 datatype splits 6 decisions 28 arith add rows 6 propagations 30 conflicts 9 arith fixed eqs 4 datatype accessor ax 10 arith conflicts 1 datatype constructor ax 14 num allocs 1.05424e+06 final checks 6 added eqs 87 del clause 17 arith eq adapter 6 memory 6.33 max memory 6.33
Expand
• start[0.031s]
(a <> [] && b <> [])
&& Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
==> not ((List.tl a) <> [] && (List.tl b) <> [])
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
(Ordinal.Int (Ordinal.count a))
• ##### simplify
 into (not (((a <> [] && b <> []) && Ordinal.count a >= 0) && Ordinal.count (List.tl a) >= 0) || not ((List.tl a) <> [] && (List.tl b) <> [])) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a))) (Ordinal.Int (Ordinal.count a)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_bool list_1230| … expansions
• unroll
 expr (|count_bool list_1230| (|get.::.1_1216| a_1217)) expansions
• unroll
 expr (|count_bool list_1230| a_1217) expansions
• ##### unsat
(let ((a!1 (= (|count_bool list_1230| a_1217)
(+ 1 (|count_bool list_1230| (|get.:…

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.029s):
let (a : bool list) = [true; true; false]
let (b : bool list) = [true; false; true]

Instance
proof attempt
ground_instances4
definitions0
inductions0
search_time
0.029s
details
Expand
smt_stats
 num checks 9 rlimit count 4328 mk clause 200 datatype occurs check 68 mk bool var 191 datatype splits 13 decisions 66 propagations 218 conflicts 19 datatype accessor ax 27 minimized lits 1 datatype constructor ax 30 num allocs 4.50725e+06 final checks 13 added eqs 297 del clause 46 memory 7.43 max memory 7.43
Expand
• start[0.029s]
false :: (false :: (false :: (true :: …)))
• unroll
 expr (ripple_carry_adder_25 a_37 b_38 false) expansions
• unroll
 expr (let ((a!1 (and (= (not (|get.::.0_1247| a_37)) (|get.::.0_1247| b_38)) false))) (ripple_carry_add… expansions
• unroll
 expr (let ((a!1 (= (not (|get.::.0_1247| (|get.::.1_1248| a_37))) (|get.::.0_1247| (|get.::… expansions
• unroll
 expr (let ((a!1 (not (|get.::.0_1247| (|get.::.1_1248| (|get.::.1_1248| a_37))))) (a!3 (= (not (|ge… expansions
• Sat (Some let (a : bool list) = [true; true; false] let (b : bool list) = [true; false; true] )

# 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 -> 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
originalint_of_bits a
subint_of_bits (List.tl a)
original ordinalOrdinal.Int (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[not (a = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.023s
details
Expand
smt_stats
 num checks 7 arith assert lower 6 arith pivots 4 rlimit count 1908 mk clause 11 datatype occurs check 33 mk bool var 58 arith assert upper 4 datatype splits 6 decisions 16 arith add rows 5 propagations 10 conflicts 7 arith fixed eqs 3 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 8 num allocs 9.45408e+06 final checks 9 added eqs 48 del clause 5 arith eq adapter 3 memory 7.82 max memory 7.82
Expand
• start[0.023s]
not (a = []) && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
==> List.tl a = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
(Ordinal.Int (Ordinal.count a))
• ##### simplify
 into (not ((not (a = []) && Ordinal.count a >= 0) && Ordinal.count (List.tl a) >= 0) || List.tl a = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a))) (Ordinal.Int (Ordinal.count a)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_bool list_1269| … expansions
• unroll
 expr (|count_bool list_1269| (|get.::.1_1259| a_1260)) expansions
• unroll
 expr (|count_bool list_1269| a_1260) expansions
• ##### unsat
(let ((a!1 (= (|count_bool list_1269| a_1260)
(+ 1 (|count_bool list_1269| (|get.:…

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

In :
int_of_bits [true; false]

Out:
- : Z.t = 1

In :
int_of_bits [false; true]

Out:
- : Z.t = 2

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

Out:
- : 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 :
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.096s):
let (a : bool list) =
[false; false; false; false; false; false; false; false; true]

Instance
proof attempt
ground_instances10
definitions0
inductions0
search_time
0.096s
details
Expand
smt_stats
 arith offset eqs 13 num checks 21 arith assert lower 269 arith pivots 69 rlimit count 14247 mk clause 605 datatype occurs check 162 mk bool var 1236 arith gcd tests 10 arith assert upper 256 datatype splits 124 decisions 190 arith add rows 114 arith bound prop 19 propagations 708 conflicts 82 arith fixed eqs 66 datatype accessor ax 108 minimized lits 12 arith conflicts 15 arith assert diseq 131 datatype constructor ax 133 num allocs 1.64258e+07 final checks 49 added eqs 1395 del clause 582 arith eq adapter 276 memory 8.84 max memory 8.84
Expand
• start[0.096s] int_of_bits :var_0: = 256
• unroll
 expr (int_of_bits_42 a_46) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_1275| a_46)) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_1275| (|get.::.1_1275| a_46))) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))))) (let ((a!2… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| (|get.::.1_1275| a_46)))))) (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:
- : 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 :
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 <> []) ==> φ cin b a)
&& ((a <> [] && b <> [])
&& φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
(List.tl a)
==> φ cin b a).

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. a <> []
C1. 0 = int_of_bits a + int_of_bits b
C2. 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. a <> []
C1. 0 = int_of_bits b
C2. cin

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

Subgoal 2.3:

H0. List.length a = 0
H1. a <> []
|---------------------------------------------------------------------------
C0. b <> []
C1. 0 = int_of_bits a + int_of_bits b
C2. 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.2:

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

But simplification reduces this to true, using the definitions of

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


Proved
proof
 ground_instances 0 definitions 33 inductions 1 search_time 1.938s
Expand
• start[1.938s, "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.937s, "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 <> []) ==> φ cin b a)
&& ((a <> [] && b <> [])
&& φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
(List.tl a)
==> φ cin b a)
• Split (((a <> [] && b <> [] || 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))
&& ((not
((a <> [] && b <> [])
&& (not (List.length (List.tl a) = List.length (List.tl b))
|| int_of_bits
(not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b))
=
(int_of_bits (List.tl a) + int_of_bits (List.tl b))
+ (if not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b
then 1 else 0)))
|| 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))
: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);
(((not (a <> []) || not (b <> []))
|| not
(not (List.length (List.tl a) = List.length (List.tl b))
|| int_of_bits
(not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b))
=
(int_of_bits (List.tl a) + int_of_bits (List.tl b))
+ (if not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b
then 1 else 0)))
|| 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)])
• ##### subproof
(((not (a <> []) || not (b <> [])) || not (not (List.length (List.tl a) = List.length (List.tl b)) || int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)) = (int_of_bits (List.tl a) + int_of_bits (List.tl b)) + (if not (List.hd a) = List.hd b && cin || List.hd a && List.hd b then 1 else 0))) || 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.935s, "1"]
(((not (a <> []) || not (b <> []))
|| not
(not (List.length (List.tl a) = List.length (List.tl b))
|| int_of_bits
(not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
=
(int_of_bits (List.tl a) + int_of_bits (List.tl b))
+ (if not (List.hd a) = List.hd b && cin || List.hd a && List.hd b
then 1 else 0)))
|| 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)
• ###### 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, 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_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) + (if cin then 1 else 0)
• start[1.935s, "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 (((((not (0 = List.length b) || a <> []) || 0 = int_of_bits a + int_of_bits b) || cin) && ((((not (List.length a = 0) || b <> []) || not (a <> [])) || 0 = int_of_bits a + int_of_bits b) || cin)) && (((not (0 = List.length b) || a <> []) || 0 = int_of_bits a + int_of_bits b) || not cin)) && ((((not (List.length a = 0) || b <> []) || not (a <> [])) || 0 = int_of_bits a + int_of_bits b) || not cin) 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.035s
details
Expand
smt_stats
 num checks 1 arith assert lower 60 arith pivots 2 rlimit count 1505 mk clause 160 mk bool var 133 arith assert upper 60 decisions 17 propagations 158 conflicts 17 minimized lits 12 arith conflicts 16 arith assert diseq 1 num allocs 2.90231e+09 added eqs 98 del clause 136 arith eq adapter 59 memory 30.02 max memory 48.7
Expand
• start[0.035s]
(if not (not (: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 not (:var_0: = :var_1:) && :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 not :var_0: = :var_1: && :var_2: || :var_0: && :var_1: then 1 else 0) expansions [] rewrite_steps forward_chaining
• #### unsat

(let ((a!1 (= (ite (= (= a_1824 b_1825) cin_1826) 1 0) 1))
(a!2 (<= (ite (= (= a_1824 b_1825) …

#### 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 <> []) ==> φ cin b a)
&& ((a <> [] && b <> [])
&& φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
(List.tl a)
==> φ cin b a).

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. a <> []
C1. 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin
C2. 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. a <> []
C1. 0 = int_of_bits b + int_of_bit false
C2. cin

This simplifies, using the definition of int_of_bits to:

Subgoal 2.4'':

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

But we verify Subgoal 2.4'' by recursive unrolling.

Subgoal 2.3:

H0. List.length a = 0
H1. a <> []
|---------------------------------------------------------------------------
C0. b <> []
C1. 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin
C2. 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.2:

H0. 0 = List.length b
H1. cin
|---------------------------------------------------------------------------
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. b = []
H1. cin
|---------------------------------------------------------------------------
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. List.length a = 0
H1. a <> []
H2. cin
|---------------------------------------------------------------------------
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 definition of int_of_bits,
and the rewrite rule List.len_zero_is_empty.

Subgoal 1:

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

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
definitions27
inductions1
search_time
1.161s
details
Expand
smt_stats
 rlimit count 12419 mk bool var 5 memory 45.67 max memory 66.65 num allocs 4.61744e+09
Expand
• start[1.161s, "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.161s, "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 <> []) ==> φ cin b a)
&& ((a <> [] && b <> [])
&& φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
(List.tl a)
==> φ cin b a)
• Split (((a <> [] && b <> [] || 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)
&& ((not
((a <> [] && b <> [])
&& (not (List.length (List.tl a) = List.length (List.tl b))
|| int_of_bits
(not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b))
=
(int_of_bits (List.tl a) + int_of_bits (List.tl b))
+ int_of_bit
(not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b)))
|| 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)
: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;
(((not (a <> []) || not (b <> []))
|| not
(not (List.length (List.tl a) = List.length (List.tl b))
|| int_of_bits
(not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b))
=
(int_of_bits (List.tl a) + int_of_bits (List.tl b))
+ int_of_bit
(not (List.hd a) = List.hd b && cin
|| List.hd a && List.hd b)))
|| 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])
• ##### subproof
(((not (a <> []) || not (b <> [])) || not (not (List.length (List.tl a) = List.length (List.tl b)) || int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)) = (int_of_bits (List.tl a) + int_of_bits (List.tl b)) + int_of_bit (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))) || 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.159s, "1"]
(((not (a <> []) || not (b <> []))
|| not
(not (List.length (List.tl a) = List.length (List.tl b))
|| int_of_bits
(not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
=
(int_of_bits (List.tl a) + int_of_bits (List.tl b))
+ int_of_bit
(not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)))
|| 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
• ###### simplify
 into true expansions [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] rewrite_steps single_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_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.159s, "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 (((((not (0 = List.length b) || a <> []) || 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin) || cin) && ((((not (List.length a = 0) || b <> []) || not (a <> [])) || 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin) || cin)) && (((not (0 = List.length b) || a <> []) || int_of_bit true = (int_of_bits a + int_of_bits b) + int_of_bit cin) || not cin)) && ((((not (List.length a = 0) || b <> []) || not (a <> [])) || int_of_bit true = (int_of_bits a + int_of_bits b) + int_of_bit cin) || not cin) 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.044s):
let (a : bool) = true
let (b : bool) = true
let (cin : bool) = true

Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.044s
details
Expand
smt_stats
 num checks 1 arith assert lower 5 arith pivots 2 rlimit count 761 mk clause 39 mk bool var 38 arith assert upper 7 decisions 4 propagations 14 arith fixed eqs 1 arith assert diseq 1 final checks 1 added eqs 9 del clause 2 arith eq adapter 6 memory 28.44 max memory 72.35 num allocs 9.04075e+09
Expand
• start[0.044s]
(if not (not (: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 not (:var_0: = :var_1:) && :var_2: || :var_0: && :var_1: then 1
else 0))
• #### simplify

 into (if not :var_0: = :var_1: || :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 not :var_0: = :var_1: && :var_2: || :var_0: && :var_1: then 1 else 0) expansions [] rewrite_steps forward_chaining
• Sat (Some let (a : bool) = true let (b : bool) = true let (cin : bool) = true )
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 (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
 num checks 8 arith assert lower 8 arith pivots 4 rlimit count 2128 mk clause 30 datatype occurs check 22 mk bool var 84 arith assert upper 5 datatype splits 6 decisions 28 arith add rows 6 propagations 30 conflicts 9 arith fixed eqs 4 datatype accessor ax 10 arith conflicts 1 datatype constructor ax 14 final checks 6 added eqs 87 del clause 17 arith eq adapter 6 memory 28.66 max memory 72.35 num allocs 9.19996e+09
Expand
• start[0.021s]
(a <> [] && b <> [])
&& Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
==> not ((List.tl a) <> [] && (List.tl b) <> [])
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
(Ordinal.Int (Ordinal.count a))
• ##### simplify
 into (not (((a <> [] && b <> []) && Ordinal.count a >= 0) && Ordinal.count (List.tl a) >= 0) || not ((List.tl a) <> [] && (List.tl b) <> [])) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a))) (Ordinal.Int (Ordinal.count a)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_bool list_2198| … expansions
• unroll
 expr (|count_bool list_2198| (|get.::.1_2184| a_2185)) expansions
• unroll
 expr (|count_bool list_2198| a_2185) expansions
• ##### unsat
(let ((a!1 (= (|count_bool list_2198| a_2185)
(+ 1 (|count_bool list_2198| (|get.:…

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.031s):
let (a : bool list) = []
let (b : bool list) = [true]

Instance
proof attempt
ground_instances5
definitions0
inductions0
search_time
0.031s
details
Expand
smt_stats
 arith offset eqs 5 num checks 11 arith assert lower 56 arith patches_succ 1 arith pivots 42 rlimit count 7199 mk clause 191 datatype occurs check 70 mk bool var 347 arith gcd tests 19 arith assert upper 80 datatype splits 32 decisions 154 arith add rows 121 arith bound prop 10 propagations 191 arith patches 6 conflicts 19 arith fixed eqs 22 datatype accessor ax 18 arith conflicts 1 arith assert diseq 26 datatype constructor ax 40 final checks 24 added eqs 380 del clause 94 arith ineq splits 3 arith eq adapter 61 memory 29.22 max memory 72.35 num allocs 9.36103e+09
Expand
• start[0.031s]
not
int_of_bits :var_0: + int_of_bits :var_1:)
• unroll
 expr (int_of_bits_42 b_81) expansions
• unroll
 expr (int_of_bits_42 a_80) expansions
• unroll
 expr (bad_ripple_carry_adder_72 a_80 b_81 false) expansions
• unroll
 expr (int_of_bits_42 (bad_ripple_carry_adder_72 a_80 b_81 false)) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_2205| b_81)) expansions
• Sat (Some let (a : bool list) = [] let (b : bool list) = [true] )

Happy verifying!