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.026s
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 allocs1319582276
final checks6
added eqs87
del clause17
arith eq adapter6
memory25.070000
max memory27.740000
Expand
  • start[0.026s]
      (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.045s):
             let a = [true; true; false]
             let b = [true; false; true]
            
            Instance
            proof attempt
            ground_instances4
            definitions12
            inductions0
            search_time
            0.045s
            details
            Expand
            smt_stats
            num checks9
            rlimit count4164
            mk clause197
            datatype occurs check56
            mk bool var186
            datatype splits12
            decisions53
            propagations204
            conflicts16
            datatype accessor ax27
            minimized lits1
            datatype constructor ax28
            num allocs1391346310
            final checks11
            added eqs281
            del clause46
            memory25.670000
            max memory27.740000
            Expand
            • start[0.045s]
                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.037s
            details
            Expand
            smt_stats
            num checks7
            arith assert lower7
            arith pivots4
            rlimit count6088
            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 allocs1432654354
            final checks9
            added eqs51
            del clause5
            arith eq adapter3
            memory28.560000
            max memory28.560000
            Expand
            • start[0.037s]
                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.101s):
                       let a = [false; false; false; false; false; false; false; false; true]
                      
                      Instance
                      proof attempt
                      ground_instances10
                      definitions10
                      inductions0
                      search_time
                      0.101s
                      details
                      Expand
                      smt_stats
                      arith offset eqs13
                      num checks21
                      arith assert lower269
                      arith pivots69
                      rlimit count14247
                      mk clause605
                      datatype occurs check162
                      mk bool var1236
                      arith gcd tests10
                      arith assert upper256
                      datatype splits124
                      decisions190
                      arith add rows114
                      arith bound prop19
                      propagations708
                      conflicts82
                      arith fixed eqs66
                      datatype accessor ax108
                      minimized lits12
                      arith conflicts15
                      arith assert diseq131
                      datatype constructor ax133
                      num allocs1482951032
                      final checks49
                      added eqs1395
                      del clause582
                      arith eq adapter276
                      memory29.460000
                      max memory29.460000
                      Expand
                      • start[0.101s] 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.094s).
                      
                      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
                      3.025s
                      Expand
                      • start[3.025s, "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[3.024s, "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[2.599s, "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[2.599s, "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.028s
                            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
                            memory36.570000
                            max memory37.030000
                            num allocs7685610769.000000
                            Expand
                            • start[0.028s]
                                (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.049s).
                                
                                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
                                1.446s
                                details
                                Expand
                                smt_stats
                                rlimit count71008
                                mk bool var5
                                memory35.710000
                                max memory42.600000
                                num allocs9916345740.000000
                                Expand
                                • start[1.446s, "Goal"]
                                    List.length :var_0: = List.length :var_1:
                                    ==> int_of_bits (ripple_carry_adder :var_0: :var_1: :var_2:) =
                                        (int_of_bits :var_0: + int_of_bits :var_1:) + int_of_bit :var_2:
                                • subproof

                                  not (List.length a = List.length b) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                  • start[1.445s, "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[1.281s, "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[1.282s, "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.020s):
                                   let a = true
                                   let b = true
                                   let cin = true
                                  
                                  Refuted
                                  proof attempt
                                  ground_instances0
                                  definitions0
                                  inductions0
                                  search_time
                                  0.020s
                                  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
                                  memory25.050000
                                  max memory42.600000
                                  num allocs17049944493.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 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.031s
                                      details
                                      Expand
                                      smt_stats
                                      num checks8
                                      arith assert lower8
                                      arith pivots4
                                      rlimit count2885
                                      mk clause30
                                      datatype occurs check22
                                      mk bool var84
                                      arith assert upper5
                                      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.880000
                                      max memory42.600000
                                      num allocs17172007929.000000
                                      Expand
                                      • start[0.031s]
                                          (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.026s):
                                                 let a = []
                                                 let b = [true]
                                                
                                                Instance
                                                proof attempt
                                                ground_instances5
                                                definitions7
                                                inductions0
                                                search_time
                                                0.026s
                                                details
                                                Expand
                                                smt_stats
                                                arith offset eqs5
                                                num checks11
                                                arith assert lower45
                                                arith patches_succ1
                                                arith pivots33
                                                rlimit count6244
                                                mk clause165
                                                datatype occurs check63
                                                mk bool var296
                                                arith gcd tests8
                                                arith assert upper55
                                                datatype splits25
                                                decisions162
                                                arith add rows93
                                                arith bound prop8
                                                propagations178
                                                arith patches2
                                                conflicts20
                                                arith fixed eqs19
                                                datatype accessor ax15
                                                arith conflicts2
                                                arith assert diseq14
                                                datatype constructor ax33
                                                final checks20
                                                added eqs335
                                                del clause70
                                                arith ineq splits1
                                                arith eq adapter48
                                                memory28.480000
                                                max memory42.600000
                                                num allocs17315494904.000000
                                                Expand
                                                • start[0.026s]
                                                    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!