Missing RBTree axioms

[Pat-Lafon]

I've needed to add 2 axioms to get the following subtyping check to go through. It corresponds to a subtyping check between missing coverage and the RBLeaf term(Noting the direction, the reverse case returns true as expected).

let[@axiom] rbtree_rb_leaf_num_black_0_second (l : int rbtree) (n : int) =
  (rb_leaf l) #==> (num_black l 0)

let[@axiom] rbtree_rb_leaf_no_red_red (l : int rbtree) (l1 : int rbtree) =
  (rb_leaf l) #==> (no_red_red l)

The testcase:

let[@assert] rty1 =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  ((h == 0
   && (not (rb_root_color v false))
   && (not (rb_root_color v true))
   && color)
   && num_black v h && no_red_red v
   &&
   if color then not (rb_root_color v true)
   else (h == 0) #==> (not (rb_root_color v false))
    : [%v: int rbtree])
    [@under]

let[@assert] rty2 =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  (h == 0 && color && rb_leaf v
   &&
   if color then not (rb_root_color v true)
   else (h == 0) #==> (not (rb_root_color v false))
    : [%v: int rbtree])
    [@under]

[Pat-Lafon]

For subtyping with the num_black predicate, I've needed to add the following axiom to describe how the number of black nodes for a root with color true can be computed by the number of black nodes in each branch(when equal).

let[@axiom] num_black_root_from_lt_rt (v : int rbtree) (lt : int rbtree)
    (rt : int rbtree) (h : int) =
  (num_black lt h && num_black rt h && rb_rch v rt && rb_lch v lt && rb_root_color v true)
  #==> (num_black v h)

with the following test case simple test case(an rbtree of just a root and two leafs has 0 black nodes):

let[@assert] rty1 =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  ((not (rb_root_color v false)) && rb_root_color v true && num_black v 0
    : [%v: int rbtree])
    [@under]

let[@assert] rty2 =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  (fun ((t [@exists]) : int rbtree) ->
     rb_leaf t && rb_root_color v true
     && (not (rb_root_color v false))
     && rb_lch v t
     && rb_rch v t
    : [%v: int rbtree])
    [@under]

[Pat-Lafon]

I would speculate then there should be an axiom for the alternative case where the node color is false(black)

let[@axiom] num_black_root_from_lt_rt_plus_1 (v : int rbtree) (lt : int rbtree)
    (rt : int rbtree) (h : int) =
  (num_black lt h && num_black rt h && rb_rch v rt && rb_lch v lt && rb_root_color v false)
  #==> (num_black v (h+1))

[Pat-Lafon]

An axiom for deriving no_red_red when the root is black

let[@axiom] no_red_red_given_lt_rt_black_root (v : int rbtree) (lt : int rbtree)
    (rt : int rbtree) =
  (no_red_red lt && no_red_red rt && rb_lch v lt && rb_rch v rt
 && rb_root_color v false)
  #==> (no_red_red v)

with a test case

let[@assert] rty1 =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  (rb_root_color v false
   && (not (rb_root_color v true))
   && no_red_red v
    : [%v: int rbtree])
    [@under]

let[@assert] rty2 =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  (fun (* ((n [@exists]) : int)  *) ((t [@exists]) : int rbtree) ->
     rb_leaf t && not (rb_root_color v true) && rb_root_color v false
     && rb_lch v t
     && rb_rch v t
    : [%v: int rbtree])
    [@under]

And an axiom for when the root is red:

let[@axiom] no_red_red_given_lt_rt_red_root (v : int rbtree) (lt : int rbtree)
    (rt : int rbtree) =
  (no_red_red lt && no_red_red rt && rb_lch v lt && rb_rch v rt
  && (not (rb_root_color lt true))
  && (not (rb_root_color rt true))
  && rb_root_color v true)
  #==> (no_red_red v)

[Pat-Lafon]

One more axiom I have needed is saying that trees that are not leafs or trees that are roots have a left and right sub tree.

There are two potential axioms for this(that should be equivalent):

let[@axiom] rbtree_root_lch_rch (l : int rbtree) (x : int) (l1 : int rbtree)
    (l2 : int rbtree) =
  (rb_root l x) #==> (rb_lch l l1 && rb_rch l l2)

let[@axiom] rbtree_root_lch_rch (l : int rbtree) (l1 : int rbtree)
    (l2 : int rbtree) =
  (not (rb_leaf l)) #==> (rb_lch l l1 && rb_rch l l2)

I was only successful with one of them because of the axiom filtering in check.ml... https://github.com/zhezhouzz/underapproximation_type/blob/94d0f056488c98bfd9177813c56237f8be466222/backend/check.ml#L63-L86 should also extend the rbtree method predicates

[Pat-Lafon]

I've gone and verified my RBTree axioms in Coq and found an issue in an above axiom and two axioms that were previously included.

The above axiom should be:

let[@axiom] rbtree_root_lch_rch (l : int rbtree) (x : int)
    ((l1 [@exists]) : int rbtree) ((l2 [@exists]) : int rbtree) =
  (rb_root l x) #==> (rb_lch l l1 && rb_rch l l2)

(Which says that there exists an l1, l2, whereas before it was accidentally forall l1, l2).

Additionally, the axioms num_black_root_black_0_lt_leaf and num_black_root_black_0_rt_leaf currently do not also state that the root node is also no_red_red v which is required for soundness:

let[@axiom] num_black_root_black_0_lt_leaf (v : int rbtree) (lt : int rbtree) =
  (no_red_red v && num_black v 0 && rb_lch v lt) #==> (rb_leaf lt)

let[@axiom] num_black_root_black_0_rt_leaf (v : int rbtree) (rt : int rbtree) =
  (no_red_red v && num_black v 0 && rb_rch v rt) #==> (rb_leaf rt)

The full proofs for my current set of rbtree axioms and proofs showing the negation of the above false axioms can be found here: https://github.com/Pat-Lafon/underapproximation_type/blob/e86470a1d897b578dccd05dc0ce30d50aecabd1f/data/validation/proofs/rbtree.v