Node reachability theory

NodeTestSandbox.fst

module NodeTestSandbox

open FStar.Seq
open FStar.Seq.Base

open FStar.IntegerIntervals

type address = UInt32.t

type address_list = seq address

let rec is_set (#t:eqtype) (p: seq t) 
  : Tot bool (decreases length p) 
  = (length p = 0) || (not (mem (head p) (tail p)) && is_set (tail p))
  
let is_address_set (l: seq address) : bool = is_set l

let address_set = v: address_list { is_address_set v }

let rec address_set_duplicate_is_nonsense (s: address_set) (i j:under (length s))
  : Lemma (requires (i<>j) /\ (index s i == index s j))
          (ensures False)
          (decreases length s) = 
  if length s > 1 then begin
    if i=0 then assert (index s j == index (tail s) (j-1))
    else if j=0 then assert (index s i == index (tail s) (i-1))
    else address_set_duplicate_is_nonsense (tail s) (i-1) (j-1)   
  end

type node = address & address_set

let address_of (n:node) = fst n
let adjacent_of (n:node) = snd n

type node_list = seq node

private let rec node_address_seq (l: node_list) 
  : Tot (aseq:address_list{length aseq = length l}) (decreases length l)
  = if length l = 0 then empty
    else cons (fst (head l)) (node_address_seq (tail l))

private let node_address_seq_lemma (l: node_list)
  : Lemma (requires length l > 0)
          (ensures node_address_seq (tail l) == tail (node_address_seq l)) 
  = lemma_eq_elim (node_address_seq (tail l)) (tail (node_address_seq l))  

private let rec node_address_seq_index_lemma (l: node_list) (i: nat{i<length l})
  : Lemma (requires length l > 0)
          (ensures fst (index l i) == index (node_address_seq l) i)
          (decreases length l) = 
  if (i>0) && (length l > 1) then node_address_seq_index_lemma (tail l) (i-1)

private let rec node_address_seq_mem (l: node_list) (n:node {mem n l})
  : Lemma (ensures mem (fst n) (node_address_seq l))
          (decreases length l) = 
  if length l > 0 && not (n = head l) then begin 
    node_address_seq_mem (tail l) n;
    lemma_eq_elim (node_address_seq (tail l)) (tail (node_address_seq l)) 
  end

let is_node_set (e: node_list) = is_address_set (node_address_seq e)

let node_set = e: node_list{is_node_set e}

let node_set_tail_is_node_set (e: node_set) 
  : Lemma (requires length e > 0)
          (ensures is_node_set (tail e)) 
          (decreases length e) = node_address_seq_lemma e 

let node_set_head_not_in_tail (e: node_set) 
  : Lemma (requires length e > 0)
          (ensures not (mem (head e) (tail e))) 
          (decreases length e) = 
  if length e < 2 then () else begin
    if mem (head e) (tail e) then begin
      let i = Seq.Properties.index_mem (head e) (tail e) in
      node_address_seq_index_lemma e (i+1);
      node_address_seq_index_lemma e 0;
      let na : address_set = node_address_seq e in
      address_set_duplicate_is_nonsense na 0 (i+1)
    end   
  end

let node_set_tail_has_address (e:node_set) (x:address)
  : Lemma (requires mem x (node_address_seq e))
          (ensures (x = fst (head e)) <> mem x (node_address_seq (tail e))) = 
  node_address_seq_lemma e

let address_mem  (x: address) (vs: address_list)
  : Tot (b:bool{b = true <==> mem x vs}) 
  = if mem x vs
    then let _ = mem_index x vs in true 
    else false  

let node_mem (e:node) (es: node_list)
  : Tot (b:bool{b = true <==> mem e es}) = mem e es 

noeq type state = {
 addresses : address_set; 
 nodes     : e : node_set { 
   forall (x:node). node_mem x e ==> address_mem (fst x) addresses 
                                   /\
                        (forall y. Seq.mem y (snd x) ==> address_mem y addresses)
 };                            
}

let rec mem_nodes_pattern (g:state) (n: node{mem n g.nodes})
  : Lemma (ensures mem (fst n) (node_address_seq g.nodes)) 
          (decreases length g.nodes)
          [SMTPat(mem n g.nodes)] = 
  node_set_tail_is_node_set g.nodes;
  if head g.nodes = n then () 
  else begin
    mem_nodes_pattern { addresses = g.addresses; nodes = tail g.nodes } n;
    node_address_seq_lemma g.nodes
  end

let is_valid_state_address (g: state) 
                           (x: address) 
  : Tot (b: bool {b = true <==> address_mem x g.addresses})
  = address_mem x (g.addresses) 

let rec find_node (g:state) (x:address)
  : Pure node (requires mem x (node_address_seq g.nodes))
              (ensures fun n -> (fst n == x) /\ mem n g.nodes)
              (decreases length g.nodes) =
  node_set_tail_has_address g.nodes x;
  if fst (head g.nodes) = x then head g.nodes
  else (node_set_tail_is_node_set g.nodes;
       find_node { addresses = g.addresses; nodes = tail g.nodes } x)

let inequal_nodes_means_inequal_addresses (nodes:node_set) (m n: (z:node{mem z nodes}))
  : Lemma (requires m <> n)
          (ensures fst m <> fst n)
          (decreases length nodes) = 
  if fst m = fst n then begin
    let i = Seq.Properties.index_mem m nodes in
    let j = Seq.Properties.index_mem n nodes in
    node_address_seq_index_lemma nodes i;
    node_address_seq_index_lemma nodes j;
    let na : address_set = node_address_seq nodes in
    address_set_duplicate_is_nonsense na i j       
  end

let rec find_node_of_node_fst (g:state) (n: node)
  : Lemma (requires mem n g.nodes) 
          (ensures find_node g (address_of n) == n)
          (decreases length g.nodes) =
  if length g.nodes = 1 then () else begin
    node_set_tail_is_node_set g.nodes;
    if head g.nodes = n then () else begin    
      inequal_nodes_means_inequal_addresses g.nodes (head g.nodes) n;   
      let sub = {addresses=g.addresses; nodes=tail g.nodes} in
      find_node_of_node_fst sub n;
      assert (find_node g (fst n) == find_node sub (fst n));
      ()
    end
  end

let rec get_adjacent_addresses (g: state) (x:address)
  : Pure address_set (requires mem x (node_address_seq g.nodes))
                     (ensures fun s -> (s == adjacent_of (find_node g x)) /\
                                    (forall a. mem a s ==> mem a g.addresses))
                     (decreases length g.nodes) = 
  if length g.nodes = 0 then empty
  else begin
    if fst (head g.nodes) = x then snd (head g.nodes)
    else begin
      node_set_tail_is_node_set g.nodes;
      let tl : node_set = tail g.nodes in 
      node_set_tail_has_address g.nodes x; 
      get_adjacent_addresses ({ addresses = g.addresses; nodes = tl }) x
    end
  end

let adjacent_addresses_lemma (g:state) (n: node)
  : Lemma (requires mem n g.nodes)
          (ensures (node_address_seq_mem g.nodes n;          
                   get_adjacent_addresses g (address_of n) == adjacent_of n)) = 
  assert (address_mem (fst n) (g.addresses));
  node_address_seq_mem g.nodes n;
  node_set_tail_has_address g.nodes (fst n);
  find_node_of_node_fst g n

let state_has_arc (g: state) (from to: address) : Tot (b:bool { b=true <==>
    (from `mem` node_address_seq g.nodes) /\
    (to `mem` get_adjacent_addresses g from)
  }) 
  = (from `mem` node_address_seq g.nodes) 
 && (to `mem` get_adjacent_addresses g from)
 
noeq type reach (g:state) 
                (x:address{ is_valid_state_address g x}) 
                (y:address{ is_valid_state_address g y})
                =                 
  | Target : (n:node { mem n g.nodes 
                     /\ fst n == x 
                     /\ fst n == y }) 
    -> reach g x y
  | Step   : (t:node { mem t g.nodes
                     /\ mem y (snd t)  })
    -> reach g x (fst t) 
    -> reach g x y

let simple_test_lemma (g:state) 
              (x y: (t: address {is_valid_state_address g t})) 
              (r: reach g x y{Step? r})
  : Lemma (fst (Step?.t r) `state_has_arc g` y) = 
  match r with 
  | Step node r ->  
    
    node_address_seq_mem g.nodes node;
    assert (mem node g.nodes);
    adjacent_addresses_lemma g node;
    assert (get_adjacent_addresses g (address_of node) == adjacent_of node); 
    assert (y `mem` get_adjacent_addresses g (address_of node))


val reachfunc: (g:state) ->
               (x:address{ is_valid_state_address g x}) ->
               (y:address{ is_valid_state_address g y}) ->
               (r: reach g x y) ->
               Tot bool
               
let reachfunc g x y r : Tot bool  = true

let test (g:state) 
         (x:address{ is_valid_state_address g x}) 
         (y:address{ is_valid_state_address g y})
         (r: reach g x y) 
  : Tot bool =
  match r with
  | Target n -> true
  | Step t r -> simple_test_lemma g x y (Step t r);
               assert ( state_has_arc g (fst t) y); 
               assert (exists (r':reach g x (fst t)). reachfunc g x (fst t) r);
               true