Verifying a Ripple-Carry Adder in Imandra

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

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

The correctness theorem we'll prove is as follows:

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

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

Building the circuit in Imandra

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

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

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

 

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

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

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

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

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

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

Termination proof

call `ripple_carry_adder (List.tl a) (List.tl b) (adder_carry_out (List.hd a) (List.hd b) cin)` from `ripple_carry_adder a b cin`
originalripple_carry_adder a b cin
subripple_carry_adder (List.tl a) (List.tl b) (adder_carry_out (List.hd a) (List.hd b) cin)
original ordinalOrdinal.Int (Ordinal.count a)
sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
path[a <> [] && b <> []]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.020s
details
Expand
smt_stats
num checks8
arith assert lower8
arith pivots4
rlimit count2128
mk clause30
datatype occurs check22
mk bool var84
arith assert upper5
datatype splits6
decisions28
arith add rows6
propagations30
conflicts9
arith fixed eqs4
datatype accessor ax10
arith conflicts1
datatype constructor ax14
num allocs1054225
final checks6
added eqs87
del clause17
arith eq adapter6
memory6.330000
max memory6.330000
Expand
  • start[0.020s]
      (a <> [] && b <> [])
      && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
      ==> not ((List.tl a) <> [] && (List.tl b) <> [])
          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
             (Ordinal.Int (Ordinal.count a))
  • simplify
    into
    (not
     (((a <> [] && b <> []) && Ordinal.count a >= 0)
      && Ordinal.count (List.tl a) >= 0)
     || not ((List.tl a) <> [] && (List.tl b) <> []))
    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
       (Ordinal.Int (Ordinal.count a))
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`bool list`_1215|
                                              …
        expansions
        • unroll
          expr
          (|count_`bool list`_1215| (|get.::.1_1201| a_1202))
          expansions
          • unroll
            expr
            (|count_`bool list`_1215| a_1202)
            expansions
            • unsat
              (let ((a!1 (= (|count_`bool list`_1215| a_1202)
                            (+ 1 (|count_`bool list`_1215| (|get.:…

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

            In [6]:
            let zero = []
            let one = [true]
            let two = [false; true]
            
            Out[6]:
            val zero : 'a list = []
            val one : bool list = [true]
            val two : bool list = [false; true]
            
            In [7]:
            ripple_carry_adder zero zero false
            
            Out[7]:
            - : bool list = []
            
            In [8]:
            ripple_carry_adder one one false
            
            Out[8]:
            - : bool list = [false; true]
            
            In [9]:
            instance (fun a b -> ripple_carry_adder a b false = [false; false; false; true])
            
            Out[9]:
            - : bool list -> bool list -> bool = <fun>
            module CX : sig val a : bool list val b : bool list end
            
            Instance (after 4 steps, 0.015s):
             let (a : bool list) = [true; true; false]
             let (b : bool list) = [true; false; true]
            
            Instance
            proof attempt
            ground_instances4
            definitions0
            inductions0
            search_time
            0.015s
            details
            Expand
            smt_stats
            num checks9
            rlimit count4328
            mk clause200
            datatype occurs check68
            mk bool var191
            datatype splits13
            decisions66
            propagations218
            conflicts19
            datatype accessor ax27
            minimized lits1
            datatype constructor ax30
            num allocs4488557
            final checks13
            added eqs297
            del clause46
            memory7.520000
            max memory7.520000
            Expand
            • start[0.015s]
                ripple_carry_adder :var_0: :var_1: false =
                false :: (false :: (false :: (true :: …)))
            • unroll
              expr
              (ripple_carry_adder_25 a_37 b_38 false)
              expansions
              • unroll
                expr
                (let ((a!1 (and (= (not (|get.::.0_1232| a_37)) (|get.::.0_1232| b_38)) false)))
                  (ripple_carry_add…
                expansions
                • unroll
                  expr
                  (let ((a!1 (= (not (|get.::.0_1232| (|get.::.1_1233| a_37)))
                                (|get.::.0_1232| (|get.::…
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (not (|get.::.0_1232| (|get.::.1_1233| (|get.::.1_1233| a_37)))))
                          (a!3 (= (not (|ge…
                    expansions
                    • Sat (Some let (a : bool list) = [true; true; false] let (b : bool list) = [true; false; true] )

                    Relating bit sequences to natural numbers

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

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

                    Termination proof

                    call `int_of_bits (List.tl a)` from `int_of_bits a`
                    originalint_of_bits a
                    subint_of_bits (List.tl a)
                    original ordinalOrdinal.Int (Ordinal.count a)
                    sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
                    path[not (a = [])]
                    proof
                    detailed proof
                    ground_instances3
                    definitions0
                    inductions0
                    search_time
                    0.013s
                    details
                    Expand
                    smt_stats
                    num checks7
                    arith assert lower6
                    arith pivots4
                    rlimit count1908
                    mk clause11
                    datatype occurs check33
                    mk bool var58
                    arith assert upper4
                    datatype splits6
                    decisions16
                    arith add rows5
                    propagations10
                    conflicts7
                    arith fixed eqs3
                    datatype accessor ax5
                    arith conflicts1
                    datatype constructor ax8
                    num allocs9373565
                    final checks9
                    added eqs48
                    del clause5
                    arith eq adapter3
                    memory7.830000
                    max memory7.830000
                    Expand
                    • start[0.013s]
                        not (a = []) && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
                        ==> List.tl a = []
                            || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
                               (Ordinal.Int (Ordinal.count a))
                    • simplify
                      into
                      (not
                       ((not (a = []) && Ordinal.count a >= 0) && Ordinal.count (List.tl a) >= 0)
                       || List.tl a = [])
                      || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
                         (Ordinal.Int (Ordinal.count a))
                      expansions
                      []
                      rewrite_steps
                        forward_chaining
                        • unroll
                          expr
                          (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`bool list`_1254|
                                                                …
                          expansions
                          • unroll
                            expr
                            (|count_`bool list`_1254| (|get.::.1_1244| a_1245))
                            expansions
                            • unroll
                              expr
                              (|count_`bool list`_1254| a_1245)
                              expansions
                              • unsat
                                (let ((a!1 (= (|count_`bool list`_1254| a_1245)
                                              (+ 1 (|count_`bool list`_1254| (|get.:…

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

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

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

                              In [14]:
                              instance (fun a -> int_of_bits a = 256)
                              
                              Out[14]:
                              - : bool list -> bool = <fun>
                              module CX : sig val a : bool list end
                              
                              Instance (after 10 steps, 0.041s):
                               let (a : bool list) =
                                 [false; false; false; false; false; false; false; false; true]
                              
                              Instance
                              proof attempt
                              ground_instances10
                              definitions0
                              inductions0
                              search_time
                              0.041s
                              details
                              Expand
                              smt_stats
                              arith offset eqs13
                              num checks21
                              arith assert lower269
                              arith pivots69
                              rlimit count14247
                              mk clause605
                              datatype occurs check162
                              mk bool var1236
                              arith gcd tests10
                              arith assert upper256
                              datatype splits124
                              decisions190
                              arith add rows114
                              arith bound prop19
                              propagations708
                              conflicts82
                              arith fixed eqs66
                              datatype accessor ax108
                              minimized lits12
                              arith conflicts15
                              arith assert diseq131
                              datatype constructor ax133
                              num allocs16668160
                              final checks49
                              added eqs1395
                              del clause582
                              arith eq adapter276
                              memory8.840000
                              max memory8.840000
                              Expand
                              • start[0.041s] int_of_bits :var_0: = 256
                              • unroll
                                expr
                                (int_of_bits_42 a_46)
                                expansions
                                • unroll
                                  expr
                                  (int_of_bits_42 (|get.::.1_1260| a_46))
                                  expansions
                                  • unroll
                                    expr
                                    (int_of_bits_42 (|get.::.1_1260| (|get.::.1_1260| a_46)))
                                    expansions
                                    • unroll
                                      expr
                                      (int_of_bits_42 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))))
                                          (int_of_…
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))))
                                            (int_of_…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))))
                                              (int_of_…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))))
                                                (int_of_…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))))
                                                (let ((a!2…
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| (|get.::.1_1260| a_46))))))
                                                  (let ((a!2…
                                                  expansions
                                                  • Sat (Some let (a : bool list) = [false; false; false; false; false; false; false; false; true] )
                                                  In [15]:
                                                  int_of_bits (ripple_carry_adder CX.a CX.a false)
                                                  
                                                  Out[15]:
                                                  - : Z.t = 512
                                                  

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

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

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

                                                  In [16]:
                                                  theorem full_ripple_carry_adder_correct a b cin =
                                                    List.length a = List.length b ==>
                                                    int_of_bits (ripple_carry_adder a b cin) =
                                                    int_of_bits a + int_of_bits b + int_of_bit cin
                                                  [@@induct functional ripple_carry_adder]
                                                  
                                                  Out[16]:
                                                  val full_ripple_carry_adder_correct : bool list -> bool list -> bool -> bool =
                                                    <fun>
                                                  Goal:
                                                  
                                                  List.length a = List.length b
                                                  ==> int_of_bits (ripple_carry_adder a b cin) =
                                                      (int_of_bits a + int_of_bits b) + int_of_bit cin.
                                                  
                                                  1 nontautological subgoal.
                                                  
                                                  We shall induct according to a scheme derived from ripple_carry_adder.
                                                  
                                                  Induction scheme:
                                                  
                                                   (not (a <> [] && b <> []) ==> φ cin b a)
                                                   && ((a <> [] && b <> [])
                                                       && φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
                                                          (List.tl a)
                                                       ==> φ cin b a).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 2:
                                                  
                                                   H0. List.length a = List.length b
                                                  |---------------------------------------------------------------------------
                                                   C0. 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. a <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                   C2. 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. a <> []
                                                   C1. 0 = int_of_bits b
                                                   C2. cin
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits.
                                                  
                                                  Subgoal 2.3:
                                                  
                                                   H0. List.length a = 0
                                                   H1. a <> []
                                                  |---------------------------------------------------------------------------
                                                   C0. b <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                   C2. 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.2:
                                                  
                                                   H0. 0 = List.length b
                                                   H1. cin
                                                  |---------------------------------------------------------------------------
                                                   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. b = []
                                                   H1. cin
                                                  |---------------------------------------------------------------------------
                                                   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. List.length a = 0
                                                   H1. a <> []
                                                   H2. cin
                                                  |---------------------------------------------------------------------------
                                                   C0. b <> []
                                                   C1. 0 = int_of_bits a + int_of_bits b
                                                  
                                                  But simplification reduces this to true, using the definition of int_of_bits,
                                                  and the rewrite rule List.len_zero_is_empty.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. a <> []
                                                   H1. b <> []
                                                   H2. List.length (List.tl a) = List.length (List.tl b)
                                                       ==> int_of_bits
                                                           (ripple_carry_adder (List.tl a) (List.tl b)
                                                            (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                                                           =
                                                           (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                           + (if not (List.hd a) = List.hd b && cin || List.hd a && List.hd b
                                                              then 1 else 0)
                                                   H3. List.length a = List.length b
                                                  |---------------------------------------------------------------------------
                                                   int_of_bits (ripple_carry_adder a b cin) =
                                                   (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)
                                                  
                                                  But simplification reduces this to true, using the definitions of
                                                  List.length, int_of_bits and ripple_carry_adder.
                                                  
                                                   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
                                                  definitions33
                                                  inductions1
                                                  search_time
                                                  0.933s
                                                  Expand
                                                  • start[0.933s, "Goal"]
                                                      List.length :var_0: = List.length :var_1:
                                                      ==> int_of_bits (ripple_carry_adder :var_0: :var_1: :var_2:) =
                                                          (int_of_bits :var_0: + int_of_bits :var_1:)
                                                          + (if :var_2: then 1 else 0)
                                                  • subproof

                                                    not (List.length a = List.length b) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)
                                                    • start[0.933s, "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 <> []) ==> φ cin b a)
                                                              && ((a <> [] && b <> [])
                                                                  && φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
                                                                     (List.tl a)
                                                                  ==> φ cin b a)
                                                    • Split (((a <> [] && b <> [] || not (List.length a = List.length b))
                                                              || int_of_bits (ripple_carry_adder a b cin) =
                                                                 (int_of_bits a + int_of_bits b) + (if cin then 1 else 0))
                                                             && ((not
                                                                  ((a <> [] && b <> [])
                                                                   && (not (List.length (List.tl a) = List.length (List.tl b))
                                                                       || int_of_bits
                                                                          (ripple_carry_adder (List.tl a) (List.tl b)
                                                                           (not (List.hd a) = List.hd b && cin
                                                                            || List.hd a && List.hd b))
                                                                          =
                                                                          (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                          + (if not (List.hd a) = List.hd b && cin
                                                                                || List.hd a && List.hd b
                                                                             then 1 else 0)))
                                                                  || not (List.length a = List.length b))
                                                                 || int_of_bits (ripple_carry_adder a b cin) =
                                                                    (int_of_bits a + int_of_bits b) + (if cin then 1 else 0))
                                                             :cases [(not (List.length a = List.length b) || 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);
                                                                     (((not (a <> []) || not (b <> []))
                                                                       || not
                                                                          (not (List.length (List.tl a) = List.length (List.tl b))
                                                                           || int_of_bits
                                                                              (ripple_carry_adder (List.tl a) (List.tl b)
                                                                               (not (List.hd a) = List.hd b && cin
                                                                                || List.hd a && List.hd b))
                                                                              =
                                                                              (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                              + (if not (List.hd a) = List.hd b && cin
                                                                                    || List.hd a && List.hd b
                                                                                 then 1 else 0)))
                                                                      || not (List.length a = List.length b))
                                                                     || int_of_bits (ripple_carry_adder a b cin) =
                                                                        (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)])
                                                      • subproof
                                                        (((not (a <> []) || not (b <> [])) || not (not (List.length (List.tl a) = List.length (List.tl b)) || int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)) = (int_of_bits (List.tl a) + int_of_bits (List.tl b)) + (if not (List.hd a) = List.hd b && cin || List.hd a && List.hd b then 1 else 0))) || not (List.length a = List.length b)) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)
                                                        • start[0.931s, "1"]
                                                            (((not (a <> []) || not (b <> []))
                                                              || not
                                                                 (not (List.length (List.tl a) = List.length (List.tl b))
                                                                  || int_of_bits
                                                                     (ripple_carry_adder (List.tl a) (List.tl b)
                                                                      (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                                                                     =
                                                                     (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                     + (if not (List.hd a) = List.hd b && cin || List.hd a && List.hd b
                                                                        then 1 else 0)))
                                                             || not (List.length a = List.length b))
                                                            || int_of_bits (ripple_carry_adder a b cin) =
                                                               (int_of_bits a + int_of_bits b) + (if cin then 1 else 0)
                                                        • simplify
                                                          into
                                                          true
                                                          expansions
                                                          [List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, List.length, List.length, List.length, List.length,
                                                           List.length, 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
                                                        • 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[0.932s, "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
                                                            (((((not (0 = List.length b) || a <> []) || 0 = int_of_bits a + int_of_bits b)
                                                               || cin)
                                                              && ((((not (List.length a = 0) || b <> []) || not (a <> []))
                                                                   || 0 = int_of_bits a + int_of_bits b)
                                                                  || cin))
                                                             && (((not (0 = List.length b) || a <> [])
                                                                  || 0 = int_of_bits a + int_of_bits b)
                                                                 || not cin))
                                                            && ((((not (List.length a = 0) || b <> []) || not (a <> []))
                                                                 || 0 = int_of_bits a + int_of_bits b)
                                                                || not cin)
                                                            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.023s
                                                      details
                                                      Expand
                                                      smt_stats
                                                      num checks1
                                                      arith assert lower60
                                                      arith pivots2
                                                      rlimit count1505
                                                      mk clause160
                                                      mk bool var133
                                                      arith assert upper60
                                                      decisions17
                                                      propagations158
                                                      conflicts17
                                                      minimized lits12
                                                      arith conflicts16
                                                      arith assert diseq1
                                                      num allocs2904834373
                                                      added eqs98
                                                      del clause136
                                                      arith eq adapter59
                                                      memory27.040000
                                                      max memory45.710000
                                                      Expand
                                                      • start[0.023s]
                                                          (if not (not (:var_0: = :var_1:) = :var_2:) then 1 else 0) =
                                                          (((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0))
                                                           + (if :var_2: then 1 else 0))
                                                          -
                                                          (2
                                                           * (if not (:var_0: = :var_1:) && :var_2: || :var_0: && :var_1: then 1
                                                              else 0))
                                                      • simplify

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

                                                            (let ((a!1 (= (ite (= (= a_1809 b_1810) cin_1811) 1 0) 1))
                                                                  (a!2 (<= (ite (= (= a_1809 b_1810) …

                                                          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 <> []) ==> φ cin b a)
                                                           && ((a <> [] && b <> [])
                                                               && φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
                                                                  (List.tl a)
                                                               ==> φ cin b a).
                                                          
                                                          2 nontautological subgoals.
                                                          
                                                          Subgoal 2:
                                                          
                                                           H0. List.length a = List.length b
                                                          |---------------------------------------------------------------------------
                                                           C0. 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. a <> []
                                                           C1. 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                           C2. 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. a <> []
                                                           C1. 0 = int_of_bits b + int_of_bit false
                                                           C2. cin
                                                          
                                                          This simplifies, using the definition of int_of_bits to:
                                                          
                                                          Subgoal 2.4'':
                                                          
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> []
                                                           C1. 0 = int_of_bit false
                                                           C2. cin
                                                          
                                                          But we verify Subgoal 2.4'' by recursive unrolling.
                                                          
                                                          Subgoal 2.3:
                                                          
                                                           H0. List.length a = 0
                                                           H1. a <> []
                                                          |---------------------------------------------------------------------------
                                                           C0. b <> []
                                                           C1. 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                           C2. 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.2:
                                                          
                                                           H0. 0 = List.length b
                                                           H1. cin
                                                          |---------------------------------------------------------------------------
                                                           C0. a <> []
                                                           C1. int_of_bit true = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                          
                                                          This simplifies, using the definition of int_of_bits, and the rewrite rule
                                                          List.len_zero_is_empty to:
                                                          
                                                          Subgoal 2.2':
                                                          
                                                           H0. b = []
                                                           H1. cin
                                                          |---------------------------------------------------------------------------
                                                           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. List.length a = 0
                                                           H1. a <> []
                                                           H2. cin
                                                          |---------------------------------------------------------------------------
                                                           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 definition of int_of_bits,
                                                          and the rewrite rule List.len_zero_is_empty.
                                                          
                                                          Subgoal 1:
                                                          
                                                           H0. a <> []
                                                           H1. b <> []
                                                           H2. List.length (List.tl a) = List.length (List.tl b)
                                                               ==> int_of_bits
                                                                   (ripple_carry_adder (List.tl a) (List.tl b)
                                                                    (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                                                                   =
                                                                   (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                   + int_of_bit
                                                                     (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)
                                                           H3. List.length a = List.length b
                                                          |---------------------------------------------------------------------------
                                                           int_of_bits (ripple_carry_adder a b cin) =
                                                           (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                          
                                                          But simplification reduces this to true, using the definitions of
                                                          List.length, int_of_bits and ripple_carry_adder, and the rewrite rule
                                                          single_adder_circuit_correct.
                                                          
                                                           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
                                                          definitions27
                                                          inductions1
                                                          search_time
                                                          0.822s
                                                          details
                                                          Expand
                                                          smt_stats
                                                          rlimit count12419
                                                          mk bool var5
                                                          memory39.970000
                                                          max memory60.940000
                                                          num allocs4655363096.000000
                                                          Expand
                                                          • start[0.822s, "Goal"]
                                                              List.length :var_0: = List.length :var_1:
                                                              ==> int_of_bits (ripple_carry_adder :var_0: :var_1: :var_2:) =
                                                                  (int_of_bits :var_0: + int_of_bits :var_1:) + int_of_bit :var_2:
                                                          • subproof

                                                            not (List.length a = List.length b) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                            • start[0.822s, "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 <> []) ==> φ cin b a)
                                                                      && ((a <> [] && b <> [])
                                                                          && φ (adder_carry_out (List.hd a) (List.hd b) cin) (List.tl b)
                                                                             (List.tl a)
                                                                          ==> φ cin b a)
                                                            • Split (((a <> [] && b <> [] || not (List.length a = List.length b))
                                                                      || int_of_bits (ripple_carry_adder a b cin) =
                                                                         (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                                                     && ((not
                                                                          ((a <> [] && b <> [])
                                                                           && (not (List.length (List.tl a) = List.length (List.tl b))
                                                                               || int_of_bits
                                                                                  (ripple_carry_adder (List.tl a) (List.tl b)
                                                                                   (not (List.hd a) = List.hd b && cin
                                                                                    || List.hd a && List.hd b))
                                                                                  =
                                                                                  (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                                  + int_of_bit
                                                                                    (not (List.hd a) = List.hd b && cin
                                                                                     || List.hd a && List.hd b)))
                                                                          || not (List.length a = List.length b))
                                                                         || int_of_bits (ripple_carry_adder a b cin) =
                                                                            (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                                                     :cases [(not (List.length a = List.length b) || a <> [] && b <> [])
                                                                             || int_of_bits (ripple_carry_adder a b cin) =
                                                                                (int_of_bits a + int_of_bits b) + int_of_bit cin;
                                                                             (((not (a <> []) || not (b <> []))
                                                                               || not
                                                                                  (not (List.length (List.tl a) = List.length (List.tl b))
                                                                                   || int_of_bits
                                                                                      (ripple_carry_adder (List.tl a) (List.tl b)
                                                                                       (not (List.hd a) = List.hd b && cin
                                                                                        || List.hd a && List.hd b))
                                                                                      =
                                                                                      (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                                      + int_of_bit
                                                                                        (not (List.hd a) = List.hd b && cin
                                                                                         || List.hd a && List.hd b)))
                                                                              || not (List.length a = List.length b))
                                                                             || int_of_bits (ripple_carry_adder a b cin) =
                                                                                (int_of_bits a + int_of_bits b) + int_of_bit cin])
                                                              • subproof
                                                                (((not (a <> []) || not (b <> [])) || not (not (List.length (List.tl a) = List.length (List.tl b)) || int_of_bits (ripple_carry_adder (List.tl a) (List.tl b) (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)) = (int_of_bits (List.tl a) + int_of_bits (List.tl b)) + int_of_bit (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))) || not (List.length a = List.length b)) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                                • start[0.820s, "1"]
                                                                    (((not (a <> []) || not (b <> []))
                                                                      || not
                                                                         (not (List.length (List.tl a) = List.length (List.tl b))
                                                                          || int_of_bits
                                                                             (ripple_carry_adder (List.tl a) (List.tl b)
                                                                              (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b))
                                                                             =
                                                                             (int_of_bits (List.tl a) + int_of_bits (List.tl b))
                                                                             + int_of_bit
                                                                               (not (List.hd a) = List.hd b && cin || List.hd a && List.hd b)))
                                                                     || not (List.length a = List.length b))
                                                                    || int_of_bits (ripple_carry_adder a b cin) =
                                                                       (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                                • simplify
                                                                  into
                                                                  true
                                                                  expansions
                                                                  [List.length, List.length, List.length, List.length, List.length,
                                                                   List.length, List.length, List.length, List.length, List.length,
                                                                   int_of_bits, int_of_bits, int_of_bits, ripple_carry_adder]
                                                                  rewrite_steps
                                                                  single_adder_circuit_correct
                                                                  forward_chaining
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                                  • List.len_nonnegative
                                                              • subproof
                                                                (not (List.length a = List.length b) || a <> [] && b <> []) || int_of_bits (ripple_carry_adder a b cin) = (int_of_bits a + int_of_bits b) + int_of_bit cin
                                                                • start[0.820s, "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
                                                                  (((((not (0 = List.length b) || a <> [])
                                                                      || 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                                                     || cin)
                                                                    && ((((not (List.length a = 0) || b <> []) || not (a <> []))
                                                                         || 0 = (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                                                        || cin))
                                                                   && (((not (0 = List.length b) || a <> [])
                                                                        || int_of_bit true = (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                                                       || not cin))
                                                                  && ((((not (List.length a = 0) || b <> []) || not (a <> []))
                                                                       || int_of_bit true = (int_of_bits a + int_of_bits b) + int_of_bit cin)
                                                                      || not cin)
                                                                  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.023s):
                                                             let (a : bool) = true
                                                             let (b : bool) = true
                                                             let (cin : bool) = true
                                                            
                                                            Refuted
                                                            proof attempt
                                                            ground_instances0
                                                            definitions0
                                                            inductions0
                                                            search_time
                                                            0.023s
                                                            details
                                                            Expand
                                                            smt_stats
                                                            num checks1
                                                            arith assert lower5
                                                            arith pivots2
                                                            rlimit count761
                                                            mk clause39
                                                            mk bool var38
                                                            arith assert upper7
                                                            decisions4
                                                            propagations14
                                                            arith fixed eqs1
                                                            arith assert diseq1
                                                            final checks1
                                                            added eqs9
                                                            del clause2
                                                            arith eq adapter6
                                                            memory25.770000
                                                            max memory69.600000
                                                            num allocs9011435695.000000
                                                            Expand
                                                            • start[0.023s]
                                                                (if not (not (:var_0: = :var_1:) || :var_2:) then 1 else 0) =
                                                                (((if :var_0: then 1 else 0) + (if :var_1: then 1 else 0))
                                                                 + (if :var_2: then 1 else 0))
                                                                -
                                                                (2
                                                                 * (if not (:var_0: = :var_1:) && :var_2: || :var_0: && :var_1: then 1
                                                                    else 0))
                                                            • simplify

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

                                                                Termination proof

                                                                call `bad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)` from `bad_ripple_carry_adder a b cin`
                                                                originalbad_ripple_carry_adder a b cin
                                                                subbad_ripple_carry_adder (List.tl a) (List.tl b) (bad_adder_carry_out (List.hd a) (List.hd b) cin)
                                                                original ordinalOrdinal.Int (Ordinal.count a)
                                                                sub ordinalOrdinal.Int (Ordinal.count (List.tl a))
                                                                path[a <> [] && b <> []]
                                                                proof
                                                                detailed proof
                                                                ground_instances3
                                                                definitions0
                                                                inductions0
                                                                search_time
                                                                0.016s
                                                                details
                                                                Expand
                                                                smt_stats
                                                                num checks8
                                                                arith assert lower8
                                                                arith pivots4
                                                                rlimit count2128
                                                                mk clause30
                                                                datatype occurs check22
                                                                mk bool var84
                                                                arith assert upper5
                                                                datatype splits6
                                                                decisions28
                                                                arith add rows6
                                                                propagations30
                                                                conflicts9
                                                                arith fixed eqs4
                                                                datatype accessor ax10
                                                                arith conflicts1
                                                                datatype constructor ax14
                                                                final checks6
                                                                added eqs87
                                                                del clause17
                                                                arith eq adapter6
                                                                memory25.970000
                                                                max memory69.600000
                                                                num allocs9170626213.000000
                                                                Expand
                                                                • start[0.016s]
                                                                    (a <> [] && b <> [])
                                                                    && Ordinal.count a >= 0 && Ordinal.count (List.tl a) >= 0
                                                                    ==> not ((List.tl a) <> [] && (List.tl b) <> [])
                                                                        || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
                                                                           (Ordinal.Int (Ordinal.count a))
                                                                • simplify
                                                                  into
                                                                  (not
                                                                   (((a <> [] && b <> []) && Ordinal.count a >= 0)
                                                                    && Ordinal.count (List.tl a) >= 0)
                                                                   || not ((List.tl a) <> [] && (List.tl b) <> []))
                                                                  || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl a)))
                                                                     (Ordinal.Int (Ordinal.count a))
                                                                  expansions
                                                                  []
                                                                  rewrite_steps
                                                                    forward_chaining
                                                                    • unroll
                                                                      expr
                                                                      (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`bool list`_2183|
                                                                                                            …
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|count_`bool list`_2183| (|get.::.1_2169| a_2170))
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|count_`bool list`_2183| a_2170)
                                                                          expansions
                                                                          • unsat
                                                                            (let ((a!1 (= (|count_`bool list`_2183| a_2170)
                                                                                          (+ 1 (|count_`bool list`_2183| (|get.:…

                                                                          In [23]:
                                                                          instance (fun a b -> int_of_bits (bad_ripple_carry_adder a b false) <> int_of_bits a + int_of_bits b)
                                                                          
                                                                          Out[23]:
                                                                          - : bool list -> bool list -> bool = <fun>
                                                                          module CX : sig val a : bool list val b : bool list end
                                                                          
                                                                          Instance (after 5 steps, 0.022s):
                                                                           let (a : bool list) = []
                                                                           let (b : bool list) = [true]
                                                                          
                                                                          Instance
                                                                          proof attempt
                                                                          ground_instances5
                                                                          definitions0
                                                                          inductions0
                                                                          search_time
                                                                          0.022s
                                                                          details
                                                                          Expand
                                                                          smt_stats
                                                                          arith offset eqs5
                                                                          num checks11
                                                                          arith assert lower56
                                                                          arith patches_succ1
                                                                          arith pivots42
                                                                          rlimit count7199
                                                                          mk clause191
                                                                          datatype occurs check70
                                                                          mk bool var347
                                                                          arith gcd tests19
                                                                          arith assert upper80
                                                                          datatype splits32
                                                                          decisions154
                                                                          arith add rows121
                                                                          arith bound prop10
                                                                          propagations191
                                                                          arith patches6
                                                                          conflicts19
                                                                          arith fixed eqs22
                                                                          datatype accessor ax18
                                                                          arith conflicts1
                                                                          arith assert diseq26
                                                                          datatype constructor ax40
                                                                          final checks24
                                                                          added eqs380
                                                                          del clause94
                                                                          arith ineq splits3
                                                                          arith eq adapter61
                                                                          memory26.530000
                                                                          max memory69.600000
                                                                          num allocs9331681795.000000
                                                                          Expand
                                                                          • start[0.022s]
                                                                              not
                                                                              (int_of_bits (bad_ripple_carry_adder :var_0: :var_1: false) =
                                                                               int_of_bits :var_0: + int_of_bits :var_1:)
                                                                          • unroll
                                                                            expr
                                                                            (int_of_bits_42 b_81)
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (int_of_bits_42 a_80)
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (bad_ripple_carry_adder_72 a_80 b_81 false)
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (int_of_bits_42 (bad_ripple_carry_adder_72 a_80 b_81 false))
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (int_of_bits_42 (|get.::.1_2190| b_81))
                                                                                    expansions
                                                                                    • Sat (Some let (a : bool list) = [] let (b : bool list) = [true] )

                                                                                    Happy verifying!