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`
originalripple_carry_adder a b cin
subripple_carry_adder (List.tl a) (List.tl b) (adder_carry_out (List.hd a) (List.hd b) cin)
original ordinalOrdinal.Int (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
num checks7
arith-make-feasible7
arith-max-columns13
arith-conflicts1
rlimit count2225
mk clause29
datatype occurs check26
mk bool var76
arith-lower4
datatype splits6
decisions30
propagations28
arith-max-rows5
conflicts8
datatype accessor ax9
datatype constructor ax14
num allocs853275053
final checks6
added eqs84
del clause14
arith eq adapter5
arith-upper6
memory19.960000
max memory21.470000
Expand
  • start[0.013s]
      let (_x_0 : int) = Ordinal.count a in
      let (_x_1 : bool list) = List.tl a in
      let (_x_2 : int) = Ordinal.count _x_1 in
      (a <> [] && b <> []) && _x_0 >= 0 && _x_2 >= 0
      ==> not (_x_1 <> [] && (List.tl b) <> [])
          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : bool list) = List.tl a in
    let (_x_1 : int) = Ordinal.count _x_0 in
    let (_x_2 : int) = Ordinal.count a in
    (not (_x_0 <> [] && (List.tl b) <> [])
     || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not (((a <> [] && b <> []) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|count_`bool list`_2456| a_2443)
        expansions
        • unroll
          expr
          (|count_`bool list`_2456| (|get.::.1_2442| a_2443))
          expansions
          • unroll
            expr
            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`bool list`_2456|
                                                  …
            expansions
            • Unsat

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

            In [6]:
            let zero = []
            let one = [true]
            let two = [false; true]
            
            Out[6]:
            val zero : 'a list = []
            val one : bool list = [true]
            val two : bool list = [false; true]
            
            In [7]:
            ripple_carry_adder zero zero false
            
            Out[7]:
            - : bool list = []
            
            In [8]:
            ripple_carry_adder one one false
            
            Out[8]:
            - : bool list = [false; true]
            
            In [9]:
            instance (fun a b -> ripple_carry_adder a b false = [false; false; false; true])
            
            Out[9]:
            - : bool list -> bool list -> bool = <fun>
            module CX : sig val a : bool list val b : bool list end
            
            Instance (after 4 steps, 0.014s):
             let (a : bool list) = [false; false; true]
             let (b : bool list) = [false; false; true]
            
            Instance
            proof attempt
            ground_instances4
            definitions0
            inductions0
            search_time
            0.015s
            details
            Expand
            smt_stats
            num checks9
            arith-make-feasible1
            arith-max-columns4
            rlimit count5791
            mk clause237
            datatype occurs check81
            mk bool var217
            datatype splits12
            decisions79
            propagations377
            conflicts23
            datatype accessor ax28
            minimized lits11
            datatype constructor ax33
            num allocs906043306
            final checks12
            added eqs478
            del clause85
            memory20.960000
            max memory21.470000
            Expand
            • start[0.015s]
                ripple_carry_adder :var_0: :var_1: false = [false; false; false; true]
            • unroll
              expr
              (ripple_carry_adder_25 a_37 b_38 false)
              expansions
              • unroll
                expr
                (ripple_carry_adder_25
                  (|get.::.1_2492| a_37)
                  (|get.::.1_2492| b_38)
                  (adder_carry_out_21 (|get…
                expansions
                • unroll
                  expr
                  (ripple_carry_adder_25
                    (|get.::.1_2492| (|get.::.1_2492| a_37))
                    (|get.::.1_2492| (|get.::.1_2492…
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (adder_carry_out_21
                                 (|get.::.0_2491| (|get.::.1_2492| (|get.::.1_2492| a_37)…
                    expansions
                    • Sat (Some let (a : bool list) = [false; false; true] let (b : bool list) = [false; false; true] )

                    Relating bit sequences to natural numbers

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

                    In [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 -> int = <fun>
                    val int_of_bits : bool list -> int = <fun>
                    
                    termination proof

                    Termination proof

                    call `int_of_bits (List.tl a)` from `int_of_bits a`
                    originalint_of_bits a
                    subint_of_bits (List.tl a)
                    original ordinalOrdinal.Int (Ordinal.count a)
                    sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
                    path[not (a = [])]
                    proof
                    detailed proof
                    ground_instances3
                    definitions0
                    inductions0
                    search_time
                    0.013s
                    details
                    Expand
                    smt_stats
                    num checks7
                    arith-make-feasible11
                    arith-max-columns13
                    arith-conflicts1
                    rlimit count2030
                    arith-cheap-eqs2
                    mk clause11
                    datatype occurs check36
                    mk bool var54
                    arith-lower5
                    datatype splits6
                    decisions17
                    propagations10
                    arith-max-rows5
                    conflicts7
                    datatype accessor ax5
                    datatype constructor ax8
                    num allocs953962553
                    final checks9
                    added eqs49
                    del clause5
                    arith eq adapter3
                    arith-upper5
                    memory21.270000
                    max memory21.470000
                    Expand
                    • start[0.013s]
                        let (_x_0 : int) = Ordinal.count a in
                        let (_x_1 : bool list) = List.tl a in
                        let (_x_2 : int) = Ordinal.count _x_1 in
                        not (a = []) && _x_0 >= 0 && _x_2 >= 0
                        ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                    • simplify
                      into
                      let (_x_0 : bool list) = List.tl a in
                      let (_x_1 : int) = Ordinal.count _x_0 in
                      let (_x_2 : int) = Ordinal.count a in
                      (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                      || not ((not (a = []) && _x_2 >= 0) && _x_1 >= 0)
                      expansions
                      []
                      rewrite_steps
                        forward_chaining
                        • unroll
                          expr
                          (|count_`bool list`_2551| a_2542)
                          expansions
                          • unroll
                            expr
                            (|count_`bool list`_2551| (|get.::.1_2541| a_2542))
                            expansions
                            • unroll
                              expr
                              (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`bool list`_2551|
                                                                    …
                              expansions
                              • Unsat

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

                              In [11]:
                              int_of_bits [true; false]
                              
                              Out[11]:
                              - : int = 1
                              
                              In [12]:
                              int_of_bits [false; true]
                              
                              Out[12]:
                              - : int = 2
                              
                              In [13]:
                              int_of_bits [true; true; true; true;]
                              
                              Out[13]:
                              - : int = 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.029s):
                               let (a : bool list) =
                                [false; false; false; false; false; false; false; false; true]
                              
                              Instance
                              proof attempt
                              ground_instances10
                              definitions0
                              inductions0
                              search_time
                              0.029s
                              details
                              Expand
                              smt_stats
                              num checks21
                              arith-make-feasible192
                              arith-max-columns43
                              arith-conflicts11
                              rlimit count11515
                              arith-gcd-calls7
                              arith-cheap-eqs16
                              mk clause657
                              datatype occurs check132
                              mk bool var897
                              arith-lower184
                              arith-diseq190
                              datatype splits70
                              decisions152
                              arith-propagations143
                              propagations588
                              arith-bound-propagations-cheap143
                              arith-max-rows19
                              conflicts71
                              datatype accessor ax60
                              minimized lits2
                              arith-bound-propagations-lp38
                              datatype constructor ax85
                              num allocs1007780545
                              final checks42
                              added eqs1082
                              del clause536
                              arith eq adapter198
                              arith-upper197
                              arith-gcd-conflict7
                              memory22.130000
                              max memory22.130000
                              Expand
                              • start[0.029s] int_of_bits :var_0: = 256
                              • unroll
                                expr
                                (int_of_bits_42 a_46)
                                expansions
                                • unroll
                                  expr
                                  (int_of_bits_42 (|get.::.1_2575| a_46))
                                  expansions
                                  • unroll
                                    expr
                                    (int_of_bits_42 (|get.::.1_2575| (|get.::.1_2575| a_46)))
                                    expansions
                                    • unroll
                                      expr
                                      (int_of_bits_42 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))))
                                          (int_of_…
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))))
                                            (int_of_…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))))
                                              (int_of_…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))))
                                                (int_of_…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))))
                                                (let ((a!2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| (|get.::.1_2575| a_46))))))
                                                  (let ((a!2…
                                                  expansions
                                                  • Sat (Some let (a : bool list) = [false; false; false; false; false; false; false; false; true] )
                                                  In [15]:
                                                  int_of_bits (ripple_carry_adder CX.a CX.a false)
                                                  
                                                  Out[15]:
                                                  - : int = 512
                                                  

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

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

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

                                                  In [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)
                                                   && ((a <> [] && b <> [])
                                                       && φ (List.tl a) (List.tl b)
                                                          (adder_carry_out (List.hd a) (List.hd b) cin)
                                                       ==> φ a b cin).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 2:
                                                  
                                                   H0. List.length a = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> [] && b <> []
                                                   C1. int_of_bits (ripple_carry_adder a b cin) =
                                                       int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                  
                                                  This simplifies, using the definitions of List.length, int_of_bits and
                                                  ripple_carry_adder to the following 4 subgoals:
                                                  
                                                  Subgoal 2.4:
                                                  
                                                   H0. 0 = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. a <> []
                                                   C2. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits,
                                                  and the rewrite rule List.len_zero_is_empty.
                                                  
                                                  Subgoal 2.3:
                                                  
                                                   H0. a <> []
                                                   H1. List.length a = 0
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. b <> []
                                                   C2. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the rewrite rule
                                                  List.len_zero_is_empty.
                                                  
                                                  Subgoal 2.2:
                                                  
                                                   H0. cin
                                                   H1. 0 = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits,
                                                  and the rewrite rule List.len_zero_is_empty.
                                                  
                                                  Subgoal 2.1:
                                                  
                                                   H0. a <> []
                                                   H1. cin
                                                   H2. List.length a = 0
                                                  |---------------------------------------------------------------------------
                                                   C0. b <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the rewrite rule
                                                  List.len_zero_is_empty.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. List.length a = List.length b
                                                   H1. a <> []
                                                   H2. b <> []
                                                   H3. List.length (List.tl a) = List.length (List.tl b)
                                                       ==> int_of_bits
                                                           (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. a <> []
                                                   H2. b <> []
                                                   H3. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. List.hd a
                                                   C2. List.hd a = List.hd b
                                                   C3. int_of_bits (ripple_carry_adder a b false) =
                                                       1 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                  Subgoal 1.3:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. a <> []
                                                   H2. b <> []
                                                   H3. cin
                                                   H4. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       1 + int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. List.hd a
                                                   C1. List.hd a = List.hd b
                                                   C2. int_of_bits (ripple_carry_adder a b true) =
                                                       2 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                  Subgoal 1.2:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. a <> []
                                                   H2. List.hd a
                                                   H3. b <> []
                                                   H4. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. List.hd b
                                                   C2. List.hd a = List.hd b
                                                   C3. int_of_bits (ripple_carry_adder a b false) =
                                                       1 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                  Subgoal 1.1:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. a <> []
                                                   H2. List.hd a
                                                   H3. b <> []
                                                   H4. cin
                                                   H5. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       1 + int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. List.hd b
                                                   C1. List.hd a = List.hd b
                                                   C2. int_of_bits (ripple_carry_adder a b true) =
                                                       2 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  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_instances0
                                                  definitions63
                                                  inductions1
                                                  search_time
                                                  1.535s
                                                  Expand
                                                  • start[1.535s, "Goal"]
                                                      List.length :var_0: = List.length :var_1:
                                                      ==> int_of_bits (ripple_carry_adder :var_0: :var_1: :var_2:) =
                                                          int_of_bits :var_0: + int_of_bits :var_1: + (if :var_2: then 1 else 0)
                                                  • subproof

                                                    not (List.length a = List.length b) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                    • start[1.535s, "1"]
                                                        not (List.length a = List.length b)
                                                        || int_of_bits (ripple_carry_adder a b cin) =
                                                           int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                    • induction on (functional ripple_carry_adder)
                                                      :scheme (not (a <> [] && b <> []) ==> φ a b cin)
                                                              && ((a <> [] && b <> [])
                                                                  && φ (List.tl a) (List.tl b)
                                                                     (adder_carry_out (List.hd a) (List.hd b) cin)
                                                                  ==> φ a b cin)
                                                    • Split (let (_x_0 : bool) = a <> [] && b <> [] in
                                                             let (_x_1 : bool) = not (List.length a = List.length b) in
                                                             let (_x_2 : bool)
                                                                 = int_of_bits (ripple_carry_adder a b cin) =
                                                                   int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                             in
                                                             let (_x_3 : bool list) = List.tl a in
                                                             let (_x_4 : bool list) = List.tl b in
                                                             let (_x_5 : bool) = List.hd a in
                                                             let (_x_6 : bool) = List.hd b in
                                                             let (_x_7 : bool) = _x_5 && _x_6 || not _x_5 = _x_6 && cin in
                                                             ((_x_0 || _x_1) || _x_2)
                                                             && ((_x_1 || _x_2)
                                                                 || not
                                                                    (_x_0
                                                                     && (not (List.length _x_3 = List.length _x_4)
                                                                         || int_of_bits (ripple_carry_adder _x_3 _x_4 _x_7) =
                                                                            int_of_bits _x_3 + int_of_bits _x_4
                                                                            + (if _x_7 then 1 else 0))))
                                                             :cases [(not (List.length a = List.length b) || a <> [] && b <> [])
                                                                     || int_of_bits (ripple_carry_adder a b cin) =
                                                                        int_of_bits a + int_of_bits b + (if cin then 1 else 0);
                                                                     let (_x_0 : bool list) = List.tl a in
                                                                     let (_x_1 : bool list) = List.tl b in
                                                                     let (_x_2 : bool) = List.hd a in
                                                                     let (_x_3 : bool) = List.hd b in
                                                                     let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in
                                                                     (((not (List.length a = List.length b) || not (a <> []))
                                                                       || not (b <> []))
                                                                      || not
                                                                         (List.length _x_0 = List.length _x_1
                                                                          ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) =
                                                                              int_of_bits _x_0 + int_of_bits _x_1
                                                                              + (if _x_4 then 1 else 0)))
                                                                     || int_of_bits (ripple_carry_adder a b cin) =
                                                                        int_of_bits a + int_of_bits b + (if cin then 1 else 0)])
                                                      • subproof
                                                        let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = List.hd a in let (_x_3 : bool) = List.hd b in let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in (((not (List.length a = List.length b) || not (a <> [])) || not (b <> [])) || not (List.length _x_0 = List.length _x_1 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) = int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0))) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                        • start[1.534s, "1"]
                                                            let (_x_0 : bool list) = List.tl a in
                                                            let (_x_1 : bool list) = List.tl b in
                                                            let (_x_2 : bool) = List.hd a in
                                                            let (_x_3 : bool) = List.hd b in
                                                            let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in
                                                            (((not (List.length a = List.length b) || not (a <> [])) || not (b <> []))
                                                             || not
                                                                (List.length _x_0 = List.length _x_1
                                                                 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) =
                                                                     int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0)))
                                                            || int_of_bits (ripple_carry_adder a b cin) =
                                                               int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                        • simplify
                                                          into
                                                          let (_x_0 : bool list) = List.tl a in
                                                          let (_x_1 : bool list) = List.tl b in
                                                          let (_x_2 : bool) = not (List.length _x_0 = List.length _x_1) in
                                                          let (_x_3 : bool) = cin || _x_2 in
                                                          let (_x_4 : bool) = List.hd a in
                                                          let (_x_5 : bool) = List.hd b in
                                                          let (_x_6 : bool) = _x_4 = _x_5 in
                                                          let (_x_7 : bool) = not (a <> []) in
                                                          let (_x_8 : bool) = not (b <> []) in
                                                          let (_x_9 : int) = int_of_bits _x_0 in
                                                          let (_x_10 : int) = 2 * _x_9 in
                                                          let (_x_11 : int) = int_of_bits _x_1 in
                                                          let (_x_12 : int) = 2 * _x_11 in
                                                          let (_x_13 : bool)
                                                              = int_of_bits (ripple_carry_adder a b false) = 1 + _x_10 + _x_12
                                                          in
                                                          let (_x_14 : int) = int_of_bits (ripple_carry_adder _x_0 _x_1 cin) in
                                                          let (_x_15 : bool) = not (_x_14 = _x_9 + _x_11) in
                                                          let (_x_16 : bool) = not cin in
                                                          let (_x_17 : bool)
                                                              = int_of_bits (ripple_carry_adder a b true) = 2 + _x_10 + _x_12
                                                          in
                                                          let (_x_18 : bool) = not (_x_14 = 1 + _x_9 + _x_11) in
                                                          let (_x_19 : bool) = not _x_4 in
                                                          ((((((((_x_3 || _x_4) || _x_6) || _x_7) || _x_8) || _x_13) || _x_15)
                                                            && (((((((_x_2 || _x_4) || _x_6) || _x_7) || _x_8) || _x_16) || _x_17)
                                                                || _x_18))
                                                           && (((((((_x_3 || _x_5) || _x_6) || _x_7) || _x_19) || _x_8) || _x_13)
                                                               || _x_15))
                                                          && ((((((((_x_2 || _x_5) || _x_6) || _x_7) || _x_19) || _x_8) || _x_16)
                                                               || _x_17)
                                                              || _x_18)
                                                          expansions
                                                          [List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder,
                                                           int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, List.length,
                                                           List.length, int_of_bits, int_of_bits, List.length, List.length,
                                                           int_of_bits, int_of_bits, List.length, List.length, int_of_bits,
                                                           int_of_bits, List.length, List.length, int_of_bits, int_of_bits,
                                                           int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder]
                                                          rewrite_steps
                                                            forward_chaining
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • 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.534s, "2"]
                                                              (not (List.length a = List.length b) || a <> [] && b <> [])
                                                              || int_of_bits (ripple_carry_adder a b cin) =
                                                                 int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                          • simplify
                                                            into
                                                            let (_x_0 : bool) = a <> [] in
                                                            let (_x_1 : bool) = 0 = int_of_bits a + int_of_bits b in
                                                            let (_x_2 : bool) = not (0 = List.length b) in
                                                            let (_x_3 : bool) = b <> [] in
                                                            let (_x_4 : bool) = not _x_0 in
                                                            let (_x_5 : bool) = not (List.length a = 0) in
                                                            let (_x_6 : bool) = not cin in
                                                            (((((cin || _x_0) || _x_1) || _x_2)
                                                              && ((((cin || _x_3) || _x_4) || _x_1) || _x_5))
                                                             && (((_x_0 || _x_6) || _x_1) || _x_2))
                                                            && ((((_x_3 || _x_4) || _x_6) || _x_1) || _x_5)
                                                            expansions
                                                            [List.length, List.length, List.length, List.length, int_of_bits,
                                                             int_of_bits, ripple_carry_adder]
                                                            rewrite_steps
                                                              forward_chaining
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • 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_instances0
                                                      definitions0
                                                      inductions0
                                                      search_time
                                                      0.026s
                                                      details
                                                      Expand
                                                      smt_stats
                                                      num checks1
                                                      arith-make-feasible30
                                                      arith-max-columns11
                                                      arith-conflicts16
                                                      rlimit count1679
                                                      mk clause115
                                                      mk bool var140
                                                      arith-lower60
                                                      arith-diseq2
                                                      decisions15
                                                      arith-propagations4
                                                      propagations142
                                                      arith-bound-propagations-cheap4
                                                      arith-max-rows2
                                                      conflicts16
                                                      minimized lits22
                                                      added eqs157
                                                      del clause81
                                                      arith eq adapter59
                                                      arith-upper60
                                                      memory56.450000
                                                      max memory61.920000
                                                      num allocs9501048525.000000
                                                      Expand
                                                      • start[0.026s]
                                                          let (_x_0 : bool) = not (:var_0: = :var_1:) in
                                                          (if not (_x_0 = :var_2:) then 1 else 0) =
                                                          ((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0)
                                                           + (if :var_2: then 1 else 0))
                                                          - (2 * (if _x_0 && :var_2: || :var_0: && :var_1: then 1 else 0))
                                                      • simplify

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

                                                          Warning

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

                                                          Warning

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

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

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

                                                          In [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)
                                                           && ((a <> [] && b <> [])
                                                               && φ (List.tl a) (List.tl b)
                                                                  (adder_carry_out (List.hd a) (List.hd b) cin)
                                                               ==> φ a b cin).
                                                          
                                                          2 nontautological subgoals.
                                                          
                                                          Subgoal 2:
                                                          
                                                           H0. List.length a = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> [] && b <> []
                                                           C1. int_of_bits (ripple_carry_adder a b cin) =
                                                               int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          This simplifies, using the definitions of List.length, int_of_bits and
                                                          ripple_carry_adder to the following 4 subgoals:
                                                          
                                                          Subgoal 2.4:
                                                          
                                                           H0. 0 = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. a <> []
                                                           C2. 0 = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          This simplifies, using the definition of int_of_bits, and the rewrite rule
                                                          List.len_zero_is_empty to:
                                                          
                                                          Subgoal 2.4':
                                                          
                                                           H0. b = []
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. a <> []
                                                           C2. 0 = int_of_bit false
                                                          
                                                          This simplifies to:
                                                          
                                                          Subgoal 2.4'':
                                                          
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. a <> []
                                                           C2. 0 = int_of_bit false
                                                          
                                                          But we verify Subgoal 2.4'' by recursive unrolling.
                                                          
                                                          Subgoal 2.3:
                                                          
                                                           H0. a <> []
                                                           H1. List.length a = 0
                                                          |---------------------------------------------------------------------------
                                                           C0. cin
                                                           C1. b <> []
                                                           C2. 0 = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          But simplification reduces this to true, using the rewrite rule
                                                          List.len_zero_is_empty.
                                                          
                                                          Subgoal 2.2:
                                                          
                                                           H0. cin
                                                           H1. 0 = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> []
                                                           C1. int_of_bit true = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          But simplification reduces this to true, using the definition of int_of_bits,
                                                          and the rewrite rule List.len_zero_is_empty.
                                                          
                                                          Subgoal 2.1:
                                                          
                                                           H0. cin
                                                           H1. a <> []
                                                           H2. List.length a = 0
                                                          |---------------------------------------------------------------------------
                                                           C0. b <> []
                                                           C1. int_of_bit true = int_of_bits a + int_of_bits b + int_of_bit cin
                                                          
                                                          But simplification reduces this to true, using the rewrite rule
                                                          List.len_zero_is_empty.
                                                          
                                                          Subgoal 1:
                                                          
                                                           H0. List.length a = List.length b
                                                           H1. a <> []
                                                           H2. b <> []
                                                           H3. List.length (List.tl a) = List.length (List.tl b)
                                                               ==> int_of_bits
                                                                   (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_instances0
                                                          definitions39
                                                          inductions1
                                                          search_time
                                                          0.949s
                                                          details
                                                          Expand
                                                          smt_stats
                                                          rlimit count16719
                                                          mk bool var1
                                                          memory88.550000
                                                          max memory88.550000
                                                          num allocs11613451303.000000
                                                          Expand
                                                          • start[0.949s, "Goal"]
                                                              List.length :var_0: = List.length :var_1:
                                                              ==> int_of_bits (ripple_carry_adder :var_0: :var_1: :var_2:) =
                                                                  int_of_bits :var_0: + int_of_bits :var_1: + int_of_bit :var_2:
                                                          • subproof

                                                            not (List.length a = List.length b) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + int_of_bit cin
                                                            • start[0.949s, "1"]
                                                                not (List.length a = List.length b)
                                                                || int_of_bits (ripple_carry_adder a b cin) =
                                                                   int_of_bits a + int_of_bits b + int_of_bit cin
                                                            • induction on (functional ripple_carry_adder)
                                                              :scheme (not (a <> [] && b <> []) ==> φ a b cin)
                                                                      && ((a <> [] && b <> [])
                                                                          && φ (List.tl a) (List.tl b)
                                                                             (adder_carry_out (List.hd a) (List.hd b) cin)
                                                                          ==> φ a b cin)
                                                            • Split (let (_x_0 : bool) = a <> [] && b <> [] in
                                                                     let (_x_1 : bool) = not (List.length a = List.length b) in
                                                                     let (_x_2 : bool)
                                                                         = int_of_bits (ripple_carry_adder a b cin) =
                                                                           int_of_bits a + int_of_bits b + int_of_bit cin
                                                                     in
                                                                     let (_x_3 : bool list) = List.tl a in
                                                                     let (_x_4 : bool list) = List.tl b in
                                                                     let (_x_5 : bool) = List.hd a in
                                                                     let (_x_6 : bool) = List.hd b in
                                                                     let (_x_7 : bool) = _x_5 && _x_6 || not _x_5 = _x_6 && cin in
                                                                     ((_x_0 || _x_1) || _x_2)
                                                                     && ((_x_1 || _x_2)
                                                                         || not
                                                                            (_x_0
                                                                             && (not (List.length _x_3 = List.length _x_4)
                                                                                 || int_of_bits (ripple_carry_adder _x_3 _x_4 _x_7) =
                                                                                    int_of_bits _x_3 + int_of_bits _x_4 + int_of_bit _x_7)))
                                                                     :cases [(not (List.length a = List.length b) || a <> [] && b <> [])
                                                                             || int_of_bits (ripple_carry_adder a b cin) =
                                                                                int_of_bits a + int_of_bits b + int_of_bit cin;
                                                                             let (_x_0 : bool list) = List.tl a in
                                                                             let (_x_1 : bool list) = List.tl b in
                                                                             let (_x_2 : bool) = List.hd a in
                                                                             let (_x_3 : bool) = List.hd b in
                                                                             let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in
                                                                             (((not (List.length a = List.length b) || not (a <> []))
                                                                               || not (b <> []))
                                                                              || not
                                                                                 (List.length _x_0 = List.length _x_1
                                                                                  ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) =
                                                                                      int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4))
                                                                             || int_of_bits (ripple_carry_adder a b cin) =
                                                                                int_of_bits a + int_of_bits b + int_of_bit cin])
                                                              • subproof
                                                                let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = List.hd a in let (_x_3 : bool) = List.hd b in let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in (((not (List.length a = List.length b) || not (a <> [])) || not (b <> [])) || not (List.length _x_0 = List.length _x_1 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) = int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4)) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + int_of_bit cin
                                                                • start[0.948s, "1"]
                                                                    let (_x_0 : bool list) = List.tl a in
                                                                    let (_x_1 : bool list) = List.tl b in
                                                                    let (_x_2 : bool) = List.hd a in
                                                                    let (_x_3 : bool) = List.hd b in
                                                                    let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in
                                                                    (((not (List.length a = List.length b) || not (a <> [])) || not (b <> []))
                                                                     || not
                                                                        (List.length _x_0 = List.length _x_1
                                                                         ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) =
                                                                             int_of_bits _x_0 + int_of_bits _x_1 + int_of_bit _x_4))
                                                                    || int_of_bits (ripple_carry_adder a b cin) =
                                                                       int_of_bits a + int_of_bits b + int_of_bit cin
                                                                • simplify
                                                                  into
                                                                  true
                                                                  expansions
                                                                  [List.length, List.length, List.length, List.length, List.length,
                                                                   List.length, List.length, List.length, int_of_bits, int_of_bits,
                                                                   int_of_bits, ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits,
                                                                   ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits,
                                                                   ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits,
                                                                   ripple_carry_adder, int_of_bits, int_of_bits, int_of_bits,
                                                                   ripple_carry_adder]
                                                                  rewrite_steps
                                                                  • single_adder_circuit_correct
                                                                  • single_adder_circuit_correct
                                                                  • single_adder_circuit_correct
                                                                  • single_adder_circuit_correct
                                                                  • 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
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • 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.948s, "2"]
                                                                    (not (List.length a = List.length b) || a <> [] && b <> [])
                                                                    || int_of_bits (ripple_carry_adder a b cin) =
                                                                       int_of_bits a + int_of_bits b + int_of_bit cin
                                                                • simplify
                                                                  into
                                                                  let (_x_0 : bool) = a <> [] in
                                                                  let (_x_1 : int) = int_of_bits a + int_of_bits b + int_of_bit cin in
                                                                  let (_x_2 : bool) = 0 = _x_1 in
                                                                  let (_x_3 : bool) = not (0 = List.length b) in
                                                                  let (_x_4 : bool) = b <> [] in
                                                                  let (_x_5 : bool) = not _x_0 in
                                                                  let (_x_6 : bool) = not (List.length a = 0) in
                                                                  let (_x_7 : bool) = not cin in
                                                                  let (_x_8 : bool) = int_of_bit true = _x_1 in
                                                                  (((((cin || _x_0) || _x_2) || _x_3)
                                                                    && ((((cin || _x_4) || _x_5) || _x_2) || _x_6))
                                                                   && (((_x_0 || _x_7) || _x_8) || _x_3))
                                                                  && ((((_x_4 || _x_7) || _x_5) || _x_8) || _x_6)
                                                                  expansions
                                                                  [List.length, List.length, List.length, List.length, int_of_bits,
                                                                   int_of_bits, ripple_carry_adder]
                                                                  rewrite_steps
                                                                    forward_chaining
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • List.len_nonnegative
                                                                    • 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.031s):
                                                             let (a : bool) = false
                                                             let (b : bool) = false
                                                             let (cin : bool) = false
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances0
                                                            definitions0
                                                            inductions0
                                                            search_time
                                                            0.031s
                                                            details
                                                            Expand
                                                            smt_stats
                                                            num checks1
                                                            arith-make-feasible13
                                                            arith-max-columns11
                                                            arith-conflicts6
                                                            rlimit count1215
                                                            mk clause88
                                                            mk bool var82
                                                            arith-lower29
                                                            arith-diseq2
                                                            decisions13
                                                            arith-propagations5
                                                            propagations72
                                                            arith-bound-propagations-cheap5
                                                            arith-max-rows2
                                                            conflicts6
                                                            minimized lits3
                                                            final checks1
                                                            added eqs75
                                                            del clause32
                                                            arith eq adapter28
                                                            arith-upper27
                                                            memory51.410000
                                                            max memory100.100000
                                                            num allocs20229031632.000000
                                                            Expand
                                                            • start[0.031s]
                                                                let (_x_0 : bool) = not (:var_0: = :var_1:) in
                                                                (if not (_x_0 || :var_2:) then 1 else 0) =
                                                                ((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0)
                                                                 + (if :var_2: then 1 else 0))
                                                                - (2 * (if _x_0 && :var_2: || :var_0: && :var_1: then 1 else 0))
                                                            • simplify

                                                              into
                                                              let (_x_0 : bool) = not :var_0: = :var_1: in
                                                              (if _x_0 || :var_2: then 0 else 1) =
                                                              (if :var_0: then 1 else 0) + (if :var_1: then 1 else 0)
                                                              + (if :var_2: then 1 else 0)
                                                              + -2 * (if :var_0: && :var_1: || _x_0 && :var_2: then 1 else 0)
                                                              expansions
                                                              []
                                                              rewrite_steps
                                                                forward_chaining
                                                                • Sat (Some let (a : bool) = false let (b : bool) = false let (cin : bool) = false )
                                                                In [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`
                                                                originalbad_ripple_carry_adder a b cin
                                                                subbad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)
                                                                original ordinalOrdinal.Int (Ordinal.count a)
                                                                sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
                                                                path[a <> [] && b <> []]
                                                                proof
                                                                detailed proof
                                                                ground_instances3
                                                                definitions0
                                                                inductions0
                                                                search_time
                                                                0.024s
                                                                details
                                                                Expand
                                                                smt_stats
                                                                num checks7
                                                                arith-make-feasible7
                                                                arith-max-columns13
                                                                arith-conflicts1
                                                                rlimit count2225
                                                                mk clause29
                                                                datatype occurs check26
                                                                mk bool var76
                                                                arith-lower4
                                                                datatype splits6
                                                                decisions30
                                                                propagations28
                                                                arith-max-rows5
                                                                conflicts8
                                                                datatype accessor ax9
                                                                datatype constructor ax14
                                                                final checks6
                                                                added eqs84
                                                                del clause14
                                                                arith eq adapter5
                                                                arith-upper6
                                                                memory51.770000
                                                                max memory100.100000
                                                                num allocs20433002211.000000
                                                                Expand
                                                                • start[0.024s]
                                                                    let (_x_0 : int) = Ordinal.count a in
                                                                    let (_x_1 : bool list) = List.tl a in
                                                                    let (_x_2 : int) = Ordinal.count _x_1 in
                                                                    (a <> [] && b <> []) && _x_0 >= 0 && _x_2 >= 0
                                                                    ==> not (_x_1 <> [] && (List.tl b) <> [])
                                                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                • simplify
                                                                  into
                                                                  let (_x_0 : bool list) = List.tl a in
                                                                  let (_x_1 : int) = Ordinal.count _x_0 in
                                                                  let (_x_2 : int) = Ordinal.count a in
                                                                  (not (_x_0 <> [] && (List.tl b) <> [])
                                                                   || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                  || not (((a <> [] && b <> []) && _x_2 >= 0) && _x_1 >= 0)
                                                                  expansions
                                                                  []
                                                                  rewrite_steps
                                                                    forward_chaining
                                                                    • unroll
                                                                      expr
                                                                      (|count_`bool list`_4301| a_4288)
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|count_`bool list`_4301| (|get.::.1_4287| a_4288))
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`bool list`_4301|
                                                                                                                …
                                                                          expansions
                                                                          • Unsat

                                                                          In [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.016s):
                                                                           let (a : bool list) = []
                                                                           let (b : bool list) = [true]
                                                                          
                                                                          Instance
                                                                          proof attempt
                                                                          ground_instances5
                                                                          definitions0
                                                                          inductions0
                                                                          search_time
                                                                          0.016s
                                                                          details
                                                                          Expand
                                                                          smt_stats
                                                                          num checks11
                                                                          arith-make-feasible44
                                                                          arith-max-columns25
                                                                          rlimit count4645
                                                                          arith-cheap-eqs29
                                                                          mk clause180
                                                                          datatype occurs check23
                                                                          mk bool var283
                                                                          arith-lower66
                                                                          arith-diseq18
                                                                          datatype splits6
                                                                          decisions80
                                                                          arith-propagations18
                                                                          propagations168
                                                                          arith-bound-propagations-cheap18
                                                                          arith-max-rows10
                                                                          conflicts13
                                                                          datatype accessor ax7
                                                                          arith-bound-propagations-lp10
                                                                          datatype constructor ax14
                                                                          final checks9
                                                                          added eqs317
                                                                          del clause66
                                                                          arith eq adapter63
                                                                          arith-upper64
                                                                          memory52.120000
                                                                          max memory100.100000
                                                                          num allocs20649927236.000000
                                                                          Expand
                                                                          • start[0.016s]
                                                                              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_42 b_81)
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (int_of_bits_42 a_80)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (bad_ripple_carry_adder_72 a_80 b_81 false)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (int_of_bits_42 (bad_ripple_carry_adder_72 a_80 b_81 false))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (int_of_bits_42 (|get.::.1_4326| b_81))
                                                                                    expansions
                                                                                    • Sat (Some let (a : bool list) = [] let (b : bool list) = [true] )

                                                                                    Happy verifying!