(* Why3 specification file for selected code in the sudoers crate.
   All proof goals generated by Why3 1.5.1 can be discharged using CVC4 1.8 *)

module Sudoers

use array.Array
use option.Option
use ref.Ref
use int.Int

(* loose models for the types in sudoers::Ast *)
type metavar 'a = All | Only 'a
type qualified 'a = Yes 'a | No 'a
type spec 'tag 'a = { inner: qualified (metavar 'a); info: 'tag }

predicate contains (pred: 'a -> bool) (a: array 'a)
  = exists i. 0 <= i < length a /\ pred a[i]

function who (item: spec 'tag 'a): metavar 'a
  = match item.inner with
    | Yes x -> x
    | No x -> x
    end

function condition (item: spec 'tag 'a): option 'tag
  = match item with
    | { inner = Yes _; info = tag } -> Some tag
    | _ -> None
    end

function matched_by (pred: 'a -> bool) (item: spec 'tag 'a): bool
  = match who item with
    | All -> true
    | Only x -> pred x
    end

let function bool_then (b: bool) (x: 'a): option 'a
  = if b then Some x else None

predicate final_match (pred: 'a -> bool) (a: array 'a) (f: 'a -> 'b) (x: 'b)
  = exists i. 0 <= i < length a /\ pred a[i] /\ f a[i] = x /\ forall k. i < k < length a -> not pred a[k]

(* Why3 model of the sudoers::find_item function *)
let find_item (items: array (spec 'tag 'a)) (pred: 'a -> bool): option 'tag
    returns {
      | Some tag -> final_match (matched_by pred) items condition (Some tag)
      | None     -> not contains (matched_by pred) items \/ final_match (matched_by pred) items condition None
    }

= let result = ref None in

  for i = 0 to items.length - 1 do
    invariant { forall tag. !result = Some tag <->
                  exists j.  0 <= j < i /\ matched_by pred items[j] /\ Some tag = condition items[j] /\
                  forall k. j < k < i -> not matched_by pred items[k] }
    let (judgement, who) = match items[i].inner with
      | No x -> (false, x)
      | Yes x -> (true, x)
    end in
    let info = items[i].info in
    match who with
      | All -> result := judgement.bool_then(info)
      | Only id -> if pred id then result := judgement.bool_then(info);
    end;
  done;

  (* perform a "virtual loop" to strength the case !result = None;
     this could also be solved by adding a ghost variable above *)
  ghost if is_none !result && contains (matched_by pred) items then
    for i = items.length - 1 downto 0 do
      invariant { forall k. i < k < items.length -> not matched_by pred items[k] }
      invariant { exists k. 0 <= k <= i /\ matched_by pred items[k] }
      if matched_by pred items[i] then break
    done;

  !result;

end