Source file ProofEngine.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Interactive Proof Engine                                           --- *)
(* -------------------------------------------------------------------------- *)

type node = {
  tree : Wpo.t ; (* root, to check consistency *)
  goal : Wpo.t ; (* only GoalAnnot of a sequent *)
  child : string option ; (* child name from parent node *)
  parent : node option ;
  mutable script : script ;
  mutable stats : Stats.stats option ; (* memoized *)
  mutable strategy : string option ; (* hint *)
  mutable search_index : int ;
  mutable search_space : Strategy.t array ; (* sorted by priority *)
}

and script =
  | Opened
  | Script of ProofScript.jscript (* to replay *)
  | Tactic of ProofScript.jtactic * (string * node) list (* played *)

module Node =
struct
  type t = node
  let hash t = Wpo.S.hash t.goal
  let equal a b = Wpo.S.equal a.goal b.goal
  let compare a b = Wpo.S.compare a.goal b.goal
  let pretty fmt a = Wpo.S.pretty fmt a.goal
end

type tree = {
  main : Wpo.t ; (* Main goal to be proved. *)
  mutable pool : Lang.F.pool option ; (* Global pool variable *)
  mutable saved : bool ; (* Saved on Disk. *)
  mutable dirty : bool ; (* Tactical result is outdated *)
  mutable gid : int ; (* WPO goal numbering *)
  mutable head : node option ; (* the current node *)
  mutable root : node option ; (* the root node *)
}

module PROOFS = WpContext.StaticGenerator(Wpo.S)
    (struct
      type key = Wpo.S.t
      type data = tree
      let name = "Wp.ProofEngine.Proofs"
      let compile main =
        ignore (Wpo.resolve main) ;
        {
          main ; gid = 0 ;
          pool = None ;
          head = None ;
          root = None ;
          dirty = true ;
          saved = false ;
        }
    end)

module NODES = WpContext.Static
    (struct
      type key = Wpo.t
      type data = node
      let name = "Wp.ProofEngine.Nodes"
      let compare = Wpo.S.compare
      let pretty = Wpo.S.pretty
    end)

(* -------------------------------------------------------------------------- *)
(* --- Signaling                                                          --- *)
(* -------------------------------------------------------------------------- *)

let goal_hooks = ref []
let clear_hooks = ref []
let remove_hooks = ref []
let update_hooks = ref []

let add_goal_hook fn = goal_hooks := !goal_hooks @ [fn]
let add_clear_hook fn = clear_hooks := !clear_hooks @ [fn]
let add_remove_hook fn = remove_hooks := !remove_hooks @ [fn]
let add_update_hook fn = update_hooks := !update_hooks @ [fn]

let signal_goal g = List.iter (fun fn -> fn g) !goal_hooks
let signal_node n = List.iter (fun fn -> fn n) !update_hooks

let dirty_root g =
  try
    let tree = PROOFS.find g in
    if not tree.dirty then
      begin
        tree.dirty <- true ;
        signal_goal g ;
      end
  with Not_found -> ()

let rec dirty_node n =
  match n.stats with
  | None -> ()
  | Some _ ->
    n.stats <- None ;
    signal_node n ;
    match n.parent with
    | Some p -> dirty_node p
    | None -> dirty_root n.tree

let self_updating = ref false

let dirty_goal g =
  if not !self_updating then
    match NODES.get g with
    | Some n -> dirty_node n
    | None -> dirty_root g

let get wpo =
  try
    let proof = PROOFS.find wpo in
    match proof.root with
    | None | Some { script = Opened | Script _ } -> raise Not_found
    | Some { script = Tactic _ } -> if proof.saved then `Saved else `Proof
  with Not_found ->
    if ProofSession.exists wpo then `Script else `None

let iter_children f ns = List.iter (fun m -> f (snd m)) ns
let map_children f ns = List.map (fun m -> fst m,f m) ns

let pool tree =
  match tree.pool with
  | Some pool -> pool
  | None ->
    let _,sequent = Wpo.compute tree.main in
    let pool = Lang.new_pool ~vars:(Conditions.vars_seq sequent) () in
    tree.pool <- Some pool ; pool

(* -------------------------------------------------------------------------- *)
(* --- Proofs                                                             --- *)
(* -------------------------------------------------------------------------- *)

let proof ~main =
  assert (not (Wpo.is_tactic main)) ;
  PROOFS.get main

let saved t = t.saved
let set_saved t s = t.saved <- s ; signal_goal t.main

(* -------------------------------------------------------------------------- *)
(* --- Removal                                                            --- *)
(* -------------------------------------------------------------------------- *)

let rec revert_tactic t n =
  n.strategy <- None ;
  match n.script with
  | Opened | Script _ -> ()
  | Tactic(_,children) ->
    t.saved <- false ;
    n.script <- Opened ;
    iter_children (remove_node t) children

and remove_node t n =
  NODES.remove n.goal ;
  if Wpo.is_tactic n.goal then
    Wpo.remove n.goal
  else
    Wpo.clear_results n.goal ;
  List.iter (fun f -> f n) !remove_hooks ;
  Option.iter (fun n0 -> if n0 == n then t.head <- None) t.head ;
  revert_tactic t n

let clear_tree t =
  begin
    Option.iter (remove_node t) t.root ;
    t.gid <- 0 ;
    t.head <- None ;
    t.root <- None ;
    t.saved <- false ;
    List.iter (fun fn -> fn t.main) !clear_hooks ;
    signal_goal t.main ;
  end

let clear_node_tactic t n =
  revert_tactic t n ; dirty_node n ;
  if t.head = None then t.head <- Some n

let clear_parent_tactic t n =
  match n.parent with
  | None -> clear_tree t
  | Some p as h -> revert_tactic t p ; dirty_node p ; t.head <- h

let clear_node t n =
  Wpo.clear_results n.goal ;
  clear_node_tactic t n

let clear_goal w =
  try clear_tree (PROOFS.find w)
  with Not_found -> Wpo.clear_results w

(* -------------------------------------------------------------------------- *)
(* --- Removal From Wpo                                                   --- *)
(* -------------------------------------------------------------------------- *)

let removed_from_wpo g =
  if not @@ Wpo.is_tactic g then
    begin
      try
        clear_tree (PROOFS.find g) ;
        PROOFS.remove g ;
      with Not_found ->
        signal_goal g
    end

let cleared_from_wpo () =
  begin
    NODES.clear () ;
    PROOFS.clear () ;
  end

let () = Wpo.add_removed_hook removed_from_wpo
let () = Wpo.add_cleared_hook cleared_from_wpo
let () = Wpo.add_modified_hook dirty_goal

(* -------------------------------------------------------------------------- *)
(* --- Walking                                                            --- *)
(* -------------------------------------------------------------------------- *)

let rec walk f node =
  if not (Wpo.is_locally_valid node.goal) then
    match node.script with
    | Tactic (_,children) -> iter_children (walk f) children
    | Opened | Script _ -> f node

let iteri f tree =
  match tree.root with
  | None -> ()
  | Some r ->
    let k = ref 0 in
    walk (fun node -> f !k node ; incr k) r

let rec depth node =
  match node.parent with
  | None -> 1
  | Some p -> succ @@ depth p

(* -------------------------------------------------------------------------- *)
(* --- Consolidating                                                      --- *)
(* -------------------------------------------------------------------------- *)

let pending n =
  let k = ref 0 in
  walk (fun _ -> incr k) n ; !k

let locally_proved n = Wpo.is_locally_valid n.goal

let fully_proved n =
  let exception HasPending in
  try walk (fun _ -> raise HasPending) n ; true
  with HasPending -> false

let is_prover (p,_) = VCS.is_prover p

let prover_stats ~smoke goal =
  Stats.results ~smoke @@
  List.filter is_prover @@
  Wpo.get_results goal

let rec consolidate ~smoke n =
  match n.stats with
  | Some s -> s
  | None -> let s = compute ~smoke n in n.stats <- Some s ; s

and compute ~smoke n =
  if Wpo.is_locally_valid n.goal then
    prover_stats ~smoke n.goal
  else
    match n.script with
    | Opened | Script _ -> prover_stats ~smoke n.goal
    | Tactic(_,children) ->
      Stats.tactical ~qed:(Wpo.qed_time n.goal) @@
      List.map (fun (_,n) -> consolidate ~smoke n) children

let tactical tree =
  match tree.root with
  | None -> VCS.no_result
  | Some root ->
    let smoke = Wpo.is_smoke_test tree.main in
    Stats.script @@ consolidate ~smoke root

let validate tree =
  if tree.dirty then
    let result =
      if Wpo.is_locally_valid tree.main then VCS.no_result else tactical tree
    in
    try
      self_updating := true ;
      Wpo.set_result tree.main VCS.Tactical result ;
      tree.dirty <- false ;
      self_updating := false ;
    with exn ->
      self_updating := false ;
      raise exn

let consolidated wpo =
  let smoke = Wpo.is_smoke_test wpo in
  try
    match (PROOFS.find wpo).root with
    | Some node -> consolidate ~smoke node
    | _ -> raise Not_found
  with Not_found -> prover_stats ~smoke wpo

let consolidate wpo =
  try validate (PROOFS.find wpo) with Not_found -> ()

let results wpo = consolidate wpo ; Wpo.get_results wpo

let stats node =
  match node.stats with Some s -> s | None ->
    let smoke = Wpo.is_smoke_test node.tree in
    let s = compute ~smoke node in
    node.stats <- Some s ; s

(* -------------------------------------------------------------------------- *)
(* --- Accessors                                                          --- *)
(* -------------------------------------------------------------------------- *)

let main t = t.main
let head t = t.head
let head_goal t = match t.head with
  | None -> t.main
  | Some n -> n.goal
let tree n = proof ~main:n.tree
let goal n = n.goal

let tree_context t = Wpo.get_context t.main
let node_context n = Wpo.get_context n.goal
let parent n = n.parent
let title n = n.goal.Wpo.po_name

let tactical n =
  match n.script with
  | Tactic(tactic,_) -> Some tactic
  | Opened | Script _ -> None

let get_strategies n = n.search_index , n.search_space
let set_strategies n ?(index=0) hs =
  n.search_index <- index ; n.search_space <- hs ; signal_node n

let children n =
  match n.script with
  | Tactic(_,children) -> children
  | Opened | Script _ -> []

let subgoals n = List.map snd @@ children n

let rec path n = match n.parent with
  | None -> []
  | Some p -> p::path p

let child_label n = n.child

let tactic_label n =
  match n.script with Tactic({ header }, _)  -> Some header | _ -> None

let tactic n =
  match n.script with
  | Tactic({ tactic }, _)  ->
    begin try Some (Tactical.lookup ~id:tactic) with Not_found -> None end
  | _ -> None

(* -------------------------------------------------------------------------- *)
(* --- State & Status                                                     --- *)
(* -------------------------------------------------------------------------- *)

type status = [
  | `Unproved (* proof obligation not proved *)
  | `Proved   (* proof obligation is proved *)
  | `Pending of int (* proof is pending *)
  | `Passed   (* smoke test is passed (PO is not proved) *)
  | `Invalid  (* smoke test has failed (PO is proved) *)
  | `StillResist of int (* proof is pending *)
]

let status t : status =
  match t.root with
  | None ->
    if Wpo.is_locally_valid t.main
    then if Wpo.is_smoke_test t.main then `Invalid else `Proved
    else if Wpo.is_smoke_test t.main then `Passed else `Unproved
  | Some root ->
    match root.script with
    | Opened | Script _ ->
      if Wpo.is_smoke_test t.main then `Passed else `Unproved
    | Tactic _ ->
      let n = pending root in
      if n = 0 then
        if Wpo.is_smoke_test t.main then `Invalid else `Proved
      else
      if Wpo.is_smoke_test t.main then `StillResist n else `Pending n

(* -------------------------------------------------------------------------- *)
(* --- Navigation                                                         --- *)
(* -------------------------------------------------------------------------- *)

type current = [ `Main | `Internal of node | `Leaf of int * node ]

let current t : current =
  match t.head with
  | Some h ->
    let p = ref (`Internal h) in
    iteri (fun i n -> if n == h then p := `Leaf(i,n)) t ; !p
  | None -> `Main

type position = [ `Main | `Node of node | `Leaf of int ]
let goto t = function
  | `Main ->
    t.head <- t.root ; signal_goal t.main
  | `Node n ->
    if n.tree == t.main then t.head <- Some n ; signal_goal t.main
  | `Leaf k ->
    t.head <- t.root ;
    iteri (fun i n -> if i = k then t.head <- Some n) t ;
    signal_goal t.main

let fetch t node =
  try
    t.head <- t.root ;
    walk (fun n -> t.head <- Some n ; raise Exit) node ;
    false
  with Exit -> true

let rec forward t =
  match t.head with
  | None -> t.head <- t.root ; signal_goal t.main
  | Some hd ->
    if not (fetch t hd)
    then ( t.head <- hd.parent ; forward t )
    else signal_goal t.main

let cancel_parent_tactic t =
  match t.head with
  | None -> ()
  | Some n -> clear_parent_tactic t n

let cancel_current_node t =
  match t.head with
  | None -> ()
  | Some node -> clear_node t node

(* -------------------------------------------------------------------------- *)
(* --- Sub-Goal                                                           --- *)
(* -------------------------------------------------------------------------- *)

let mk_formula ~main axioms sequent =
  Wpo.VC_Annot.{ main with goal = Wpo.GOAL.make sequent ; axioms }

let mk_goal t ~title ~part ~axioms sequent =
  let id = t.gid in t.gid <- succ id ;
  let gid = Printf.sprintf "%s-%d" t.main.Wpo.po_gid id in
  let sid = Printf.sprintf "%s-%d" t.main.Wpo.po_sid id in
  Wpo.({
      po_gid = gid ;
      po_sid = sid ;
      po_name = Printf.sprintf "%s (%s)" title part ;
      po_idx = t.main.po_idx ;
      po_pid = WpPropId.tactical ~gid ;
      po_model = t.main.po_model ;
      po_formula = mk_formula ~main:t.main.po_formula axioms sequent ;
    })

let mk_node ~main ?parent ?child goal =
  let node = {
    tree=main ; parent ; child ; goal ;
    script = Opened ;
    stats = None ;
    search_index = 0 ;
    search_space = [| |] ;
    strategy = None ;
  } in NODES.define goal node ; node

let mk_root ~tree =
  let main = tree.main in
  let node = mk_node ~main main in
  let root = Some node in
  tree.root <- root ;
  tree.head <- root ;
  node

let root tree =
  match tree.root with
  | Some node -> node
  | None -> mk_root ~tree

(* -------------------------------------------------------------------------- *)
(* --- Forking                                                            --- *)
(* -------------------------------------------------------------------------- *)

module Fork =
struct
  type t = {
    tree : tree ;
    anchor : node ;
    tactic : ProofScript.jtactic ;
    goals : (string * Wpo.t) list ;
  }

  let create tree ~anchor tactic process =
    let axioms , sequent = Wpo.compute anchor.goal in
    let vars = Conditions.vars_seq sequent in
    let dseqs = Lang.local ~vars process sequent in
    let title = tactic.ProofScript.header in
    let goals = List.map
        (fun (part,s) -> part , mk_goal tree ~title ~part ~axioms s) dseqs
    in { tree ; tactic ; anchor ; goals }

  let iter f w = iter_children f w.goals

  let header frk = frk.tactic.ProofScript.header
end

let pretty fmt frk = Format.pp_print_string fmt (Fork.header frk)

type fork = Fork.t

let fork = Fork.create
let iter = Fork.iter

let anchor tree ?node () =
  match node with
  | Some n -> n
  | None ->
    match tree.head with
    | Some n -> n
    | None ->
      match tree.root with
      | Some n -> n
      | None -> mk_root ~tree

let commit fork =
  List.iter (fun (_,wp) -> ignore (Wpo.resolve wp)) fork.Fork.goals ;
  let tree = fork.Fork.tree in
  let parent = fork.Fork.anchor in
  let subnode (child,goal) = mk_node ~main:tree.main ~parent ~child goal in
  let children = map_children subnode fork.Fork.goals in
  tree.saved <- false ;
  parent.script <- Tactic( fork.Fork.tactic , children ) ;
  dirty_node parent ;
  parent , children

(* -------------------------------------------------------------------------- *)
(* --- Scripting                                                          --- *)
(* -------------------------------------------------------------------------- *)

let script_provers wpo =
  List.map (fun (p,r) -> ProofScript.a_prover p r) @@
  Wpo.get_prover_results wpo

let rec script_node (node : node) =
  script_provers node.goal @
  begin
    match node.script with
    | Script s -> List.filter ProofScript.is_tactic s
    | Tactic( tactic , children ) ->
      [ ProofScript.a_tactic tactic (List.map subscript_node children) ]
    | Opened -> []
  end

and subscript_node (key,node) = key , script_node node

let script tree =
  match tree.root with
  | None -> script_provers tree.main
  | Some node -> script_node node

let bind node script =
  match node.script with
  | Tactic _ ->
    (*TODO: saveback the thrown script *)
    ()
  | Opened | Script _ ->
    (*TODO: saveback the previous script *)
    node.script <- Script script ;
    signal_node node ;
    signal_goal node.tree

let bound node =
  match node.script with
  | Tactic _ | Opened -> []
  | Script s -> s

let is_script_result ~margin (prv,res) =
  VCS.is_extern prv && VCS.is_valid res &&
  res.prover_time > margin

let has_result tree =
  let margin = float_of_string @@ Wp_parameters.TimeMargin.get () in
  let results = Wpo.get_results tree.main in
  List.exists (is_script_result ~margin) results

let has_tactics tree =
  match tree.root with
  | None -> false
  | Some node ->
    match node.script with
    | Opened -> false
    | Tactic _ -> true
    | Script s -> List.exists ProofScript.is_tactic s

let has_script tree = has_tactics tree || has_result tree
let has_proof wpo =
  try has_script @@ PROOFS.find wpo
  with Not_found -> false

let get_hint node = node.strategy
let set_hint node strategy = node.strategy <- Some strategy ; signal_node node

(* -------------------------------------------------------------------------- *)