Verifying a Ripple-Carry Adder in Imandra

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

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

The correctness theorem we'll prove is as follows:

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

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

Building the circuit in Imandra

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

In [1]:
let xor (x : bool) (y : bool) : bool = x <> y
Out[1]:
val xor : bool -> bool -> bool = <fun>

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

 

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

In [2]:
let adder_sum a b cin =
  xor (xor a b) cin
Out[2]:
val adder_sum : bool -> bool -> bool -> bool = <fun>
In [3]:
let adder_carry_out a b cin =
  ((xor a b) && cin) || (a && b)
Out[3]:
val adder_carry_out : bool -> bool -> bool -> bool = <fun>

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

In [4]:
let args = CCList.cartesian_product [[true; false]; [true; false]; [true; false]] in
let pb b = Document.s (string_of_bool b) in
Imandra.display @@
 Document.(tbl ~headers:["a";"b";"cin";"sum";"cout"] @@
  List.map (function [a;b;cin] ->
   [pb a; pb b; pb cin; pb (adder_sum a b cin); pb (adder_carry_out a b cin)]
   | _ -> [])
   args)
Out[4]:
- : unit = ()
abcinsumcout
falsefalsefalsefalsefalse
falsefalsetruetruefalse
falsetruefalsetruefalse
falsetruetruefalsetrue
truefalsefalsetruefalse
truefalsetruefalsetrue
truetruefalsefalsetrue
truetruetruetruetrue

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

In [5]:
let rec ripple_carry_adder (a : bool list) (b : bool list) (cin : bool) : bool list =
  match a, b with
  | a1 :: a', b1 :: b' ->
    adder_sum a1 b1 cin ::
    ripple_carry_adder a' b' (adder_carry_out a1 b1 cin)
  | _ -> if cin then [cin] else []
Out[5]:
val ripple_carry_adder : bool list -> bool list -> bool -> bool list = <fun>
termination proof

Termination proof

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

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

            In [6]:
            let zero = []
            let one = [true]
            let two = [false; true]
            
            Out[6]:
            val zero : 'a list = []
            val one : bool list = [true]
            val two : bool list = [false;true]
            
            In [7]:
            ripple_carry_adder zero zero false
            
            Out[7]:
            - : bool list = []
            
            In [8]:
            ripple_carry_adder one one false
            
            Out[8]:
            - : bool list = [false;true]
            
            In [9]:
            instance (fun a b -> ripple_carry_adder a b false = [false; false; false; true])
            
            Out[9]:
            - : bool list -> bool list -> bool = <fun>
            module CX : sig val a : bool list val b : bool list end
            
            Instance (after 4 steps, 0.015s):
            let a : bool list = [true; true; true]
            let b : bool list = [true; false; false]
            
            Instance
            proof attempt
            ground_instances:4
            definitions:0
            inductions:0
            search_time:
            0.015s
            details:
            Expand
            smt_stats:
            num checks:9
            rlimit count:5367
            mk clause:238
            datatype occurs check:60
            mk bool var:227
            datatype splits:8
            decisions:57
            propagations:275
            conflicts:13
            datatype accessor ax:31
            minimized lits:3
            datatype constructor ax:37
            num allocs:11115038
            final checks:9
            added eqs:416
            del clause:90
            memory:16.810000
            max memory:16.810000
            Expand
            • start[0.015s]
                ripple_carry_adder ( :var_0: ) ( :var_1: ) false
                = [false; false; false; true]
            • unroll
              expr:
              (ripple_carry_adder_1267/client a_1281/client b_1282/client false)
              expansions:
              • unroll
                expr:
                (ripple_carry_adder_1267/client
                  (|get.::.1_443/server| a_1281/client)
                  (|get.::.1_443/server| b_1…
                expansions:
                • unroll
                  expr:
                  (ripple_carry_adder_1267/client
                    (|get.::.1_443/server| (|get.::.1_443/server| a_1281/client))
                    (|…
                  expansions:
                  • unroll
                    expr:
                    (let ((a!1 (adder_carry_out_1263/client
                                 (|get.::.0_442/server|
                                   (|get.::.…
                    expansions:
                    • Sat (Some let a : bool list = [true; true; true] let b : bool list = [true; false; false] )

                    Relating bit sequences to natural numbers

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

                    In [10]:
                    let int_of_bit (a : bool) : Z.t =
                     if a then 1 else 0
                    
                    let rec int_of_bits (a : bool list) : Z.t =
                      match a with
                       | [] -> 0
                       | a :: a' -> int_of_bit a + 2 * (int_of_bits a')
                    
                    Out[10]:
                    val int_of_bit : bool -> Z.t = <fun>
                    val int_of_bits : bool list -> Z.t = <fun>
                    
                    termination proof

                    Termination proof

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

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

                              In [11]:
                              int_of_bits [true; false]
                              
                              Out[11]:
                              - : Z.t = 1
                              
                              In [12]:
                              int_of_bits [false; true]
                              
                              Out[12]:
                              - : Z.t = 2
                              
                              In [13]:
                              int_of_bits [true; true; true; true;]
                              
                              Out[13]:
                              - : Z.t = 15
                              

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

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

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

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

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

                                                  In [16]:
                                                  theorem full_ripple_carry_adder_correct a b cin =
                                                    List.length a = List.length b ==>
                                                    int_of_bits (ripple_carry_adder a b cin) =
                                                    int_of_bits a + int_of_bits b + int_of_bit cin
                                                  [@@induct functional ripple_carry_adder]
                                                  
                                                  Out[16]:
                                                  val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
                                                    <fun>
                                                  Goal:
                                                  
                                                  List.length a = List.length b
                                                  ==> int_of_bits (ripple_carry_adder a b cin)
                                                      = int_of_bits a + int_of_bits b + int_of_bit cin.
                                                  
                                                  1 nontautological subgoal.
                                                  
                                                  We shall induct according to a scheme derived from ripple_carry_adder.
                                                  
                                                  Induction scheme:
                                                  
                                                   (not (a <> [] && b <> []) ==> φ a b cin)
                                                   && (b <> []
                                                       && (a <> []
                                                           && φ (List.tl a) (List.tl b)
                                                              (adder_carry_out (List.hd a) (List.hd b) cin))
                                                       ==> φ a b cin).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 2:
                                                  
                                                   H0. List.length a = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> [] && b <> []
                                                   C1. int_of_bits (ripple_carry_adder a b cin)
                                                       = int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                  
                                                  This simplifies, using the definitions of List.length, int_of_bits and
                                                  ripple_carry_adder to the following 4 subgoals:
                                                  
                                                  Subgoal 2.4:
                                                  
                                                   H0. 0 = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. a <> []
                                                   C2. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  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. List.length a = 0
                                                   H1. a <> []
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. b <> []
                                                   C2. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits,
                                                  and the rewrite rule List.len_zero_is_empty.
                                                  
                                                  Subgoal 2.2:
                                                  
                                                   H0. cin
                                                   H1. 0 = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  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. List.length a = 0
                                                   H1. cin
                                                   H2. a <> []
                                                  |---------------------------------------------------------------------------
                                                   C0. b <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits,
                                                  and the rewrite rule List.len_zero_is_empty.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. List.length a = List.length b
                                                   H1. b <> []
                                                   H2. a <> []
                                                   H3. List.length (List.tl a) = List.length (List.tl b)
                                                       ==> int_of_bits
                                                           (ripple_carry_adder (List.tl a) (List.tl b)
                                                            ((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
                                                  and ripple_carry_adder.
                                                  
                                                  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
                                                  and ripple_carry_adder.
                                                  
                                                  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
                                                  and ripple_carry_adder.
                                                  
                                                  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
                                                  and ripple_carry_adder.
                                                  
                                                   Rules:
                                                      (:def List.length)
                                                      (:def int_of_bits)
                                                      (:def ripple_carry_adder)
                                                      (:rw List.len_zero_is_empty)
                                                      (:fc List.len_nonnegative)
                                                      (:induct ripple_carry_adder)
                                                  
                                                  
                                                  Proved
                                                  proof
                                                  ground_instances:0
                                                  definitions:105
                                                  inductions:1
                                                  search_time:
                                                  1.219s
                                                  Expand
                                                  • start[1.219s, "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.219s, "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.216s, "1"]
                                                            let (_x_0 : bool list) = List.tl a in
                                                            let (_x_1 : bool list) = List.tl b in
                                                            let (_x_2 : bool) = List.hd a in
                                                            let (_x_3 : bool) = List.hd b in
                                                            let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in
                                                            not (List.length a = List.length b) || not (b <> []) || not (a <> [])
                                                            || not
                                                               (List.length _x_0 = List.length _x_1
                                                                ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
                                                                    = int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0))
                                                            || (int_of_bits (ripple_carry_adder a b cin)
                                                                = int_of_bits a + int_of_bits b + (if cin then 1 else 0))
                                                        • simplify
                                                          into:
                                                          let (_x_0 : bool list) = List.tl a in
                                                          let (_x_1 : bool list) = List.tl b in
                                                          let (_x_2 : bool) = not (List.length _x_0 = List.length _x_1) in
                                                          let (_x_3 : bool) = cin || _x_2 in
                                                          let (_x_4 : bool) = List.hd a in
                                                          let (_x_5 : bool) = List.hd b in
                                                          let (_x_6 : bool) = _x_4 = _x_5 in
                                                          let (_x_7 : bool) = not (b <> []) in
                                                          let (_x_8 : bool) = not (a <> []) in
                                                          let (_x_9 : int) = int_of_bits _x_0 in
                                                          let (_x_10 : int) = 2 * _x_9 in
                                                          let (_x_11 : int) = int_of_bits _x_1 in
                                                          let (_x_12 : int) = 2 * _x_11 in
                                                          let (_x_13 : bool)
                                                              = int_of_bits (ripple_carry_adder a b false) = 1 + _x_10 + _x_12
                                                          in
                                                          let (_x_14 : int) = int_of_bits (ripple_carry_adder _x_0 _x_1 cin) in
                                                          let (_x_15 : bool) = not (_x_14 = _x_9 + _x_11) in
                                                          let (_x_16 : bool) = not cin in
                                                          let (_x_17 : bool) = not (_x_14 = 1 + _x_9 + _x_11) in
                                                          let (_x_18 : bool)
                                                              = int_of_bits (ripple_carry_adder a b true) = 2 + _x_10 + _x_12
                                                          in
                                                          let (_x_19 : bool) = not _x_4 in
                                                          (_x_3 || _x_4 || _x_6 || _x_7 || _x_8 || _x_13 || _x_15)
                                                          && (_x_2 || _x_4 || _x_6 || _x_16 || _x_7 || _x_8 || _x_17 || _x_18)
                                                          && (_x_3 || _x_5 || _x_6 || _x_19 || _x_7 || _x_8 || _x_13 || _x_15)
                                                          && (_x_2 || _x_5 || _x_6 || _x_16 || _x_19 || _x_7 || _x_8 || _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, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder,
                                                           int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, List.length,
                                                           List.length, int_of_bits, int_of_bits, List.length, List.length,
                                                           int_of_bits, int_of_bits, List.length, List.length, int_of_bits,
                                                           int_of_bits, List.length, List.length, int_of_bits, int_of_bits,
                                                           int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder]
                                                          rewrite_steps:
                                                            forward_chaining:
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.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.216s, "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 (List.length a = 0) in
                                                            let (_x_5 : bool) = not _x_0 in
                                                            let (_x_6 : bool) = not cin in
                                                            (cin || _x_0 || _x_1 || _x_2) && (cin || _x_3 || _x_4 || _x_5 || _x_1)
                                                            && (_x_0 || _x_6 || _x_1 || _x_2) && (_x_3 || _x_4 || _x_6 || _x_5 || _x_1)
                                                            expansions:
                                                            [List.length, List.length, List.length, List.length, int_of_bits,
                                                             int_of_bits, ripple_carry_adder]
                                                            rewrite_steps:
                                                              forward_chaining:
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • Subproof
                                                              • Subproof
                                                              • Subproof
                                                              • Subproof

                                                      Excellent!

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

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

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

                                                      In [17]:
                                                      theorem single_adder_circuit_correct a b cin =
                                                        int_of_bit (adder_sum a b cin)
                                                          = int_of_bit a + int_of_bit b + int_of_bit cin - (2 * (int_of_bit (adder_carry_out a b cin)))
                                                      [@@rewrite]
                                                      
                                                      Out[17]:
                                                      val single_adder_circuit_correct : bool -> bool -> bool -> bool = <fun>
                                                      
                                                      Proved
                                                      proof
                                                      ground_instances:0
                                                      definitions:0
                                                      inductions:0
                                                      search_time:
                                                      0.023s
                                                      details:
                                                      Expand
                                                      smt_stats:
                                                      num checks:1
                                                      arith assert lower:60
                                                      arith tableau max rows:1
                                                      arith tableau max columns:10
                                                      arith pivots:4
                                                      rlimit count:1593
                                                      mk clause:162
                                                      mk bool var:127
                                                      arith assert upper:60
                                                      decisions:17
                                                      propagations:156
                                                      conflicts:18
                                                      minimized lits:12
                                                      arith conflicts:16
                                                      arith num rows:1
                                                      arith assert diseq:1
                                                      num allocs:2688711894
                                                      added eqs:98
                                                      del clause:138
                                                      arith eq adapter:59
                                                      time:0.011000
                                                      memory:18.500000
                                                      max memory:19.330000
                                                      Expand
                                                      • start[0.023s]
                                                          let (_x_0 : bool) = not (( :var_0: ) = ( :var_1: )) in
                                                          (if not (_x_0 = ( :var_2: )) then 1 else 0)
                                                          = ((if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0)
                                                             + (if ( :var_2: ) then 1 else 0))
                                                            - 2
                                                              * (if (_x_0 && ( :var_2: )) || (( :var_0: ) && ( :var_1: )) then 1
                                                                 else 0)
                                                      • simplify

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

                                                          Warning

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

                                                          Warning

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

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

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

                                                          In [18]:
                                                          theorem full_ripple_carry_adder_correct a b cin =
                                                            List.length a = List.length b ==>
                                                            int_of_bits (ripple_carry_adder a b cin) =
                                                            int_of_bits a + int_of_bits b + int_of_bit cin
                                                          [@@induct functional ripple_carry_adder]
                                                          [@@disable adder_sum, int_of_bit]
                                                          
                                                          Out[18]:
                                                          val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
                                                            <fun>
                                                          Goal:
                                                          
                                                          List.length a = List.length b
                                                          ==> int_of_bits (ripple_carry_adder a b cin)
                                                              = int_of_bits a + int_of_bits b + int_of_bit cin.
                                                          
                                                          1 nontautological subgoal.
                                                          
                                                          We shall induct according to a scheme derived from ripple_carry_adder.
                                                          
                                                          Induction scheme:
                                                          
                                                           (not (a <> [] && b <> []) ==> φ a b cin)
                                                           && (b <> []
                                                               && (a <> []
                                                                   && φ (List.tl a) (List.tl b)
                                                                      (adder_carry_out (List.hd a) (List.hd b) cin))
                                                               ==> φ a b cin).
                                                          
                                                          2 nontautological subgoals.
                                                          
                                                          Subgoal 2:
                                                          
                                                           H0. List.length a = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> [] && b <> []
                                                           C1. int_of_bits (ripple_carry_adder a b cin)
                                                               = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          This simplifies, using the definitions of List.length, int_of_bits and
                                                          ripple_carry_adder to the following 4 subgoals:
                                                          
                                                          Subgoal 2.4:
                                                          
                                                           H0. 0 = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. a <> []
                                                           C2. 0 = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          This simplifies, using the definition of int_of_bits, and the rewrite rule
                                                          List.len_zero_is_empty to:
                                                          
                                                          Subgoal 2.4':
                                                          
                                                           H0. b = []
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. a <> []
                                                           C2. 0 = int_of_bits b + int_of_bit false
                                                          
                                                          This simplifies, using the definition of int_of_bits to:
                                                          
                                                          Subgoal 2.4'':
                                                          
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. a <> []
                                                           C2. 0 = int_of_bit false
                                                          
                                                          But we verify Subgoal 2.4'' by recursive unrolling.
                                                          
                                                          Subgoal 2.3:
                                                          
                                                           H0. a <> []
                                                           H1. List.length a = 0
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. b <> []
                                                           C2. 0 = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          But simplification reduces this to true, using the rewrite rule
                                                          List.len_zero_is_empty.
                                                          
                                                          Subgoal 2.2:
                                                          
                                                           H0. cin
                                                           H1. 0 = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> []
                                                           C1. int_of_bit true = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          This simplifies, using the definition of int_of_bits, and the rewrite rule
                                                          List.len_zero_is_empty to:
                                                          
                                                          Subgoal 2.2':
                                                          
                                                           H0. cin
                                                           H1. b = []
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> []
                                                           C1. 0 = int_of_bits b
                                                          
                                                          But simplification reduces this to true, using the definition of int_of_bits.
                                                          
                                                          Subgoal 2.1:
                                                          
                                                           H0. cin
                                                           H1. a <> []
                                                           H2. List.length a = 0
                                                          |---------------------------------------------------------------------------
                                                           C0. b <> []
                                                           C1. int_of_bit true = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          But simplification reduces this to true, using the rewrite rule
                                                          List.len_zero_is_empty.
                                                          
                                                          Subgoal 1:
                                                          
                                                           H0. List.length a = List.length b
                                                           H1. b <> []
                                                           H2. a <> []
                                                           H3. List.length (List.tl a) = List.length (List.tl b)
                                                               ==> int_of_bits
                                                                   (ripple_carry_adder (List.tl a) (List.tl b)
                                                                    ((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
                                                          single_adder_circuit_correct.
                                                          
                                                           Rules:
                                                              (:def List.length)
                                                              (:def int_of_bits)
                                                              (:def ripple_carry_adder)
                                                              (:rw List.len_zero_is_empty)
                                                              (:rw single_adder_circuit_correct)
                                                              (:fc List.len_nonnegative)
                                                              (:induct ripple_carry_adder)
                                                          
                                                          
                                                          Proved
                                                          proof
                                                          ground_instances:0
                                                          definitions:33
                                                          inductions:1
                                                          search_time:
                                                          0.472s
                                                          details:
                                                          Expand
                                                          smt_stats:
                                                          rlimit count:17193
                                                          time:0.009000
                                                          memory:19.030000
                                                          max memory:19.430000
                                                          num allocs:4388183589.000000
                                                          Expand
                                                          • start[0.472s, "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.472s, "1"]
                                                                not (List.length a = List.length b)
                                                                || (int_of_bits (ripple_carry_adder a b cin)
                                                                    = int_of_bits a + int_of_bits b + int_of_bit cin)
                                                            • induction on (functional ripple_carry_adder)
                                                              :scheme (not (a <> [] && b <> []) ==> φ a b cin)
                                                                      && (b <> []
                                                                          && (a <> []
                                                                              && φ (List.tl a) (List.tl b)
                                                                                 (adder_carry_out (List.hd a) (List.hd b) cin))
                                                                          ==> φ a b cin)
                                                            • Split (let (_x_0 : bool) = a <> [] in
                                                                     let (_x_1 : bool) = b <> [] in
                                                                     let (_x_2 : bool) = not (List.length a = List.length b) in
                                                                     let (_x_3 : bool)
                                                                         = int_of_bits (ripple_carry_adder a b cin)
                                                                           = int_of_bits a + int_of_bits b + int_of_bit cin
                                                                     in
                                                                     let (_x_4 : bool list) = List.tl a in
                                                                     let (_x_5 : bool list) = List.tl b in
                                                                     let (_x_6 : bool) = List.hd a in
                                                                     let (_x_7 : bool) = List.hd b in
                                                                     let (_x_8 : bool) = (_x_6 && _x_7) || ((not _x_6 = _x_7) && cin) in
                                                                     ((_x_0 && _x_1) || _x_2 || _x_3)
                                                                     && (_x_2 || _x_3
                                                                         || not
                                                                            (_x_1 && _x_0
                                                                             && (not (List.length _x_4 = List.length _x_5)
                                                                                 || (int_of_bits (ripple_carry_adder _x_4 _x_5 _x_8)
                                                                                     = int_of_bits _x_4 + int_of_bits _x_5
                                                                                       + int_of_bit _x_8))))
                                                                     :cases [not (List.length a = List.length b) || (a <> [] && b <> [])
                                                                             || (int_of_bits (ripple_carry_adder a b cin)
                                                                                 = int_of_bits a + int_of_bits b + int_of_bit cin);
                                                                             let (_x_0 : bool list) = List.tl a in
                                                                             let (_x_1 : bool list) = List.tl b in
                                                                             let (_x_2 : bool) = List.hd a in
                                                                             let (_x_3 : bool) = List.hd b in
                                                                             let (_x_4 : bool)
                                                                                 = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin)
                                                                             in
                                                                             not (List.length a = List.length b) || not (b <> [])
                                                                             || not (a <> [])
                                                                             || not
                                                                                (List.length _x_0 = List.length _x_1
                                                                                 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
                                                                                     = int_of_bits _x_0 + int_of_bits _x_1
                                                                                       + int_of_bit _x_4)
                                                                             || (int_of_bits (ripple_carry_adder a b cin)
                                                                                 = int_of_bits a + int_of_bits b + int_of_bit cin)])
                                                              • subproof
                                                                let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = List.hd a in let (_x_3 : bool) = List.hd b in let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in not (List.length a = List.length b) || not (b <> []) || not (a <> []) || not (List.length _x_0 = List.length _x_1 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) = int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4) || (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + int_of_bit cin)
                                                                • start[0.471s, "1"]
                                                                    let (_x_0 : bool list) = List.tl a in
                                                                    let (_x_1 : bool list) = List.tl b in
                                                                    let (_x_2 : bool) = List.hd a in
                                                                    let (_x_3 : bool) = List.hd b in
                                                                    let (_x_4 : bool) = (_x_2 && _x_3) || ((not _x_2 = _x_3) && cin) in
                                                                    not (List.length a = List.length b) || not (b <> []) || not (a <> [])
                                                                    || not
                                                                       (List.length _x_0 = List.length _x_1
                                                                        ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4)
                                                                            = int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4)
                                                                    || (int_of_bits (ripple_carry_adder a b cin)
                                                                        = int_of_bits a + int_of_bits b + int_of_bit cin)
                                                                • simplify
                                                                  into:
                                                                  true
                                                                  expansions:
                                                                  [List.length, List.length, List.length, List.length, List.length,
                                                                   List.length, List.length, List.length, List.length, List.length,
                                                                   List.length, List.length, List.length, List.length, List.length,
                                                                   List.length, List.length, List.length, int_of_bits, int_of_bits,
                                                                   int_of_bits, ripple_carry_adder]
                                                                  rewrite_steps:
                                                                  single_adder_circuit_correct
                                                                  forward_chaining:
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.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.471s, "2"]
                                                                    not (List.length a = List.length b) || (a <> [] && b <> [])
                                                                    || (int_of_bits (ripple_carry_adder a b cin)
                                                                        = int_of_bits a + int_of_bits b + int_of_bit cin)
                                                                • simplify
                                                                  into:
                                                                  let (_x_0 : bool) = a <> [] in
                                                                  let (_x_1 : bool) = not (0 = List.length b) in
                                                                  let (_x_2 : int) = int_of_bits a + int_of_bits b + int_of_bit cin in
                                                                  let (_x_3 : bool) = 0 = _x_2 in
                                                                  let (_x_4 : bool) = b <> [] in
                                                                  let (_x_5 : bool) = not _x_0 in
                                                                  let (_x_6 : bool) = not (List.length a = 0) in
                                                                  let (_x_7 : bool) = not cin in
                                                                  let (_x_8 : bool) = int_of_bit true = _x_2 in
                                                                  (cin || _x_0 || _x_1 || _x_3) && (cin || _x_4 || _x_5 || _x_3 || _x_6)
                                                                  && (_x_0 || _x_7 || _x_1 || _x_8) && (_x_4 || _x_7 || _x_5 || _x_8 || _x_6)
                                                                  expansions:
                                                                  [List.length, List.length, List.length, List.length, int_of_bits,
                                                                   int_of_bits, ripple_carry_adder]
                                                                  rewrite_steps:
                                                                    forward_chaining:
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • Subproof
                                                                    • Subproof
                                                                    • Subproof
                                                                    • Subproof

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

                                                            Examining a flawed circuit with Imandra

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

                                                            Can you spot the error?

                                                            In [19]:
                                                            let bad_adder_sum a b cin =
                                                              not ((xor a b) || cin)
                                                            
                                                            Out[19]:
                                                            val bad_adder_sum : bool -> bool -> bool -> bool = <fun>
                                                            
                                                            In [20]:
                                                            let bad_adder_carry_out a b cin =
                                                              ((xor a b) && cin) || (a && b)
                                                            
                                                            Out[20]:
                                                            val bad_adder_carry_out : bool -> bool -> bool -> bool = <fun>
                                                            
                                                            In [21]:
                                                            verify (fun a b cin ->
                                                             int_of_bit (bad_adder_sum a b cin)
                                                                = int_of_bit a + int_of_bit b + int_of_bit cin - (2 * (int_of_bit (bad_adder_carry_out a b cin))))
                                                            
                                                            Out[21]:
                                                            - : bool -> bool -> bool -> bool = <fun>
                                                            module CX : sig val a : bool val b : bool val cin : bool end
                                                            
                                                            Counterexample (after 0 steps, 0.018s):
                                                            let a : bool = true
                                                            let b : bool = true
                                                            let cin : bool = false
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances:0
                                                            definitions:0
                                                            inductions:0
                                                            search_time:
                                                            0.018s
                                                            details:
                                                            Expand
                                                            smt_stats:
                                                            num checks:1
                                                            arith assert lower:11
                                                            arith tableau max rows:1
                                                            arith tableau max columns:10
                                                            arith pivots:3
                                                            rlimit count:948
                                                            mk clause:54
                                                            mk bool var:46
                                                            arith assert upper:13
                                                            decisions:10
                                                            propagations:31
                                                            conflicts:3
                                                            arith fixed eqs:1
                                                            arith conflicts:2
                                                            arith num rows:1
                                                            arith assert diseq:1
                                                            final checks:1
                                                            added eqs:20
                                                            del clause:8
                                                            arith eq adapter:12
                                                            time:0.009000
                                                            memory:19.220000
                                                            max memory:19.600000
                                                            num allocs:6639106235.000000
                                                            Expand
                                                            • start[0.018s]
                                                                let (_x_0 : bool) = not (( :var_0: ) = ( :var_1: )) in
                                                                (if not (_x_0 || ( :var_2: )) then 1 else 0)
                                                                = ((if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0)
                                                                   + (if ( :var_2: ) then 1 else 0))
                                                                  - 2
                                                                    * (if (_x_0 && ( :var_2: )) || (( :var_0: ) && ( :var_1: )) then 1
                                                                       else 0)
                                                            • simplify

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

                                                                Termination proof

                                                                call `bad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)` from `bad_ripple_carry_adder a b cin`
                                                                original:bad_ripple_carry_adder a b cin
                                                                sub:bad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)
                                                                original ordinal:Ordinal.Int (_cnt a)
                                                                sub ordinal:Ordinal.Int (_cnt (List.tl a))
                                                                path:[a <> [] && b <> []]
                                                                proof:
                                                                detailed proof
                                                                ground_instances:3
                                                                definitions:0
                                                                inductions:0
                                                                search_time:
                                                                0.015s
                                                                details:
                                                                Expand
                                                                smt_stats:
                                                                num checks:8
                                                                arith assert lower:8
                                                                arith tableau max rows:5
                                                                arith tableau max columns:12
                                                                arith pivots:4
                                                                rlimit count:2175
                                                                mk clause:29
                                                                datatype occurs check:25
                                                                mk bool var:79
                                                                arith assert upper:5
                                                                datatype splits:6
                                                                decisions:28
                                                                arith row summations:6
                                                                propagations:30
                                                                conflicts:9
                                                                arith fixed eqs:4
                                                                datatype accessor ax:10
                                                                arith conflicts:1
                                                                arith num rows:5
                                                                datatype constructor ax:14
                                                                final checks:6
                                                                added eqs:89
                                                                del clause:16
                                                                arith eq adapter:6
                                                                memory:19.520000
                                                                max memory:19.600000
                                                                num allocs:6754539789.000000
                                                                Expand
                                                                • start[0.015s]
                                                                    let (_x_0 : int) = count.list (const 0) a in
                                                                    let (_x_1 : bool list) = List.tl a in
                                                                    let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                    a <> [] && (b <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                                                                    ==> not (_x_1 <> [] && (List.tl b) <> [])
                                                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                • simplify
                                                                  into:
                                                                  let (_x_0 : bool list) = List.tl a in
                                                                  let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                  let (_x_2 : int) = count.list (const 0) a in
                                                                  not (_x_0 <> [] && (List.tl b) <> [])
                                                                  || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                  || not (a <> [] && b <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                  expansions:
                                                                  []
                                                                  rewrite_steps:
                                                                    forward_chaining:
                                                                    • unroll
                                                                      expr:
                                                                      (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                      (|count.list_1672/server|
                                                                                        (|g…
                                                                      expansions:
                                                                      • unroll
                                                                        expr:
                                                                        (|count.list_1672/server| (|get.::.1_1656/server| a_1657/server))
                                                                        expansions:
                                                                        • unroll
                                                                          expr:
                                                                          (|count.list_1672/server| a_1657/server)
                                                                          expansions:
                                                                          • Unsat
                                                                          In [23]:
                                                                          instance (fun a b -> int_of_bits (bad_ripple_carry_adder a b false) <> int_of_bits a + int_of_bits b)
                                                                          
                                                                          Out[23]:
                                                                          - : bool list -> bool list -> bool = <fun>
                                                                          module CX : sig val a : bool list val b : bool list end
                                                                          
                                                                          Instance (after 5 steps, 0.020s):
                                                                          let a : bool list = []
                                                                          let b : bool list = [true]
                                                                          
                                                                          Instance
                                                                          proof attempt
                                                                          ground_instances:5
                                                                          definitions:0
                                                                          inductions:0
                                                                          search_time:
                                                                          0.020s
                                                                          details:
                                                                          Expand
                                                                          smt_stats:
                                                                          arith offset eqs:2
                                                                          num checks:11
                                                                          arith assert lower:59
                                                                          arith tableau max rows:11
                                                                          arith tableau max columns:25
                                                                          arith pivots:39
                                                                          rlimit count:6641
                                                                          mk clause:163
                                                                          datatype occurs check:25
                                                                          mk bool var:306
                                                                          arith assert upper:60
                                                                          datatype splits:10
                                                                          decisions:52
                                                                          arith row summations:115
                                                                          arith bound prop:9
                                                                          propagations:130
                                                                          conflicts:10
                                                                          arith fixed eqs:30
                                                                          datatype accessor ax:15
                                                                          arith conflicts:2
                                                                          arith num rows:11
                                                                          arith assert diseq:12
                                                                          datatype constructor ax:27
                                                                          final checks:11
                                                                          added eqs:366
                                                                          del clause:75
                                                                          arith eq adapter:60
                                                                          memory:19.920000
                                                                          max memory:19.920000
                                                                          num allocs:6877920252.000000
                                                                          Expand
                                                                          • start[0.020s]
                                                                              not
                                                                              (int_of_bits (bad_ripple_carry_adder ( :var_0: ) ( :var_1: ) false)
                                                                               = int_of_bits ( :var_0: ) + int_of_bits ( :var_1: ))
                                                                          • unroll
                                                                            expr:
                                                                            (int_of_bits_1286/client b_1327/client)
                                                                            expansions:
                                                                            • unroll
                                                                              expr:
                                                                              (int_of_bits_1286/client a_1326/client)
                                                                              expansions:
                                                                              • unroll
                                                                                expr:
                                                                                (int_of_bits_1286/client
                                                                                  (bad_ripple_carry_adder_1316/client a_1326/client b_1327/client false))
                                                                                expansions:
                                                                                • unroll
                                                                                  expr:
                                                                                  (bad_ripple_carry_adder_1316/client a_1326/client b_1327/client false)
                                                                                  expansions:
                                                                                  • unroll
                                                                                    expr:
                                                                                    (int_of_bits_1286/client (|get.::.1_1704/server| b_1327/client))
                                                                                    expansions:
                                                                                    • Sat (Some let a : bool list = [] let b : bool list = [true] )

                                                                                    Happy verifying!