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 (_cnt a)
sub ordinalOrdinal.Int (_cnt (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
num checks7
arith-make-feasible7
arith-max-columns13
arith-conflicts1
rlimit count2072
mk clause29
datatype occurs check26
mk bool var75
arith-lower4
datatype splits6
decisions30
propagations28
arith-max-rows5
conflicts8
datatype accessor ax9
datatype constructor ax14
num allocs792930
final checks6
added eqs86
del clause14
arith eq adapter5
arith-upper6
memory5.660000
max memory5.660000
Expand
  • start[0.016s]
      let (_x_0 : int) = count.list (const 0) a in
      let (_x_1 : bool list) = List.tl a in
      let (_x_2 : int) = count.list (const 0) _x_1 in
      a <> [] && b <> [] && _x_0 >= 0 && _x_2 >= 0
      ==> not (_x_1 <> [] && (List.tl b) <> [])
          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : bool list) = List.tl a in
    let (_x_1 : int) = count.list (const 0) _x_0 in
    let (_x_2 : int) = count.list (const 0) a in
    (not (_x_0 <> [] && (List.tl b) <> [])
     || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not (((a <> [] && b <> []) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list (const 0)[0]`_1703| a_1688)
        expansions
        • unroll
          expr
          (|`count.list (const 0)[0]`_1703| (|get.::.1_1687| a_1688))
          expansions
          • unroll
            expr
            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                (|`count.list (const 0)[0]`_1703| (|get.::.…
            expansions
            • Unsat

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

            In [6]:
            let zero = []
            let one = [true]
            let two = [false; true]
            
            Out[6]:
            val zero : 'a list = []
            val one : bool list = [true]
            val two : bool list = [false;true]
            
            In [7]:
            ripple_carry_adder zero zero false
            
            Out[7]:
            - : bool list = []
            
            In [8]:
            ripple_carry_adder one one false
            
            Out[8]:
            - : bool list = [false;true]
            
            In [9]:
            instance (fun a b -> ripple_carry_adder a b false = [false; false; false; true])
            
            Out[9]:
            - : bool list -> bool list -> bool = <fun>
            module CX : sig val a : bool list val b : bool list end
            
            Instance (after 4 steps, 0.015s):
             let (a : bool list) = [true; true; true]
             let (b : bool list) = [true; false; false; false]
            
            Instance
            proof attempt
            ground_instances4
            definitions0
            inductions0
            search_time
            0.015s
            details
            Expand
            smt_stats
            num checks9
            arith-make-feasible6
            arith-max-columns4
            rlimit count5515
            mk clause246
            datatype occurs check61
            mk bool var240
            datatype splits8
            decisions65
            propagations290
            conflicts19
            datatype accessor ax32
            minimized lits4
            datatype constructor ax42
            num allocs3239354
            final checks9
            added eqs435
            del clause90
            time0.001000
            memory6.650000
            max memory6.650000
            Expand
            • start[0.015s]
                ripple_carry_adder ( :var_0: ) ( :var_1: ) false =
                [false; false; false; true]
            • unroll
              expr
              (ripple_carry_adder_25 a_43 b_44 false)
              expansions
              • unroll
                expr
                (ripple_carry_adder_25
                  (|get.::.1_1746| a_43)
                  (|get.::.1_1746| b_44)
                  (adder_carry_out_21 (|get…
                expansions
                • unroll
                  expr
                  (ripple_carry_adder_25
                    (|get.::.1_1746| (|get.::.1_1746| a_43))
                    (|get.::.1_1746| (|get.::.1_1746…
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (adder_carry_out_21
                                 (|get.::.0_1745| (|get.::.1_1746| (|get.::.1_1746| a_43)…
                    expansions
                    • Sat (Some let (a : bool list) = [true; true; true] let (b : bool list) = [true; false; false; false] )

                    Relating bit sequences to natural numbers

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

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

                    Termination proof

                    call `int_of_bits (List.tl a)` from `int_of_bits a`
                    originalint_of_bits a
                    subint_of_bits (List.tl a)
                    original ordinalOrdinal.Int (_cnt a)
                    sub ordinalOrdinal.Int (_cnt (List.tl a))
                    path[not Is_a([], a)]
                    proof
                    detailed proof
                    ground_instances3
                    definitions0
                    inductions0
                    search_time
                    0.014s
                    details
                    Expand
                    smt_stats
                    num checks7
                    arith-make-feasible7
                    arith-max-columns11
                    rlimit count1647
                    mk clause19
                    datatype occurs check18
                    mk bool var42
                    arith-lower3
                    datatype splits3
                    decisions10
                    propagations12
                    arith-max-rows3
                    conflicts3
                    datatype accessor ax7
                    datatype constructor ax5
                    num allocs5324983
                    final checks6
                    added eqs38
                    del clause13
                    arith eq adapter3
                    arith-upper6
                    memory9.590000
                    max memory9.590000
                    Expand
                    • start[0.014s]
                        let (_x_0 : int) = count.list (const 0) a in
                        let (_x_1 : bool list) = List.tl a in
                        let (_x_2 : int) = count.list (const 0) _x_1 in
                        not Is_a([], a) && _x_0 >= 0 && _x_2 >= 0
                        ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                    • simplify
                      into
                      let (_x_0 : bool list) = List.tl a in
                      let (_x_1 : int) = count.list (const 0) _x_0 in
                      let (_x_2 : int) = count.list (const 0) a in
                      (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                      || not ((not Is_a([], a) && _x_2 >= 0) && _x_1 >= 0)
                      expansions
                      []
                      rewrite_steps
                        forward_chaining
                        • unroll
                          expr
                          (|`count.list (const 0)[0]`_1803| a_1792)
                          expansions
                          • unroll
                            expr
                            (|`count.list (const 0)[0]`_1803| (|get.::.1_1791| a_1792))
                            expansions
                            • unroll
                              expr
                              (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                  (|`count.list (const 0)[0]`_1803| (|get.::.…
                              expansions
                              • Unsat

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

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

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

                              In [14]:
                              instance (fun a -> int_of_bits a = 256)
                              
                              Out[14]:
                              - : bool list -> bool = <fun>
                              module CX : sig val a : bool list end
                              
                              Instance (after 10 steps, 0.026s):
                               let (a : bool list) =
                                [false; false; false; false; false; false; false; false; true]
                              
                              Instance
                              proof attempt
                              ground_instances10
                              definitions0
                              inductions0
                              search_time
                              0.026s
                              details
                              Expand
                              smt_stats
                              num checks21
                              arith-make-feasible121
                              arith-max-columns43
                              arith-conflicts14
                              rlimit count8248
                              arith-gcd-calls8
                              arith-cheap-eqs9
                              mk clause359
                              datatype occurs check29
                              mk bool var518
                              arith-lower95
                              arith-diseq109
                              datatype splits10
                              decisions66
                              arith-propagations81
                              propagations315
                              arith-bound-propagations-cheap81
                              arith-max-rows18
                              conflicts43
                              datatype accessor ax44
                              arith-bound-propagations-lp24
                              datatype constructor ax44
                              num allocs8395731
                              final checks29
                              added eqs598
                              del clause337
                              arith eq adapter135
                              arith-upper140
                              arith-gcd-conflict8
                              memory12.950000
                              max memory12.950000
                              Expand
                              • start[0.026s] int_of_bits ( :var_0: ) = 256
                              • unroll
                                expr
                                (int_of_bits_48 a_54)
                                expansions
                                • unroll
                                  expr
                                  (int_of_bits_48 (|get.::.1_1834| a_54))
                                  expansions
                                  • unroll
                                    expr
                                    (int_of_bits_48 (|get.::.1_1834| (|get.::.1_1834| a_54)))
                                    expansions
                                    • unroll
                                      expr
                                      (int_of_bits_48 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))))
                                          (int_of_…
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))))
                                            (int_of_…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))))
                                              (int_of_…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))))
                                                (int_of_…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))))
                                                (let ((a!2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| (|get.::.1_1834| a_54))))))
                                                  (let ((a!2…
                                                  expansions
                                                  • Sat (Some let (a : bool list) = [false; false; false; false; false; false; false; false; true] )
                                                  In [15]:
                                                  int_of_bits (ripple_carry_adder CX.a CX.a false)
                                                  
                                                  Out[15]:
                                                  - : int = 512
                                                  

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

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

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

                                                  In [16]:
                                                  theorem full_ripple_carry_adder_correct a b cin =
                                                    List.length a = List.length b ==>
                                                    int_of_bits (ripple_carry_adder a b cin) =
                                                    int_of_bits a + int_of_bits b + int_of_bit cin
                                                  [@@induct functional ripple_carry_adder]
                                                  
                                                  Out[16]:
                                                  val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
                                                    <fun>
                                                  Goal:
                                                  
                                                  List.length a = List.length b
                                                  ==> int_of_bits (ripple_carry_adder a b cin) =
                                                      int_of_bits a + int_of_bits b + int_of_bit cin.
                                                  
                                                  1 nontautological subgoal.
                                                  
                                                  We shall induct according to a scheme derived from ripple_carry_adder.
                                                  
                                                  Induction scheme:
                                                  
                                                   (not (a <> [] && b <> []) ==> φ a b cin)
                                                   && (b <> []
                                                       && a <> []
                                                          && φ (List.tl a) (List.tl b)
                                                             (adder_carry_out (List.hd a) (List.hd b) cin)
                                                       ==> φ a b cin).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 2:
                                                  
                                                   H0. List.length a = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> [] && b <> []
                                                   C1. int_of_bits (ripple_carry_adder a b cin) =
                                                       int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                  
                                                  This simplifies, using the definitions of List.length, int_of_bits and
                                                  ripple_carry_adder to the following 4 subgoals:
                                                  
                                                  Subgoal 2.4:
                                                  
                                                   H0. 0 = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. a <> []
                                                   C2. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  This simplifies, using the definition of int_of_bits, and the rewrite rule
                                                  List.len_zero_is_empty to:
                                                  
                                                  Subgoal 2.4':
                                                  
                                                   H0. b = []
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. a <> []
                                                   C2. 0 = int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits.
                                                  
                                                  Subgoal 2.3:
                                                  
                                                   H0. a <> []
                                                   H1. List.length a = 0
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. b <> []
                                                   C2. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the rewrite rule
                                                  List.len_zero_is_empty.
                                                  
                                                  Subgoal 2.2:
                                                  
                                                   H0. cin
                                                   H1. 0 = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  This simplifies, using the definition of int_of_bits, and the rewrite rule
                                                  List.len_zero_is_empty to:
                                                  
                                                  Subgoal 2.2':
                                                  
                                                   H0. cin
                                                   H1. b = []
                                                  |---------------------------------------------------------------------------
                                                   C0. a <> []
                                                   C1. 0 = int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits.
                                                  
                                                  Subgoal 2.1:
                                                  
                                                   H0. cin
                                                   H1. a <> []
                                                   H2. List.length a = 0
                                                  |---------------------------------------------------------------------------
                                                   C0. b <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the rewrite rule
                                                  List.len_zero_is_empty.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. List.length a = List.length b
                                                   H1. b <> []
                                                   H2. a <> []
                                                   H3. List.length (List.tl a) = List.length (List.tl b)
                                                       ==> int_of_bits
                                                           (ripple_carry_adder (List.tl a) (List.tl b)
                                                            (List.hd a && List.hd b || not (List.hd a) = List.hd b && cin))
                                                           =
                                                           int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                           + (if List.hd a && List.hd b || not (List.hd a) = List.hd b && cin
                                                              then 1 else 0)
                                                  |---------------------------------------------------------------------------
                                                   int_of_bits (ripple_carry_adder a b cin) =
                                                   int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                  
                                                  This simplifies, using the definitions of List.length, int_of_bits and
                                                  ripple_carry_adder to the following 4 subgoals:
                                                  
                                                  Subgoal 1.4:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. b <> []
                                                   H2. a <> []
                                                   H3. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. List.hd a
                                                   C2. List.hd a = List.hd b
                                                   C3. int_of_bits (ripple_carry_adder a b false) =
                                                       1 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                  Subgoal 1.3:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. cin
                                                   H2. b <> []
                                                   H3. a <> []
                                                   H4. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       1 + int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. List.hd a
                                                   C1. List.hd a = List.hd b
                                                   C2. int_of_bits (ripple_carry_adder a b true) =
                                                       2 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                  Subgoal 1.2:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. List.hd a
                                                   H2. b <> []
                                                   H3. a <> []
                                                   H4. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. cin
                                                   C1. List.hd b
                                                   C2. List.hd a = List.hd b
                                                   C3. int_of_bits (ripple_carry_adder a b false) =
                                                       1 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                  Subgoal 1.1:
                                                  
                                                   H0. List.length (List.tl a) = List.length (List.tl b)
                                                   H1. cin
                                                   H2. List.hd a
                                                   H3. b <> []
                                                   H4. a <> []
                                                   H5. int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) cin) =
                                                       1 + int_of_bits (List.tl a) + int_of_bits (List.tl b)
                                                  |---------------------------------------------------------------------------
                                                   C0. List.hd b
                                                   C1. List.hd a = List.hd b
                                                   C2. int_of_bits (ripple_carry_adder a b true) =
                                                       2 + 2 * int_of_bits (List.tl a) + 2 * int_of_bits (List.tl b)
                                                  
                                                  But simplification reduces this to true, using the definitions of int_of_bits
                                                  and ripple_carry_adder.
                                                  
                                                   Rules:
                                                      (:def List.length)
                                                      (:def int_of_bits)
                                                      (:def ripple_carry_adder)
                                                      (:rw List.len_zero_is_empty)
                                                      (:fc List.len_nonnegative)
                                                      (:induct ripple_carry_adder)
                                                  
                                                  
                                                  Proved
                                                  proof
                                                  ground_instances0
                                                  definitions63
                                                  inductions1
                                                  search_time
                                                  1.776s
                                                  Expand
                                                  • start[1.776s, "Goal"]
                                                      List.length ( :var_0: ) = List.length ( :var_1: )
                                                      ==> int_of_bits (ripple_carry_adder ( :var_0: ) ( :var_1: ) ( :var_2: )) =
                                                          int_of_bits ( :var_0: ) + int_of_bits ( :var_1: )
                                                          + (if ( :var_2: ) then 1 else 0)
                                                  • subproof

                                                    not (List.length a = List.length b) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                    • start[1.776s, "1"]
                                                        not (List.length a = List.length b)
                                                        || int_of_bits (ripple_carry_adder a b cin) =
                                                           int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                    • induction on (functional ripple_carry_adder)
                                                      :scheme (not (a <> [] && b <> []) ==> φ a b cin)
                                                              && (b <> []
                                                                  && a <> []
                                                                     && φ (List.tl a) (List.tl b)
                                                                        (adder_carry_out (List.hd a) (List.hd b) cin)
                                                                  ==> φ a b cin)
                                                    • Split (let (_x_0 : bool) = a <> [] in
                                                             let (_x_1 : bool) = b <> [] in
                                                             let (_x_2 : bool) = not (List.length a = List.length b) in
                                                             let (_x_3 : bool)
                                                                 = int_of_bits (ripple_carry_adder a b cin) =
                                                                   int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                             in
                                                             let (_x_4 : bool list) = List.tl a in
                                                             let (_x_5 : bool list) = List.tl b in
                                                             let (_x_6 : bool) = List.hd a in
                                                             let (_x_7 : bool) = List.hd b in
                                                             let (_x_8 : bool) = _x_6 && _x_7 || not _x_6 = _x_7 && cin in
                                                             ((_x_0 && _x_1 || _x_2) || _x_3)
                                                             && ((_x_2 || _x_3)
                                                                 || not
                                                                    ((_x_1 && _x_0)
                                                                     && (not (List.length _x_4 = List.length _x_5)
                                                                         || int_of_bits (ripple_carry_adder _x_4 _x_5 _x_8) =
                                                                            int_of_bits _x_4 + int_of_bits _x_5
                                                                            + (if _x_8 then 1 else 0))))
                                                             :cases [(not (List.length a = List.length b) || a <> [] && b <> [])
                                                                     || int_of_bits (ripple_carry_adder a b cin) =
                                                                        int_of_bits a + int_of_bits b + (if cin then 1 else 0);
                                                                     let (_x_0 : bool list) = List.tl a in
                                                                     let (_x_1 : bool list) = List.tl b in
                                                                     let (_x_2 : bool) = List.hd a in
                                                                     let (_x_3 : bool) = List.hd b in
                                                                     let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in
                                                                     (((not (List.length a = List.length b) || not (b <> []))
                                                                       || not (a <> []))
                                                                      || not
                                                                         (List.length _x_0 = List.length _x_1
                                                                          ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) =
                                                                              int_of_bits _x_0 + int_of_bits _x_1
                                                                              + (if _x_4 then 1 else 0)))
                                                                     || int_of_bits (ripple_carry_adder a b cin) =
                                                                        int_of_bits a + int_of_bits b + (if cin then 1 else 0)])
                                                      • subproof
                                                        let (_x_0 : bool list) = List.tl a in let (_x_1 : bool list) = List.tl b in let (_x_2 : bool) = List.hd a in let (_x_3 : bool) = List.hd b in let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in (((not (List.length a = List.length b) || not (b <> [])) || not (a <> [])) || not (List.length _x_0 = List.length _x_1 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) = int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0))) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                        • start[1.775s, "1"]
                                                            let (_x_0 : bool list) = List.tl a in
                                                            let (_x_1 : bool list) = List.tl b in
                                                            let (_x_2 : bool) = List.hd a in
                                                            let (_x_3 : bool) = List.hd b in
                                                            let (_x_4 : bool) = _x_2 && _x_3 || not _x_2 = _x_3 && cin in
                                                            (((not (List.length a = List.length b) || not (b <> [])) || not (a <> []))
                                                             || not
                                                                (List.length _x_0 = List.length _x_1
                                                                 ==> int_of_bits (ripple_carry_adder _x_0 _x_1 _x_4) =
                                                                     int_of_bits _x_0 + int_of_bits _x_1 + (if _x_4 then 1 else 0)))
                                                            || int_of_bits (ripple_carry_adder a b cin) =
                                                               int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                        • simplify
                                                          into
                                                          let (_x_0 : bool list) = List.tl a in
                                                          let (_x_1 : bool list) = List.tl b in
                                                          let (_x_2 : bool) = not (List.length _x_0 = List.length _x_1) in
                                                          let (_x_3 : bool) = cin || _x_2 in
                                                          let (_x_4 : bool) = List.hd a in
                                                          let (_x_5 : bool) = List.hd b in
                                                          let (_x_6 : bool) = _x_4 = _x_5 in
                                                          let (_x_7 : int) = int_of_bits _x_0 in
                                                          let (_x_8 : int) = 2 * _x_7 in
                                                          let (_x_9 : int) = int_of_bits _x_1 in
                                                          let (_x_10 : int) = 2 * _x_9 in
                                                          let (_x_11 : bool)
                                                              = int_of_bits (ripple_carry_adder a b false) = 1 + _x_8 + _x_10
                                                          in
                                                          let (_x_12 : bool) = not (b <> []) in
                                                          let (_x_13 : bool) = not (a <> []) in
                                                          let (_x_14 : int) = int_of_bits (ripple_carry_adder _x_0 _x_1 cin) in
                                                          let (_x_15 : bool) = not (_x_14 = _x_7 + _x_9) in
                                                          let (_x_16 : bool) = not cin in
                                                          let (_x_17 : bool)
                                                              = int_of_bits (ripple_carry_adder a b true) = 2 + _x_8 + _x_10
                                                          in
                                                          let (_x_18 : bool) = not (_x_14 = 1 + _x_7 + _x_9) in
                                                          let (_x_19 : bool) = not _x_4 in
                                                          ((((((((_x_3 || _x_4) || _x_6) || _x_11) || _x_12) || _x_13) || _x_15)
                                                            && (((((((_x_2 || _x_4) || _x_6) || _x_16) || _x_12) || _x_13) || _x_17)
                                                                || _x_18))
                                                           && (((((((_x_3 || _x_5) || _x_6) || _x_11) || _x_19) || _x_12) || _x_13)
                                                               || _x_15))
                                                          && ((((((((_x_2 || _x_5) || _x_6) || _x_16) || _x_19) || _x_12) || _x_13)
                                                               || _x_17)
                                                              || _x_18)
                                                          expansions
                                                          [List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder,
                                                           int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder, List.length,
                                                           List.length, int_of_bits, int_of_bits, List.length, List.length,
                                                           int_of_bits, int_of_bits, List.length, List.length, int_of_bits,
                                                           int_of_bits, List.length, List.length, int_of_bits, int_of_bits,
                                                           int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder]
                                                          rewrite_steps
                                                            forward_chaining
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • List.len_nonnegative
                                                            • Subproof
                                                            • Subproof
                                                            • Subproof
                                                            • Subproof
                                                        • subproof
                                                          (not (List.length a = List.length b) || a <> [] && b <> []) || int_of_bits (ripple_carry_adder a b cin) = int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                          • start[1.775s, "2"]
                                                              (not (List.length a = List.length b) || a <> [] && b <> [])
                                                              || int_of_bits (ripple_carry_adder a b cin) =
                                                                 int_of_bits a + int_of_bits b + (if cin then 1 else 0)
                                                          • simplify
                                                            into
                                                            let (_x_0 : bool) = a <> [] in
                                                            let (_x_1 : bool) = not (0 = List.length b) in
                                                            let (_x_2 : bool) = 0 = int_of_bits a + int_of_bits b in
                                                            let (_x_3 : bool) = b <> [] in
                                                            let (_x_4 : bool) = not _x_0 in
                                                            let (_x_5 : bool) = not (List.length a = 0) in
                                                            let (_x_6 : bool) = not cin in
                                                            (((((cin || _x_0) || _x_1) || _x_2)
                                                              && ((((cin || _x_3) || _x_4) || _x_2) || _x_5))
                                                             && (((_x_0 || _x_6) || _x_1) || _x_2))
                                                            && ((((_x_3 || _x_6) || _x_4) || _x_2) || _x_5)
                                                            expansions
                                                            [List.length, List.length, List.length, List.length, int_of_bits,
                                                             int_of_bits, ripple_carry_adder]
                                                            rewrite_steps
                                                              forward_chaining
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • List.len_nonnegative
                                                              • Subproof
                                                              • Subproof
                                                              • Subproof
                                                              • Subproof

                                                      Excellent!

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

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

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

                                                      In [17]:
                                                      theorem single_adder_circuit_correct a b cin =
                                                        int_of_bit (adder_sum a b cin)
                                                          = int_of_bit a + int_of_bit b + int_of_bit cin - (2 * (int_of_bit (adder_carry_out a b cin)))
                                                      [@@rewrite]
                                                      
                                                      Out[17]:
                                                      val single_adder_circuit_correct : bool -> bool -> bool -> bool = <fun>
                                                      
                                                      Proved
                                                      proof
                                                      ground_instances0
                                                      definitions0
                                                      inductions0
                                                      search_time
                                                      0.041s
                                                      details
                                                      Expand
                                                      smt_stats
                                                      num checks1
                                                      arith-make-feasible31
                                                      arith-max-columns11
                                                      arith-conflicts16
                                                      rlimit count1683
                                                      mk clause115
                                                      mk bool var138
                                                      arith-lower60
                                                      arith-diseq2
                                                      decisions15
                                                      arith-propagations4
                                                      propagations142
                                                      arith-bound-propagations-cheap4
                                                      arith-max-rows1
                                                      conflicts16
                                                      minimized lits22
                                                      added eqs157
                                                      del clause81
                                                      arith eq adapter59
                                                      arith-upper60
                                                      time0.023000
                                                      memory48.970000
                                                      max memory66.440000
                                                      num allocs5833158865.000000
                                                      Expand
                                                      • start[0.041s]
                                                          let (_x_0 : bool) = not (( :var_0: ) = ( :var_1: )) in
                                                          (if not (_x_0 = ( :var_2: )) then 1 else 0) =
                                                          ((if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0)
                                                           + (if ( :var_2: ) then 1 else 0))
                                                          -
                                                          (2 * (if _x_0 && ( :var_2: ) || ( :var_0: ) && ( :var_1: ) then 1 else 0))
                                                      • simplify

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

                                                          Warning

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

                                                          Warning

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

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

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

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

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

                                                            Examining a flawed circuit with Imandra

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

                                                            Can you spot the error?

                                                            In [19]:
                                                            let bad_adder_sum a b cin =
                                                              not ((xor a b) || cin)
                                                            
                                                            Out[19]:
                                                            val bad_adder_sum : bool -> bool -> bool -> bool = <fun>
                                                            
                                                            In [20]:
                                                            let bad_adder_carry_out a b cin =
                                                              ((xor a b) && cin) || (a && b)
                                                            
                                                            Out[20]:
                                                            val bad_adder_carry_out : bool -> bool -> bool -> bool = <fun>
                                                            
                                                            In [21]:
                                                            verify (fun a b cin ->
                                                             int_of_bit (bad_adder_sum a b cin)
                                                                = int_of_bit a + int_of_bit b + int_of_bit cin - (2 * (int_of_bit (bad_adder_carry_out a b cin))))
                                                            
                                                            Out[21]:
                                                            - : bool -> bool -> bool -> bool = <fun>
                                                            module CX : sig val a : bool val b : bool val cin : bool end
                                                            
                                                            Counterexample (after 0 steps, 0.035s):
                                                             let (a : bool) = false
                                                             let (b : bool) = false
                                                             let (cin : bool) = false
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances0
                                                            definitions0
                                                            inductions0
                                                            search_time
                                                            0.035s
                                                            details
                                                            Expand
                                                            smt_stats
                                                            num checks1
                                                            arith-make-feasible14
                                                            arith-max-columns11
                                                            arith-conflicts6
                                                            rlimit count1219
                                                            mk clause88
                                                            mk bool var80
                                                            arith-lower29
                                                            arith-diseq2
                                                            decisions13
                                                            arith-propagations5
                                                            propagations72
                                                            arith-bound-propagations-cheap5
                                                            arith-max-rows1
                                                            conflicts6
                                                            minimized lits3
                                                            final checks1
                                                            added eqs75
                                                            del clause32
                                                            arith eq adapter28
                                                            arith-upper27
                                                            time0.019000
                                                            memory72.410000
                                                            max memory81.950000
                                                            num allocs13737713775.000000
                                                            Expand
                                                            • start[0.035s]
                                                                let (_x_0 : bool) = not (( :var_0: ) = ( :var_1: )) in
                                                                (if not (_x_0 || ( :var_2: )) then 1 else 0) =
                                                                ((if ( :var_0: ) then 1 else 0) + (if ( :var_1: ) then 1 else 0)
                                                                 + (if ( :var_2: ) then 1 else 0))
                                                                -
                                                                (2 * (if _x_0 && ( :var_2: ) || ( :var_0: ) && ( :var_1: ) then 1 else 0))
                                                            • simplify

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

                                                                Termination proof

                                                                call `bad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)` from `bad_ripple_carry_adder a b cin`
                                                                originalbad_ripple_carry_adder a b cin
                                                                subbad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)
                                                                original ordinalOrdinal.Int (_cnt a)
                                                                sub ordinalOrdinal.Int (_cnt (List.tl a))
                                                                path[a <> [] && b <> []]
                                                                proof
                                                                detailed proof
                                                                ground_instances3
                                                                definitions0
                                                                inductions0
                                                                search_time
                                                                0.170s
                                                                details
                                                                Expand
                                                                smt_stats
                                                                num checks7
                                                                arith-make-feasible7
                                                                arith-max-columns13
                                                                arith-conflicts1
                                                                rlimit count2072
                                                                mk clause29
                                                                datatype occurs check26
                                                                mk bool var75
                                                                arith-lower4
                                                                datatype splits6
                                                                decisions30
                                                                propagations28
                                                                arith-max-rows5
                                                                conflicts8
                                                                datatype accessor ax9
                                                                datatype constructor ax14
                                                                final checks6
                                                                added eqs86
                                                                del clause14
                                                                arith eq adapter5
                                                                arith-upper6
                                                                memory69.710000
                                                                max memory81.950000
                                                                num allocs14003112877.000000
                                                                Expand
                                                                • start[0.170s]
                                                                    let (_x_0 : int) = count.list (const 0) a in
                                                                    let (_x_1 : bool list) = List.tl a in
                                                                    let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                    a <> [] && b <> [] && _x_0 >= 0 && _x_2 >= 0
                                                                    ==> not (_x_1 <> [] && (List.tl b) <> [])
                                                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                • simplify
                                                                  into
                                                                  let (_x_0 : bool list) = List.tl a in
                                                                  let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                  let (_x_2 : int) = count.list (const 0) a in
                                                                  (not (_x_0 <> [] && (List.tl b) <> [])
                                                                   || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                  || not (((a <> [] && b <> []) && _x_2 >= 0) && _x_1 >= 0)
                                                                  expansions
                                                                  []
                                                                  rewrite_steps
                                                                    forward_chaining
                                                                    • unroll
                                                                      expr
                                                                      (|`count.list (const 0)[0]`_3637| a_3622)
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|`count.list (const 0)[0]`_3637| (|get.::.1_3621| a_3622))
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                              (|`count.list (const 0)[0]`_3637| (|get.::.…
                                                                          expansions
                                                                          • Unsat

                                                                          In [23]:
                                                                          instance (fun a b -> int_of_bits (bad_ripple_carry_adder a b false) <> int_of_bits a + int_of_bits b)
                                                                          
                                                                          Out[23]:
                                                                          - : bool list -> bool list -> bool = <fun>
                                                                          module CX : sig val a : bool list val b : bool list end
                                                                          
                                                                          Instance (after 5 steps, 0.062s):
                                                                           let (a : bool list) = []
                                                                           let (b : bool list) = [true]
                                                                          
                                                                          Instance
                                                                          proof attempt
                                                                          ground_instances5
                                                                          definitions0
                                                                          inductions0
                                                                          search_time
                                                                          0.062s
                                                                          details
                                                                          Expand
                                                                          smt_stats
                                                                          num checks11
                                                                          arith-make-feasible54
                                                                          arith-max-columns30
                                                                          arith-conflicts3
                                                                          rlimit count5203
                                                                          arith-gcd-calls1
                                                                          arith-cheap-eqs33
                                                                          mk clause231
                                                                          datatype occurs check71
                                                                          mk bool var359
                                                                          arith-lower68
                                                                          arith-diseq28
                                                                          datatype splits26
                                                                          decisions108
                                                                          arith-propagations20
                                                                          arith-patches-success1
                                                                          propagations167
                                                                          arith-patches1
                                                                          arith-bound-propagations-cheap20
                                                                          arith-max-rows15
                                                                          conflicts19
                                                                          datatype accessor ax15
                                                                          minimized lits2
                                                                          arith-bound-propagations-lp17
                                                                          datatype constructor ax44
                                                                          final checks17
                                                                          added eqs429
                                                                          del clause88
                                                                          arith eq adapter65
                                                                          arith-upper60
                                                                          time0.001000
                                                                          memory54.470000
                                                                          max memory81.950000
                                                                          num allocs14705109783.000000
                                                                          Expand
                                                                          • start[0.062s]
                                                                              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_48 b_95)
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (int_of_bits_48 a_94)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (bad_ripple_carry_adder_80 a_94 b_95 false)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (int_of_bits_48 (bad_ripple_carry_adder_80 a_94 b_95 false))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (int_of_bits_48 (|get.::.1_3669| b_95))
                                                                                    expansions
                                                                                    • Sat (Some let (a : bool list) = [] let (b : bool list) = [true] )

                                                                                    Happy verifying!