AstraVer Toolset » Deductive Verification Tools for Linux Kernel

Why3 generates definition for Count2 predicate:

Inductive usCount2: (Pointer.pointer intP) -> Numbers.BinNums.Z -> Int32.t ->
  Numbers.BinNums.Z -> (map.Map.map (Pointer.pointer intP) Int32.t) ->
  Prop :=
  | usNil : forall (intP_intM_a_2_at_L:(map.Map.map (Pointer.pointer intP)
      Int32.t)), forall (a_0:(Pointer.pointer intP)), forall (v_0:Int32.t),
      forall (n_2:Numbers.BinNums.Z), (n_2 <= 0%Z)%Z -> (usCount2 a_0 n_2 v_0
      0%Z intP_intM_a_2_at_L)
  | usHit : forall (intP_intM_a_2_at_L:(map.Map.map (Pointer.pointer intP)
      Int32.t)), forall (a_1:(Pointer.pointer intP)), forall (v_1:Int32.t),
      forall (n_3:Numbers.BinNums.Z), forall (sum_0:Numbers.BinNums.Z),
      ((0%Z < n_3)%Z /\ (((map.Map.get intP_intM_a_2_at_L (Pointer.shift a_1
      (n_3 - 1%Z)%Z)) = v_1) /\ (usCount2 a_1 (n_3 - 1%Z)%Z v_1 sum_0
      intP_intM_a_2_at_L))) -> (usCount2 a_1 n_3 v_1 (sum_0 + 1%Z)%Z
      intP_intM_a_2_at_L)
  | usMiss : forall (intP_intM_a_2_at_L:(map.Map.map (Pointer.pointer intP)
      Int32.t)), forall (a_2:(Pointer.pointer intP)), forall (v_2:Int32.t),
      forall (n_4:Numbers.BinNums.Z), forall (sum_1:Numbers.BinNums.Z),
      ((0%Z < n_4)%Z /\ ((~ ((map.Map.get intP_intM_a_2_at_L
      (Pointer.shift a_2 (n_4 - 1%Z)%Z)) = v_2)) /\ (usCount2 a_2
      (n_4 - 1%Z)%Z v_2 sum_1 intP_intM_a_2_at_L))) -> (usCount2 a_2 n_4 v_2
      sum_1 intP_intM_a_2_at_L).

Vanilla Frama-C simplifies this to (->, let):

Inductive P_Count2 : farray addr Z -> addr -> Z -> Z -> Z -> Prop :=
    | Q_Nil: forall (i_1 i : Z), forall (t : farray addr Z),
        forall (a : addr), ((i <= 0)%Z) -> ((is_sint32 i_1%Z)) ->
        ((P_Count2 t a i%Z i_1%Z 0%Z))
    | Q_Hit: forall (i_1 i : Z), forall (t : farray addr Z),
        forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
        let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((0 < i_1)%Z) ->
        ((is_sint32 x_1)) -> ((P_Count2 t a x x_1 i%Z)) ->
        ((P_Count2 t a i_1%Z x_1 (1%Z + i%Z)%Z))
    | Q_Miss: forall (i_2 i_1 i : Z), forall (t : farray addr Z),
        forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
        (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((0 < i_1)%Z) ->
        ((is_sint32 i_2%Z)) -> ((P_Count2 t a x i_2%Z i%Z)) ->
        ((P_Count2 t a i_1%Z i_2%Z i%Z)).

Thus, the original deifinition:

    inductive Count2{L}(value_type *a, integer n, value_type v, integer sum) {
      case Nil{L}:
        \forall value_type *a, v, integer n;
          n <= 0 ==>
            Count2{L}(a, n, v, 0);
      case Hit{L}:
        \forall value_type *a, v, integer n, sum;
          0 < n && a[n-1] == v && Count2{L}(a, n-1, v, sum) ==>
            Count2{L}(a, n, v, sum + 1);
      case Miss{L}:
        \forall value_type *a, v, integer n, sum;
          0 < n && a[n-1] != v && Count2{L}(a, n-1, v, sum) ==>
            Count2{L}(a, n, v, sum);
    }

simplified to:

    inductive Count2{L}(value_type *a, integer n, value_type v, integer sum) {
      case Nil{L}:
        \forall value_type *a, v, integer n;
          n <= 0 ==>
            Count2{L}(a, n, v, 0);
      case Hit{L}:
        \forall value_type *a, v, integer n, sum;
        \let n1 = n - 1;
        \let an = a[n1];
          0 < n ==> Count2{L}(a, n1, an, sum) ==>
            Count2{L}(a, n, an, sum + 1);
      case Miss{L}:
       \forall value_type *a, v, integer n, sum;
         \let n1 = n - 1;
          0 < n ==> a[n1] != v ==> Count2{L}(a, n1, v, sum) ==>
            Count2{L}(a, n, v, sum);
    }

After the simplification the Coq proof can be as short as:

intros. induction H; auto with zarith.