# 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.013s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 13 arith-conflicts 1 rlimit count 2225 mk clause 29 datatype occurs check 26 mk bool var 76 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 8.53275e+08 final checks 6 added eqs 84 del clause 14 arith eq adapter 5 arith-upper 6 memory 19.96 max memory 21.47
Expand
• start[0.013s]
let (_x_0 : int) = Ordinal.count a in
let (_x_1 : bool list) = List.tl a in
let (_x_2 : int) = Ordinal.count _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) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count 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_bool list_2456| a_2443) expansions
• unroll
 expr (|count_bool list_2456| (|get.::.1_2442| a_2443)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_bool list_2456| … 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.014s):
let (a : bool list) = [false; false; true]
let (b : bool list) = [false; false; true]

Instance
proof attempt
ground_instances4
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 9 arith-make-feasible 1 arith-max-columns 4 rlimit count 5791 mk clause 237 datatype occurs check 81 mk bool var 217 datatype splits 12 decisions 79 propagations 377 conflicts 23 datatype accessor ax 28 minimized lits 11 datatype constructor ax 33 num allocs 9.06043e+08 final checks 12 added eqs 478 del clause 85 memory 20.96 max memory 21.47
Expand
• start[0.015s]
ripple_carry_adder :var_0: :var_1: false = [false; false; false; true]
• unroll
 expr (ripple_carry_adder_25 a_37 b_38 false) expansions
• unroll
 expr (ripple_carry_adder_25 (|get.::.1_2492| a_37) (|get.::.1_2492| b_38) (adder_carry_out_21 (|get… expansions
• unroll
 expr (ripple_carry_adder_25 (|get.::.1_2492| (|get.::.1_2492| a_37)) (|get.::.1_2492| (|get.::.1_2492… expansions
• unroll
 expr (let ((a!1 (adder_carry_out_21 (|get.::.0_2491| (|get.::.1_2492| (|get.::.1_2492| a_37)… expansions
• Sat (Some let (a : bool list) = [false; false; true] let (b : bool list) = [false; 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 -> 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 (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[not (a = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 11 arith-max-columns 13 arith-conflicts 1 rlimit count 2030 arith-cheap-eqs 2 mk clause 11 datatype occurs check 36 mk bool var 54 arith-lower 5 datatype splits 6 decisions 17 propagations 10 arith-max-rows 5 conflicts 7 datatype accessor ax 5 datatype constructor ax 8 num allocs 9.53963e+08 final checks 9 added eqs 49 del clause 5 arith eq adapter 3 arith-upper 5 memory 21.27 max memory 21.47
Expand
• start[0.013s]
let (_x_0 : int) = Ordinal.count a in
let (_x_1 : bool list) = List.tl a in
let (_x_2 : int) = Ordinal.count _x_1 in
not (a = []) && _x_0 >= 0 && _x_2 >= 0
==> _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) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count a in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (a = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_bool list_2551| a_2542) expansions
• unroll
 expr (|count_bool list_2551| (|get.::.1_2541| a_2542)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_bool list_2551| … 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.029s):
let (a : bool list) =
[false; false; false; false; false; false; false; false; true]

Instance
proof attempt
ground_instances10
definitions0
inductions0
search_time
0.029s
details
Expand
smt_stats
 num checks 21 arith-make-feasible 192 arith-max-columns 43 arith-conflicts 11 rlimit count 11515 arith-gcd-calls 7 arith-cheap-eqs 16 mk clause 657 datatype occurs check 132 mk bool var 897 arith-lower 184 arith-diseq 190 datatype splits 70 decisions 152 arith-propagations 143 propagations 588 arith-bound-propagations-cheap 143 arith-max-rows 19 conflicts 71 datatype accessor ax 60 minimized lits 2 arith-bound-propagations-lp 38 datatype constructor ax 85 num allocs 1.00778e+09 final checks 42 added eqs 1082 del clause 536 arith eq adapter 198 arith-upper 197 arith-gcd-conflict 7 memory 22.13 max memory 22.13
Expand
• start[0.029s] int_of_bits :var_0: = 256
• unroll
 expr (int_of_bits_42 a_46) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_2575| a_46)) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_2575| (|get.::.1_2575| a_46))) expansions
• unroll
 expr (int_of_bits_42 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46)))) expansions
• unroll
 expr (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46)))))) (int_of_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46)))))) (let ((a!2… expansions
• unroll
 expr (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| 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:
- : 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)
&& ((a <> [] && b <> [])
&& φ (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

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

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

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. a <> []
H1. cin
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. a <> []
H2. b <> []
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. a <> []
H2. b <> []
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. a <> []
H2. b <> []
H3. cin
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. a <> []
H2. List.hd a
H3. b <> []
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. a <> []
H2. List.hd a
H3. b <> []
H4. cin
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.535s
Expand
• start[1.535s, "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.535s, "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)
&& ((a <> [] && b <> [])
&& φ (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 <> [] && b <> [] in
let (_x_1 : bool) = not (List.length a = List.length b) in
let (_x_2 : 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_3 : bool list) = List.tl a in
let (_x_4 : bool list) = List.tl b in
let (_x_5 : bool) = List.hd a in
let (_x_6 : bool) = List.hd b in
let (_x_7 : bool) = _x_5 && _x_6 || not _x_5 = _x_6 && cin in
((_x_0 || _x_1) || _x_2)
&& ((_x_1 || _x_2)
|| not
(_x_0
&& (not (List.length _x_3 = List.length _x_4)
|| int_of_bits (ripple_carry_adder _x_3 _x_4 _x_7) =
int_of_bits _x_3 + int_of_bits _x_4
+ (if _x_7 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 (a <> []))
|| not (b <> []))
|| 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 (a <> [])) || not (b <> [])) || 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.534s, "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 (a <> [])) || not (b <> []))
|| 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 (a <> []) in let (_x_8 : bool) = not (b <> []) 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) = int_of_bits (ripple_carry_adder a b true) = 2 + _x_10 + _x_12 in let (_x_18 : bool) = not (_x_14 = 1 + _x_9 + _x_11) 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_7) || _x_8) || _x_16) || _x_17) || _x_18)) && (((((((_x_3 || _x_5) || _x_6) || _x_7) || _x_19) || _x_8) || _x_13) || _x_15)) && ((((((((_x_2 || _x_5) || _x_6) || _x_7) || _x_19) || _x_8) || _x_16) || _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.534s, "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) = 0 = int_of_bits a + int_of_bits b in let (_x_2 : bool) = not (0 = List.length 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_1) || _x_5)) && (((_x_0 || _x_6) || _x_1) || _x_2)) && ((((_x_3 || _x_4) || _x_6) || _x_1) || _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.026s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 30 arith-max-columns 11 arith-conflicts 16 rlimit count 1679 mk clause 115 mk bool var 140 arith-lower 60 arith-diseq 2 decisions 15 arith-propagations 4 propagations 142 arith-bound-propagations-cheap 4 arith-max-rows 2 conflicts 16 minimized lits 22 added eqs 157 del clause 81 arith eq adapter 59 arith-upper 60 memory 56.45 max memory 61.92 num allocs 9.50105e+09
Expand
• start[0.026s]
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)
&& ((a <> [] && b <> [])
&& φ (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. a <> []
H2. b <> []
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
0.949s
details
Expand
smt_stats
 rlimit count 16719 mk bool var 1 memory 88.55 max memory 88.55 num allocs 1.16135e+10
Expand
• start[0.949s, "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.949s, "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)
&& ((a <> [] && b <> [])
&& φ (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 <> [] && b <> [] in
let (_x_1 : bool) = not (List.length a = List.length b) in
let (_x_2 : 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_3 : bool list) = List.tl a in
let (_x_4 : bool list) = List.tl b in
let (_x_5 : bool) = List.hd a in
let (_x_6 : bool) = List.hd b in
let (_x_7 : bool) = _x_5 && _x_6 || not _x_5 = _x_6 && cin in
((_x_0 || _x_1) || _x_2)
&& ((_x_1 || _x_2)
|| not
(_x_0
&& (not (List.length _x_3 = List.length _x_4)
|| int_of_bits (ripple_carry_adder _x_3 _x_4 _x_7) =
int_of_bits _x_3 + int_of_bits _x_4 + int_of_bit _x_7)))
: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 (a <> []))
|| not (b <> []))
|| 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 (a <> [])) || not (b <> [])) || 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.948s, "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 (a <> [])) || not (b <> []))
|| 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[0.948s, "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.031s):
let (a : bool) = false
let (b : bool) = false
let (cin : bool) = false

Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.031s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 13 arith-max-columns 11 arith-conflicts 6 rlimit count 1215 mk clause 88 mk bool var 82 arith-lower 29 arith-diseq 2 decisions 13 arith-propagations 5 propagations 72 arith-bound-propagations-cheap 5 arith-max-rows 2 conflicts 6 minimized lits 3 final checks 1 added eqs 75 del clause 32 arith eq adapter 28 arith-upper 27 memory 51.41 max memory 100.1 num allocs 2.0229e+10
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 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 (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.024s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 13 arith-conflicts 1 rlimit count 2225 mk clause 29 datatype occurs check 26 mk bool var 76 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 84 del clause 14 arith eq adapter 5 arith-upper 6 memory 51.77 max memory 100.1 num allocs 2.0433e+10
Expand
• start[0.024s]
let (_x_0 : int) = Ordinal.count a in
let (_x_1 : bool list) = List.tl a in
let (_x_2 : int) = Ordinal.count _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) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count 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_bool list_4301| a_4288) expansions
• unroll
 expr (|count_bool list_4301| (|get.::.1_4287| a_4288)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_bool list_4301| … 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.016s):
let (a : bool list) = []
let (b : bool list) = [true]

Instance
proof attempt
ground_instances5
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 11 arith-make-feasible 44 arith-max-columns 25 rlimit count 4645 arith-cheap-eqs 29 mk clause 180 datatype occurs check 23 mk bool var 283 arith-lower 66 arith-diseq 18 datatype splits 6 decisions 80 arith-propagations 18 propagations 168 arith-bound-propagations-cheap 18 arith-max-rows 10 conflicts 13 datatype accessor ax 7 arith-bound-propagations-lp 10 datatype constructor ax 14 final checks 9 added eqs 317 del clause 66 arith eq adapter 63 arith-upper 64 memory 52.12 max memory 100.1 num allocs 2.06499e+10
Expand
• start[0.016s]
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_4326| b_81)) expansions
• Sat (Some let (a : bool list) = [] let (b : bool list) = [true] )

Happy verifying!