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[b <> [] && a <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
num checks8
arith assert lower9
arith pivots4
rlimit count2128
mk clause30
datatype occurs check22
mk bool var84
arith assert upper4
datatype splits6
decisions28
arith add rows6
propagations30
conflicts9
arith fixed eqs4
datatype accessor ax10
arith conflicts1
datatype constructor ax14
num allocs1365201036
final checks6
added eqs87
del clause17
arith eq adapter6
memory16.080000
max memory18.750000
Expand
  • start[0.015s]
      (b <> [] && a <> [])
      && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
      ==> not ((List.tl b) <> [] && (List.tl a) <> [])
          || Ordinal.Int (Ordinal.count (List.tl a)) Ordinal.<<
             Ordinal.Int (Ordinal.count a)
  • simplify
    into
    (not
     (((b <> [] && a <> []) && Ordinal.count a >= 0)
      && Ordinal.count (List.tl a) >= 0)
     || not ((List.tl b) <> [] && (List.tl a) <> []))
    || Ordinal.Int (Ordinal.count (List.tl a)) Ordinal.<<
       Ordinal.Int (Ordinal.count a)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_121| (|Ordinal.Int_112|
                            (|count_`bool list`_2472| (|get.::.1_2458| …
        expansions
        • unroll
          expr
          (|count_`bool list`_2472| (|get.::.1_2458| a_2459))
          expansions
          • unroll
            expr
            (|count_`bool list`_2472| a_2459)
            expansions
            • unsat
              (let ((a!1 (= (|count_`bool list`_2472| a_2459)
                            (+ 1 (|count_`bool list`_2472| (|get.:…

            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.018s):
             let a = [true; true; false]
             let b = [true; false; true]
            
            Instance
            proof attempt
            ground_instances4
            definitions12
            inductions0
            search_time
            0.018s
            details
            Expand
            smt_stats
            num checks9
            rlimit count4287
            mk clause200
            datatype occurs check62
            mk bool var189
            datatype splits12
            decisions62
            propagations216
            conflicts19
            datatype accessor ax27
            minimized lits1
            datatype constructor ax30
            num allocs1436875574
            final checks12
            added eqs296
            del clause46
            memory16.690000
            max memory18.750000
            Expand
            • start[0.018s]
                ripple_carry_adder :var_0: :var_1: false =
                false :: (false :: (false :: (true :: …)))
            • unroll
              expr
              (ripple_carry_adder_2445 a_2484 b_2485 false)
              expansions
              • xor
              • xoradder_sum
              • xoradder_sumadder_carry_out
            • unroll
              expr
              (let ((a!1 (and (= (not (|get.::.0_2490| a_2484)) (|get.::.0_2490| b_2485))
                              false)))…
              expansions
              • xor
              • xoradder_sum
              • xoradder_sumadder_carry_out
            • unroll
              expr
              (let ((a!1 (= (not (|get.::.0_2490| (|get.::.1_2491| a_2484)))
                            (|get.::.0_2490| (|get.…
              expansions
              • xor
              • xoradder_sum
              • xoradder_sumadder_carry_out
            • unroll
              expr
              (let ((a!1 (not (|get.::.0_2490| (|get.::.1_2491| (|get.::.1_2491| a_2484)))))
                    (a!3 (= (not (|…
              expansions
              • xor
              • xoradder_sum
              • xoradder_sumadder_carry_out
            • Sat (Some let a = [true; true; false] let b = [true; false; true] )

            Relating bit sequences to natural numbers

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

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

            Termination proof

            call `int_of_bits (List.tl a)` from `int_of_bits a`
            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.016s
            details
            Expand
            smt_stats
            num checks7
            arith assert lower7
            arith pivots4
            rlimit count6211
            mk clause11
            datatype occurs check33
            mk bool var60
            arith assert upper3
            datatype splits6
            decisions17
            arith add rows5
            propagations10
            conflicts8
            arith fixed eqs3
            datatype accessor ax5
            arith conflicts1
            datatype constructor ax9
            num allocs1478129834
            final checks9
            added eqs51
            del clause5
            arith eq adapter3
            memory19.580000
            max memory19.580000
            Expand
            • start[0.016s]
                not (a = []) && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
                ==> List.tl a = []
                    || Ordinal.Int (Ordinal.count (List.tl a)) Ordinal.<<
                       Ordinal.Int (Ordinal.count a)
            • simplify
              into
              (not
               ((not (a = []) && Ordinal.count a >= 0) && Ordinal.count (List.tl a) >= 0)
               || List.tl a = [])
              || Ordinal.Int (Ordinal.count (List.tl a)) Ordinal.<<
                 Ordinal.Int (Ordinal.count a)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                      (|count_`bool list`_2518| (|get.::.1_2491| …
                  expansions
                  • unroll
                    expr
                    (|count_`bool list`_2518| (|get.::.1_2491| a_2509))
                    expansions
                    • unroll
                      expr
                      (|count_`bool list`_2518| a_2509)
                      expansions
                      • unsat
                        (let ((a!1 (= (|count_`bool list`_2518| a_2509)
                                      (+ 1 (|count_`bool list`_2518| (|get.:…

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

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

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

                      In [14]:
                      instance (fun a -> int_of_bits a = 256)
                      
                      Out[14]:
                      - : bool list -> bool = <fun>
                      module CX : sig val a : bool list end
                      
                      Instance (after 10 steps, 0.036s):
                       let a = [false; false; false; false; false; false; false; false; true]
                      
                      Instance
                      proof attempt
                      ground_instances10
                      definitions10
                      inductions0
                      search_time
                      0.036s
                      details
                      Expand
                      smt_stats
                      arith offset eqs11
                      num checks21
                      arith assert lower185
                      arith pivots50
                      rlimit count10746
                      mk clause375
                      datatype occurs check85
                      mk bool var752
                      arith gcd tests9
                      arith assert upper165
                      datatype splits51
                      decisions146
                      arith add rows88
                      arith bound prop10
                      propagations473
                      conflicts71
                      arith fixed eqs44
                      datatype accessor ax40
                      minimized lits14
                      arith conflicts11
                      arith assert diseq79
                      datatype constructor ax69
                      num allocs1529521950
                      final checks44
                      added eqs792
                      del clause320
                      arith eq adapter194
                      memory20.510000
                      max memory20.510000
                      Expand
                      • start[0.036s] int_of_bits :var_0: = 256
                      • unroll
                        expr
                        (int_of_bits_2504 a_2521)
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (int_of_bits_2504 (|get.::.1_2526| a_2521))
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (int_of_bits_2504 (|get.::.1_2526| (|get.::.1_2526| a_2521)))
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (int_of_bits_2504 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (let ((a!1 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))))
                          (int_o…
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (let ((a!1 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))))
                          (int_o…
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (let ((a!1 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))))
                          (int_o…
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (let ((a!1 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))))
                          (int_o…
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (let ((a!1 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))))
                        (let ((a…
                        expansions
                        int_of_bit
                      • unroll
                        expr
                        (let ((a!1 (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| (|get.::.1_2526| a_2521))))))
                        (let ((a…
                        expansions
                        int_of_bit
                      • Sat (Some let a = [false; false; false; false; false; false; false; false; true] )
                      In [15]:
                      int_of_bits (ripple_carry_adder CX.a CX.a false)
                      
                      Out[15]:
                      - : Z.t = 512
                      

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

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

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

                      In [16]:
                      theorem full_ripple_carry_adder_correct a b cin =
                        List.length a = List.length b ==>
                        int_of_bits (ripple_carry_adder a b cin) =
                        int_of_bits a + int_of_bits b + int_of_bit cin
                      [@@induct functional ripple_carry_adder]
                      
                      Out[16]:
                      val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
                        <fun>
                      Goal:
                      
                      List.length a = List.length b
                      ==> int_of_bits (ripple_carry_adder a b cin) =
                          (int_of_bits a + int_of_bits b) + int_of_bit cin.
                      
                      1 nontautological subgoal.
                      
                      Subgoal 1:
                      
                       H0. 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)
                      
                      This simplifies, using the forward-chaining rule List.len_nonnegative to the
                      following 2 subgoals:
                      
                      Subgoal 1.2:
                      
                       H0. List.length a = List.length b
                      |---------------------------------------------------------------------------
                       C0. int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b
                       C1. cin
                      
                      This further simplifies to:
                      
                      Subgoal 1.2':
                      
                       H0. List.length a = List.length b
                      |---------------------------------------------------------------------------
                       C0. int_of_bits (ripple_carry_adder a b false) =
                           int_of_bits a + int_of_bits b
                       C1. cin
                      
                      Verified up to bound 10 (after 0.049s).
                      
                      Note: We must proceed by induction, but our current subgoal is less
                      appropriate for induction than our original conjecture. Thus, we prefer to
                      abandon our work until now and return our focus to the original conjecture
                      which we shall attempt to prove by induction directly.
                      
                      We shall induct according to a scheme derived from ripple_carry_adder.
                      
                      Induction scheme:
                      
                       (not (b <> [] && a <> []) ==> φ cin b a)
                       && ((b <> [] && a <> [])
                           && φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
                              (List.tl a)
                           ==> φ cin b a).
                      
                      2 nontautological subgoals.
                      
                      Subgoal 2:
                      
                       H0. List.length a = List.length b
                      |---------------------------------------------------------------------------
                       C0. b <> [] && a <> []
                       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 int_of_bits and ripple_carry_adder
                      to the following 2 subgoals:
                      
                      Subgoal 2.2:
                      
                       H0. List.length a = List.length b
                      |---------------------------------------------------------------------------
                       C0. 0 = int_of_bits a
                       C1. b <> []
                      
                      This simplifies, using the definition of List.length to:
                      
                      Subgoal 2.2':
                      
                       H0. List.length a = 0
                      |---------------------------------------------------------------------------
                       C0. b <> []
                       C1. 0 = int_of_bits a
                      
                      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. b <> []
                       H1. List.length a = List.length b
                      |---------------------------------------------------------------------------
                       C0. 0 = int_of_bits b
                       C1. a <> []
                      
                      This simplifies, using the definition of List.length to:
                      
                      Subgoal 2.1':
                      
                       H0. 0 = List.length b
                       H1. b <> []
                      |---------------------------------------------------------------------------
                       C0. a <> []
                       C1. 0 = int_of_bits b
                      
                      But simplification reduces this to true, using the rewrite rule
                      List.len_zero_is_empty.
                      
                      Subgoal 1:
                      
                       H0. b <> []
                       H1. a <> []
                       H2. List.length (List.tl a) = List.length (List.tl b)
                           ==> int_of_bits
                               (ripple_carry_adder (List.tl a) (List.tl b)
                                (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                               =
                               (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                               + (if not (List.hd a) = List.hd b && cin || List.hd a && List.hd b
                                  then 1 else 0)
                       H3. List.length a = List.length b
                      |---------------------------------------------------------------------------
                       int_of_bits (ripple_carry_adder a b cin) =
                       (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)
                      
                      But simplification reduces this to true, using the definitions of
                      List.length, int_of_bits and ripple_carry_adder.
                      
                      
                      Proved
                      proof
                      ground_instances0
                      definitions70
                      inductions1
                      search_time
                      0.895s
                      Expand
                      • start[0.895s, "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[0.894s, "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)
                        • simplify
                          into
                          ((int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b
                            || cin)
                           || not (List.length a = List.length b))
                          && ((int_of_bits (ripple_carry_adder a b cin) =
                               (1 + int_of_bits a) + int_of_bits b || not cin)
                              || not (List.length a = List.length b))
                          expansions
                          []
                          rewrite_steps
                            forward_chaining
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • subproof
                              (int_of_bits (ripple_carry_adder a b cin) = (1 + int_of_bits a) + int_of_bits b || not cin) || not (List.length a = List.length b)
                              start[0.818s, "1.1"]
                                (int_of_bits (ripple_carry_adder a b cin) =
                                 (1 + int_of_bits a) + int_of_bits b || not cin)
                                || not (List.length a = List.length b)
                            • subproof
                              (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b || cin) || not (List.length a = List.length b)
                              • start[0.818s, "1.2"]
                                  (int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b
                                   || cin)
                                  || not (List.length a = List.length b)
                              • simplify
                                into
                                (not (List.length a = List.length b)
                                 || int_of_bits (ripple_carry_adder a b false) =
                                    int_of_bits a + int_of_bits b)
                                || cin
                                expansions
                                int_of_bit
                                rewrite_steps
                                  forward_chaining
                                  • induction on (functional ripple_carry_adder)
                                    :scheme (not (b <> [] && a <> []) ==> φ cin b a)
                                            && ((b <> [] && a <> [])
                                                && φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
                                                   (List.tl a)
                                                ==> φ cin b a)
                                  • Split (((b <> [] && a <> [] || not (List.length a = List.length b))
                                            || int_of_bits (ripple_carry_adder a b cin) =
                                               (int_of_bits a + int_of_bits b) + (if cin then 1 else 0))
                                           && ((not
                                                ((b <> [] && a <> [])
                                                 && (not (List.length (List.tl a) = List.length (List.tl b))
                                                     || int_of_bits
                                                        (ripple_carry_adder (List.tl a) (List.tl b)
                                                         (not (List.hd a) = List.hd b && cin
                                                          || List.hd a && List.hd b))
                                                        =
                                                        (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                        + (if not (List.hd a) = List.hd b && cin
                                                              || List.hd a && List.hd b
                                                           then 1 else 0)))
                                                || not (List.length a = List.length b))
                                               || int_of_bits (ripple_carry_adder a b cin) =
                                                  (int_of_bits a + int_of_bits b) + (if cin then 1 else 0))
                                           :cases [(not (List.length a = List.length b) || b <> [] && a <> [])
                                                   || int_of_bits (ripple_carry_adder a b cin) =
                                                      (int_of_bits a + int_of_bits b) + (if cin then 1 else 0);
                                                   (((not (b <> []) || not (a <> []))
                                                     || not
                                                        (not (List.length (List.tl a) = List.length (List.tl b))
                                                         || int_of_bits
                                                            (ripple_carry_adder (List.tl a) (List.tl b)
                                                             (not (List.hd a) = List.hd b && cin
                                                              || List.hd a && List.hd b))
                                                            =
                                                            (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                            + (if not (List.hd a) = List.hd b && cin
                                                                  || List.hd a && List.hd b
                                                               then 1 else 0)))
                                                    || not (List.length a = List.length b))
                                                   || int_of_bits (ripple_carry_adder a b cin) =
                                                      (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)])
                                    • 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.020s
                            details
                            Expand
                            smt_stats
                            num checks1
                            arith assert lower60
                            arith pivots2
                            rlimit count1505
                            mk clause160
                            mk bool var133
                            arith assert upper60
                            decisions17
                            propagations158
                            conflicts17
                            minimized lits12
                            arith conflicts16
                            arith assert diseq1
                            added eqs98
                            del clause136
                            arith eq adapter59
                            memory26.610000
                            max memory27.360000
                            num allocs7730830316.000000
                            Expand
                            • start[0.020s]
                                (if not (not (:var_0: = :var_1:) = :var_2:) then 1 else 0) =
                                (((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0))
                                 + (if :var_2: then 1 else 0))
                                -
                                (2
                                 * (if not (:var_0: = :var_1:) && :var_2: || :var_0: && :var_1: then 1
                                    else 0))
                            • simplify

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

                                  (let ((a!1 (= (ite (= (= a_2585 b_2586) cin_2587) 1 0) 1))
                                        (a!2 (<= (ite (= (= a_2585 b_2586) …

                                Warning

                                Pattern will match only if `int_of_bit` is disabled
                                (non-recursive function)

                                Warning

                                Pattern will match only if `adder_sum` is disabled
                                (non-recursive function)

                                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.
                                
                                Subgoal 1:
                                
                                 H0. 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
                                
                                Verified up to bound 10 (after 0.032s).
                                
                                Must try induction.
                                
                                We shall induct according to a scheme derived from ripple_carry_adder.
                                
                                Induction scheme:
                                
                                 (not (b <> [] && a <> []) ==> φ b a cin)
                                 && ((b <> [] && a <> [])
                                     && φ (List.tl b) (List.tl a)
                                        (adder_carry_out (List.hd a) (List.hd b) cin)
                                     ==> φ b a cin).
                                
                                2 nontautological subgoals.
                                
                                Subgoal 1.2:
                                
                                 H0. List.length a = List.length b
                                |---------------------------------------------------------------------------
                                 C0. b <> [] && a <> []
                                 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 int_of_bits and ripple_carry_adder
                                to the following 4 subgoals:
                                
                                Subgoal 1.2.4:
                                
                                 H0. List.length a = List.length b
                                |---------------------------------------------------------------------------
                                 C0. 0 = int_of_bits a + int_of_bit cin
                                 C1. cin
                                 C2. b <> []
                                
                                This simplifies, using the definition of List.length to:
                                
                                Subgoal 1.2.4':
                                
                                 H0. List.length a = 0
                                |---------------------------------------------------------------------------
                                 C0. b <> []
                                 C1. cin
                                 C2. 0 = int_of_bits a + int_of_bit cin
                                
                                This simplifies, using the definition of int_of_bits, and the rewrite rule
                                List.len_zero_is_empty to:
                                
                                Subgoal 1.2.4'':
                                
                                 H0. a = []
                                |---------------------------------------------------------------------------
                                 C0. 0 = int_of_bit cin
                                 C1. cin
                                 C2. b <> []
                                
                                This simplifies to:
                                
                                Subgoal 1.2.4''':
                                
                                |---------------------------------------------------------------------------
                                 C0. b <> []
                                 C1. cin
                                 C2. 0 = int_of_bit cin
                                
                                This further simplifies to:
                                
                                Subgoal 1.2.4'''':
                                
                                |---------------------------------------------------------------------------
                                 C0. b <> []
                                 C1. cin
                                 C2. 0 = int_of_bit false
                                
                                But we verify Subgoal 1.2.4'''' by recursive unrolling.
                                
                                Subgoal 1.2.3:
                                
                                 H0. cin
                                 H1. List.length a = List.length b
                                |---------------------------------------------------------------------------
                                 C0. 0 = int_of_bits a
                                 C1. b <> []
                                
                                This simplifies, using the definition of List.length to:
                                
                                Subgoal 1.2.3':
                                
                                 H0. List.length a = 0
                                 H1. cin
                                |---------------------------------------------------------------------------
                                 C0. b <> []
                                 C1. 0 = int_of_bits a
                                
                                But simplification reduces this to true, using the definition of int_of_bits,
                                and the rewrite rule List.len_zero_is_empty.
                                
                                Subgoal 1.2.2:
                                
                                 H0. b <> []
                                 H1. List.length a = List.length b
                                |---------------------------------------------------------------------------
                                 C0. 0 = int_of_bits b + int_of_bit cin
                                 C1. cin
                                 C2. a <> []
                                
                                This simplifies, using the definition of List.length to:
                                
                                Subgoal 1.2.2':
                                
                                 H0. 0 = List.length b
                                 H1. b <> []
                                |---------------------------------------------------------------------------
                                 C0. a <> []
                                 C1. cin
                                 C2. 0 = 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.2.1:
                                
                                 H0. cin
                                 H1. b <> []
                                 H2. List.length a = List.length b
                                |---------------------------------------------------------------------------
                                 C0. 0 = int_of_bits b
                                 C1. a <> []
                                
                                This simplifies, using the definition of List.length to:
                                
                                Subgoal 1.2.1':
                                
                                 H0. 0 = List.length b
                                 H1. b <> []
                                 H2. cin
                                |---------------------------------------------------------------------------
                                 C0. a <> []
                                 C1. 0 = int_of_bits b
                                
                                But simplification reduces this to true, using the rewrite rule
                                List.len_zero_is_empty.
                                
                                Subgoal 1.1:
                                
                                 H0. b <> []
                                 H1. a <> []
                                 H2. List.length (List.tl a) = List.length (List.tl b)
                                     ==> int_of_bits
                                         (ripple_carry_adder (List.tl a) (List.tl b)
                                          (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                                         =
                                         (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                         + int_of_bit
                                           (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)
                                 H3. List.length a = List.length b
                                |---------------------------------------------------------------------------
                                 int_of_bits (ripple_carry_adder a b cin) =
                                 (int_of_bits a + int_of_bits b) + int_of_bit cin
                                
                                But simplification reduces this to true, using the definitions of
                                List.length, int_of_bits and ripple_carry_adder, and the rewrite rule
                                single_adder_circuit_correct.
                                
                                
                                Proved
                                proof
                                ground_instances0
                                definitions68
                                inductions1
                                search_time
                                0.741s
                                details
                                Expand
                                smt_stats
                                rlimit count65124
                                mk bool var5
                                memory38.500000
                                max memory38.800000
                                num allocs9685118049.000000
                                Expand
                                • start[0.741s, "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.740s, "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 (b <> [] && a <> []) ==> φ b a cin)
                                            && ((b <> [] && a <> [])
                                                && φ (List.tl b) (List.tl a)
                                                   (adder_carry_out (List.hd a) (List.hd b) cin)
                                                ==> φ b a cin)
                                  • Split (((b <> [] && a <> [] || not (List.length a = List.length b))
                                            || int_of_bits (ripple_carry_adder a b cin) =
                                               (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                           && ((not
                                                ((b <> [] && a <> [])
                                                 && (not (List.length (List.tl a) = List.length (List.tl b))
                                                     || int_of_bits
                                                        (ripple_carry_adder (List.tl a) (List.tl b)
                                                         (not (List.hd a) = List.hd b && cin
                                                          || List.hd a && List.hd b))
                                                        =
                                                        (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                        + int_of_bit
                                                          (not (List.hd a) = List.hd b && cin
                                                           || List.hd a && List.hd b)))
                                                || not (List.length a = List.length b))
                                               || int_of_bits (ripple_carry_adder a b cin) =
                                                  (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                           :cases [(not (List.length a = List.length b) || b <> [] && a <> [])
                                                   || int_of_bits (ripple_carry_adder a b cin) =
                                                      (int_of_bits a + int_of_bits b) + int_of_bit cin;
                                                   (((not (b <> []) || not (a <> []))
                                                     || not
                                                        (not (List.length (List.tl a) = List.length (List.tl b))
                                                         || int_of_bits
                                                            (ripple_carry_adder (List.tl a) (List.tl b)
                                                             (not (List.hd a) = List.hd b && cin
                                                              || List.hd a && List.hd b))
                                                            =
                                                            (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                            + int_of_bit
                                                              (not (List.hd a) = List.hd b && cin
                                                               || List.hd a && List.hd b)))
                                                    || not (List.length a = List.length b))
                                                   || int_of_bits (ripple_carry_adder a b cin) =
                                                      (int_of_bits a + int_of_bits b) + int_of_bit cin])
                                    • subproof
                                      (((not (b <> []) || not (a <> [])) || not (not (List.length (List.tl a) = List.length (List.tl b)) || int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)) = (int_of_bits (List.tl a) + int_of_bits (List.tl b)) + int_of_bit (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))) || not (List.length a = List.length b)) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                      • start[0.643s, "1.1"]
                                          (((not (b <> []) || not (a <> []))
                                            || not
                                               (not (List.length (List.tl a) = List.length (List.tl b))
                                                || int_of_bits
                                                   (ripple_carry_adder (List.tl a) (List.tl b)
                                                    (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                                                   =
                                                   (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                   + int_of_bit
                                                     (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)))
                                           || not (List.length a = List.length b))
                                          || int_of_bits (ripple_carry_adder a b cin) =
                                             (int_of_bits a + int_of_bits b) + int_of_bit cin
                                      • simplify
                                        into
                                        true
                                        expansions
                                        [List.length, List.length, int_of_bits, int_of_bits, int_of_bits,
                                         ripple_carry_adder, List.length, List.length, List.length, List.length,
                                         List.length, List.length, int_of_bits, int_of_bits, int_of_bits,
                                         ripple_carry_adder, List.length, List.length, List.length, List.length,
                                         int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, 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, List.length, List.length, List.length, List.length,
                                         List.length, List.length, int_of_bits, int_of_bits, int_of_bits,
                                         ripple_carry_adder, List.length, List.length]
                                        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
                                    • subproof
                                      (not (List.length a = List.length b) || b <> [] && a <> []) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                      • start[0.643s, "1.2"]
                                          (not (List.length a = List.length b) || b <> [] && a <> [])
                                          || int_of_bits (ripple_carry_adder a b cin) =
                                             (int_of_bits a + int_of_bits b) + int_of_bit cin
                                      • simplify
                                        into
                                        (((((0 = int_of_bits a + int_of_bit cin || cin) || b <> [])
                                           || not (List.length a = List.length b))
                                          && (((0 = int_of_bits a || not cin) || b <> [])
                                              || not (List.length a = List.length b)))
                                         && ((((0 = int_of_bits b + int_of_bit cin || cin) || a <> [])
                                              || not (b <> []))
                                             || not (List.length a = List.length b)))
                                        && ((((0 = int_of_bits b || not cin) || a <> []) || not (b <> []))
                                            || not (List.length a = List.length b))
                                        expansions
                                        [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
                                          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
                                          • 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.021s):
                                   let a = true
                                   let b = true
                                   let cin = true
                                  
                                  Refuted
                                  proof attempt
                                  ground_instances0
                                  definitions0
                                  inductions0
                                  search_time
                                  0.021s
                                  details
                                  Expand
                                  smt_stats
                                  num checks1
                                  arith assert lower5
                                  arith pivots2
                                  rlimit count761
                                  mk clause39
                                  mk bool var38
                                  arith assert upper7
                                  decisions4
                                  propagations14
                                  arith fixed eqs1
                                  arith assert diseq1
                                  final checks1
                                  added eqs9
                                  del clause2
                                  arith eq adapter6
                                  memory33.210000
                                  max memory38.800000
                                  num allocs16696026731.000000
                                  Expand
                                  • start[0.021s]
                                      (if not (not (:var_0: = :var_1:) || :var_2:) then 1 else 0) =
                                      (((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0))
                                       + (if :var_2: then 1 else 0))
                                      -
                                      (2
                                       * (if not (:var_0: = :var_1:) && :var_2: || :var_0: && :var_1: then 1
                                          else 0))
                                  • simplify

                                    into
                                    (if not :var_0: = :var_1: || :var_2: then 0 else 1) =
                                    (((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0))
                                     + (if :var_2: then 1 else 0))
                                    + -2
                                      * (if not :var_0: = :var_1: && :var_2: || :var_0: && :var_1: then 1 else 0)
                                    expansions
                                    []
                                    rewrite_steps
                                      forward_chaining
                                      • Sat (Some let a = true let b = true let cin = true )
                                      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[b <> [] && a <> []]
                                      proof
                                      detailed proof
                                      ground_instances3
                                      definitions0
                                      inductions0
                                      search_time
                                      0.017s
                                      details
                                      Expand
                                      smt_stats
                                      num checks8
                                      arith assert lower9
                                      arith pivots4
                                      rlimit count2885
                                      mk clause30
                                      datatype occurs check22
                                      mk bool var84
                                      arith assert upper4
                                      datatype splits6
                                      decisions28
                                      arith add rows6
                                      propagations30
                                      conflicts9
                                      arith fixed eqs4
                                      datatype accessor ax10
                                      arith conflicts1
                                      datatype constructor ax14
                                      final checks6
                                      added eqs87
                                      del clause17
                                      arith eq adapter6
                                      memory27.510000
                                      max memory38.800000
                                      num allocs17008680175.000000
                                      Expand
                                      • start[0.017s]
                                          (b <> [] && a <> [])
                                          && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
                                          ==> not ((List.tl b) <> [] && (List.tl a) <> [])
                                              || Ordinal.Int (Ordinal.count (List.tl a)) Ordinal.<<
                                                 Ordinal.Int (Ordinal.count a)
                                      • simplify
                                        into
                                        (not
                                         (((b <> [] && a <> []) && Ordinal.count a >= 0)
                                          && Ordinal.count (List.tl a) >= 0)
                                         || not ((List.tl b) <> [] && (List.tl a) <> []))
                                        || Ordinal.Int (Ordinal.count (List.tl a)) Ordinal.<<
                                           Ordinal.Int (Ordinal.count a)
                                        expansions
                                        []
                                        rewrite_steps
                                          forward_chaining
                                          • unroll
                                            expr
                                            (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                (|count_`bool list`_2722| (|get.::.1_2708| …
                                            expansions
                                            • unroll
                                              expr
                                              (|count_`bool list`_2722| (|get.::.1_2708| a_2709))
                                              expansions
                                              • unroll
                                                expr
                                                (|count_`bool list`_2722| a_2709)
                                                expansions
                                                • unsat
                                                  (let ((a!1 (= (|count_`bool list`_2722| a_2709)
                                                                (+ 1 (|count_`bool list`_2722| (|get.:…

                                                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 : 'a list val b : bool list end
                                                
                                                Instance (after 5 steps, 0.021s):
                                                 let a = []
                                                 let b = [true]
                                                
                                                Instance
                                                proof attempt
                                                ground_instances5
                                                definitions7
                                                inductions0
                                                search_time
                                                0.021s
                                                details
                                                Expand
                                                smt_stats
                                                arith offset eqs5
                                                num checks11
                                                arith assert lower54
                                                arith patches_succ1
                                                arith pivots32
                                                rlimit count6041
                                                mk clause185
                                                datatype occurs check65
                                                mk bool var331
                                                arith gcd tests7
                                                arith assert upper64
                                                datatype splits29
                                                decisions145
                                                arith add rows83
                                                arith bound prop8
                                                propagations201
                                                arith patches4
                                                conflicts22
                                                arith fixed eqs19
                                                datatype accessor ax19
                                                minimized lits1
                                                arith conflicts1
                                                arith assert diseq24
                                                datatype constructor ax38
                                                final checks23
                                                added eqs373
                                                del clause85
                                                arith ineq splits2
                                                arith eq adapter54
                                                memory28.080000
                                                max memory38.800000
                                                num allocs17147778628.000000
                                                Expand
                                                • start[0.021s]
                                                    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_2504 b_2726)
                                                  expansions
                                                  int_of_bit
                                                • unroll
                                                  expr
                                                  (int_of_bits_2504 a_2725)
                                                  expansions
                                                  int_of_bit
                                                • unroll
                                                  expr
                                                  (bad_ripple_carry_adder_2695 a_2725 b_2726 false)
                                                  expansions
                                                  • xor
                                                  • xorbad_adder_sum
                                                  • xorbad_adder_sumbad_adder_carry_out
                                                • unroll
                                                  expr
                                                  (int_of_bits_2504 (bad_ripple_carry_adder_2695 a_2725 b_2726 false))
                                                  expansions
                                                  int_of_bit
                                                • unroll
                                                  expr
                                                  (int_of_bits_2504 (|get.::.1_2732| b_2726))
                                                  expansions
                                                  int_of_bit
                                                • Sat (Some let a = [] let b = [true] )

                                                Happy verifying!