diff --git a/dune-project b/dune-project index 16fe1c96..468c78f8 100644 --- a/dune-project +++ b/dune-project @@ -32,4 +32,5 @@ (js_of_ocaml (>= 5.4.0)) (unionFind (>= 20220122)) (visitors (>= 20210608)) - (pprint (>= 20230830)))) + (pprint (>= 20230830)) + (cmdliner (>= 2.0.0)))) diff --git a/heifer.opam b/heifer.opam index 7b9f49dc..ca309fb0 100644 --- a/heifer.opam +++ b/heifer.opam @@ -21,6 +21,7 @@ depends: [ "unionFind" {>= "20220122"} "visitors" {>= "20210608"} "pprint" {>= "20230830"} + "cmdliner" {>= "2.0.0"} "odoc" {with-doc} ] build: [ diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml index ed12a439..80d1d854 100644 --- a/lib/hipcore_typed/subst.ml +++ b/lib/hipcore_typed/subst.ml @@ -61,6 +61,16 @@ let types_of_free_vars (type ctx_type) (ctx_type : ctx_type subst_context) (ctx method zero = SMap.empty method plus = SMap.merge_right_priority + (* ens binds 'res', remove it as a free var *) + method! visit_NormalReturn () p k = + let free_p = super#visit_pi () p in + let free_k = super#visit_kappa () k in + SMap.merge_arbitrary free_p free_k |> SMap.remove "res" + + method! visit_PointsTo () loc v = + let b = super#visit_term () v in + SMap.add loc (Some (TConstr ("ref", [v.term_type]))) b + method! visit_Exists () x f = let b = super#visit_Exists () x f in SMap.remove (ident_of_binder x) b diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml index 35694cd0..5aced0b3 100644 --- a/lib/hiplib/hiplib.ml +++ b/lib/hiplib/hiplib.ml @@ -31,6 +31,8 @@ let ocaml_prelude = " " +let entailment_succeeded = Hipprover.Entail.Entail_result.entailment_succeeded + (* let debug_tokens str = let lb = Lexing.from_string str in @@ -81,6 +83,21 @@ let check_lambda_obligation_ name params lemmas predicates obl = check_obligation_ name params lemmas preds (obl.lo_left, obl.lo_right) *) +let certificate_output : Hipprover.Certificate.certificate_file option ref = ref None + +let print_certificate program name constr proof_log = + let open Hipprover.Certificate in + ignore proof_log; + match !certificate_output with + | None -> () + | Some file -> + write_theorem ~out:file + ~program + ~name:(name ^ "_correctness") + ~statement:constr + ~string_of_step:Hipprover.Entail.string_of_coq_tactic + (Some proof_log) + let test_failed result name = if String.ends_with ~suffix:"_false" name then result @@ -170,12 +187,12 @@ let infer_spec (prog : core_program) (meth : meth_def) = let check_method prog inferred given = match given with - | None -> true + | None -> None | Some given_spec -> let open Hipprover.Entail in (* likely that we need some env or extra setup later *) let pctx = create_pctx prog in - check_staged_spec_entailment pctx inferred given_spec + Some (check_staged_spec_entailment pctx inferred given_spec) let infer_and_check_method (prog : core_program) (meth : meth_def) (given_spec : staged_spec option) = let inferred_spec = infer_spec prog meth in @@ -214,23 +231,32 @@ let analyze_method (prog : core_program) (meth : meth_def) : core_program = let updated_meth = {meth with m_spec = Some choosen_spec} in (* we always add the method into the program, regardless of whether it is verified or not? *) let prog = {prog with cp_methods = updated_meth :: prog.cp_methods} in - let prog = - (* let@ _ = Globals.Timing.(time overall) in *) - if not result then prog - else begin - let@ _ = Debug.span (fun _ -> debug - ~at:2 - ~title:(Format.asprintf "remembering predicate for %s" meth.m_name) - "") - in - let pred = Hipprover.Entail.derive_predicate meth.m_name - meth.m_params - inferred_spec in - (* let pred = todo () in *) - let cp_predicates = SMap.add meth.m_name pred prog.cp_predicates in - {prog with cp_predicates} + let is_success = match result with + | None -> true + | Some result -> entailment_succeeded result + in + let add_predicate prog name params spec = + let@ _ = Debug.span (fun _ -> debug + ~at:2 + ~title:(Format.asprintf "remembering predicate for %s" name) + "") + in + let pred = Hipprover.Entail.derive_predicate name params spec in + (* let pred = todo () in *) + let cp_predicates = SMap.add name pred prog.cp_predicates in + {prog with cp_predicates} + in (* prog *) - end + let prog = match result with + (* let@ _ = Globals.Timing.(time overall) in *) + | None -> add_predicate prog meth.m_name meth.m_params inferred_spec + | Some result -> + let open Hipprover.Entail.Entail_result in + match theorem_of_entailment result with + | Some (statement, proof) -> + print_certificate prog meth.m_name statement proof; + add_predicate prog meth.m_name meth.m_params inferred_spec + | None -> prog in (* potentially report the normalized spec as well. Refactor *) report_result @@ -238,13 +264,13 @@ let analyze_method (prog : core_program) (meth : meth_def) : core_program = ~name:meth.m_name ~inferred_spec ~given_spec - ~result; + ~result:is_success; prog let check_lemma (prog : core_program) (l : lemma) : bool = let open Hipprover.Entail in let pctx = create_pctx prog in - check_staged_spec_entailment pctx l.l_left l.l_right + entailment_succeeded (check_staged_spec_entailment pctx l.l_left l.l_right) let analyze_lemma (prog : core_program) (l : lemma) : core_program = let result = check_lemma prog l in @@ -479,8 +505,14 @@ let preprocess_spec_comments = let output = Str.global_replace lemma_attr_regex "@@@lemma" output in output -let run_file input_file = +let run_file ~certificate_file input_file = let open Utils.Io in + begin + let open Hipprover.Certificate in + match certificate_file with + | Some f -> certificate_output := Some (open_out f |> make_certificate_file) + | None -> () + end; let chan = open_in input_file in let lines = input_lines chan in let content = String.concat "\n" lines in @@ -512,7 +544,6 @@ let run_file input_file = let lexbuf = Lexing.from_string content in let staged_spec = Parser.parse_staged_spec Lexer.token lexbuf in print_endline (Pretty.string_of_staged_spec staged_spec) -*) let main () = if Array.length (Sys.argv) < 2 then begin @@ -523,3 +554,4 @@ let main () = run_file inputfile; if !test_mode && not !tests_failed then Format.printf "ALL OK!@."; exit (if !tests_failed then 1 else 0) +*) diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml new file mode 100644 index 00000000..696ab472 --- /dev/null +++ b/lib/hipprover/certificate.ml @@ -0,0 +1,278 @@ + +open Hipcore_typed.Typedhip +open Hipcore_typed.Pretty + +let config = default_config |> set_single_line + +type 'a proof_log = + | Step of 'a + | Subproof of 'a proof_log list + +(* a zipper over a proof log *) +type 'a partial_proof_log = { + current_proof : 'a proof_log list; + parent_env : 'a partial_proof_log option +} + +let empty_partial_log = {current_proof = []; parent_env = None} + +let proof_step s = Step s + +let append ppl step = + { ppl with current_proof = step :: ppl.current_proof } + +let open_subproof ppl = { + current_proof = []; + parent_env = Some ppl +} + +let close_subproof ppl = + let parent_env = Option.get ppl.parent_env in + let current_proof = Subproof (List.rev ppl.current_proof) :: parent_env.current_proof in + { parent_env with current_proof } + +let rec finalize_proof_log ppl = + match ppl.parent_env with + | None -> Subproof (List.rev ppl.current_proof) + | Some _ -> finalize_proof_log (close_subproof ppl) + +let rec string_of_proof_log ?(indent = 0) log string_of_step = + let indent_string = String.init indent (Fun.const ' ') in + match log with + | Step s -> indent_string ^ (string_of_step s) ^ "\n" + | Subproof steps -> + indent_string ^ "{\n" ^ + (steps |> List.map (fun s -> string_of_proof_log ~indent:(indent + 2) s string_of_step) |> String.concat "") ^ + indent_string ^ "}\n" + +let%expect_test "proof logging" = + let output_log log = + Printf.printf "%s\n" (string_of_proof_log log Fun.id) + in + let log = empty_partial_log in + let log = append log (proof_step "intros.") in + let log = append log (proof_step "split.") in + let log = open_subproof log in + let log = append log (proof_step "exfalso.") in + let log = append log (proof_step "assumption.") in + let log = close_subproof log in + let log = open_subproof log in + let log = append log (proof_step "auto.") in + let log = close_subproof log in + output_log (finalize_proof_log log); + [%expect {| + { + intros. + split. + { + exfalso. + assumption. + } + { + auto. + } + } + |}];; + + + +type constr = CVar of string + | CConst of const + | CApp of constr * constr list + | CFun of string * constr + (* these are only to make the output look nicer *) + | CInfix of constr * string * constr + | CSurround of string * constr * string + (* invalid node, meant to allow for better context regarding incomplete constr generation *) + | CError of string + | CQuantify of string * string list * constr + +(* Do not throw an exception when processing an invalid node. Instead, return a CError. *) + +let pi_mentions_result p = Hipcore_typed.(Syntax.conjuncts_of_pi p |> List.exists Variables.is_eq_res) + +let rec hprop_of_kappa (k : kappa) : constr = + match k with + | SepConj (k1, k2) -> CInfix (hprop_of_kappa k1, "\\*", hprop_of_kappa k2) + | EmptyHeap -> CVar "\\[]" + | PointsTo (l, v) -> CInfix (CVar l, "~~>", constr_of_term v) +and constr_of_term (t : term) : constr = + match t.term_desc with + | Const c -> CConst c + | Var v -> CVar v + | TNot t -> CApp (CVar "vnot", [constr_of_term t]) + | BinOp (op, lhs, rhs) -> + let op_fun = match op with + | Plus -> CVar "vplus" + | _ -> CError "[binary operation]" + in + CApp (op_fun, [constr_of_term lhs; constr_of_term rhs]) + | _ -> CError (string_of_term ~config t) +and constr_of_pi (p : pi) : constr = + match p with + | True -> CVar "True" + | False -> CVar "False" + | And (lhs, rhs) -> CInfix (constr_of_pi lhs, "/\\", constr_of_pi rhs) + | Or (lhs, rhs) -> CInfix (constr_of_pi lhs, "\\/", constr_of_pi rhs) + | Imply (lhs, rhs) -> CInfix (constr_of_pi lhs, "->", constr_of_pi rhs) + | Atomic (op, lhs, rhs) -> + (* if this is a result comparison, insert a cast to [val] *) + begin + match Hipcore_typed.Variables.eq_res_term p with + | Some t -> CInfix (CVar "res", "=", CApp (CVar "into", [constr_of_term t])) + | None -> + (* NOTE: these are currently implemented to only compare integers! *) + let operator = match op with + | EQ -> "=" + | GT -> ">" + | LT -> "<" + | GTEQ -> ">=" + | LTEQ -> "<=" + in + CInfix (constr_of_term lhs, operator, constr_of_term rhs) + end + | Not p -> CSurround ("~", constr_of_pi p, "") + | _ -> CError (string_of_pi ~config p) +and constr_of_state ((p, k) : state) = + CInfix (hprop_of_kappa k, "\\*", CSurround ("\\[", constr_of_pi p, "]")) +and constr_of_staged_spec (ss : staged_spec) : constr = + match ss with + | Exists (v, ss) -> CApp (CVar "fex", [CFun (ident_of_binder v, constr_of_staged_spec ss)]) + | ForAll (v, ss) -> CApp (CVar "fall", [CFun (ident_of_binder v, constr_of_staged_spec ss)]) + | Require (p, k) -> CApp (CVar "req_", [constr_of_state (p, k)]) + (* support only one argument for now, pack multiple arguments via vtup...? *) + | HigherOrder (f, [arg]) -> CApp (CVar "unk", [CConst (TStr f); constr_of_term arg]) + (* need to convert anything that says nothing about the result to an [ens_] ... *) + | NormalReturn (p, k) -> + if pi_mentions_result p + then CApp (CVar "ens", [CFun ("res", constr_of_state (p, k))]) + else CApp (CVar "ens_", [constr_of_state (p, k)]) + | Sequence (Require (p, k), f) -> CApp (CVar "req", [constr_of_state (p, k); constr_of_staged_spec f]) + | Sequence (f1, f2) -> CInfix (constr_of_staged_spec f1, ";;", constr_of_staged_spec f2) + | Disjunction (f1, f2) -> CApp (CVar "disj", [constr_of_staged_spec f1; constr_of_staged_spec f2]) + | Bind (v, f1, f2) -> + let bind f fk = match type_of_binder v with + | Int -> CApp (CVar "@bind_t", [CVar "int"; CVar "_"; f; fk]) + | TConstr ("ref", _) -> CApp (CVar "@bind_t", [CVar "loc"; CVar "_"; f; fk]) + (* let Coq infer the underlying type *) + (* if the bound variable is unused, it infers Int, which breaks some of the rewriting rules *) + (* there might need to be a better special case for that scenario... *) + | _ -> CApp (CVar "bind_t", [f; fk]) + in + bind (constr_of_staged_spec f1) (CFun (ident_of_binder v, constr_of_staged_spec f2)) + | _ -> CError (string_of_staged_spec ~config ss) + +let rec string_of_constr c = + match c with + | CConst c -> begin match c with + | ValUnit -> "vunit" + | TStr s -> "\"" ^ s ^ "\"" + | Num n -> string_of_int n + | Nil -> "[]" + | TTrue -> "true" + | TFalse -> "false" + end + | CVar v -> v + | CFun (x, body) -> Printf.sprintf "(fun %s => %s)" x (string_of_constr body) + | CApp (f, args) -> Printf.sprintf "(%s %s)" (string_of_constr f) (List.map string_of_constr args |> String.concat " ") + | CInfix (lhs, op, rhs) -> Printf.sprintf "(%s %s %s)" (string_of_constr lhs) op (string_of_constr rhs) + | CSurround (lp, sub, rp) -> Printf.sprintf "%s %s %s" lp (string_of_constr sub) rp + | CError s -> Printf.sprintf "(* unsupported node: %s *) _" s + | CQuantify (q, vars, body) -> Printf.sprintf "%s %s, %s" q (String.concat " " vars) (string_of_constr body) + +let quantify vars constr = + match vars with + | [] -> constr + | free_vars -> CQuantify ("forall", free_vars, constr) + +let remove_nonterm_variables free_var_mapping = + free_var_mapping + |> Utils.Hstdlib.SMap.to_list + |> List.filter_map (fun (fv, ty) -> + match ty with + | None -> None + | Some _ -> Some fv) + +let statement_of_entailment f1 f2 = + let free_vars = + let open Utils.Hstdlib in + let open Hipcore_typed.Subst in + SMap.merge_arbitrary (types_of_free_vars Sctx_staged f1) (types_of_free_vars Sctx_staged f2) + |> SMap.remove "res" + |> remove_nonterm_variables + in + let entailment = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2]) in + quantify free_vars entailment + +let statement_of_method name params spec = + match params with + | [p] -> + let free_vars = + let open Hipcore_typed.Subst in + let open Utils.Hstdlib in + types_of_free_vars Sctx_staged spec + |> SMap.add (ident_of_binder p) (Some (type_of_binder p)) + |> remove_nonterm_variables + in + CQuantify ("forall", free_vars, + CApp (CVar "entails", [CApp (CVar "unk", [CConst (TStr name); CVar (ident_of_binder p)]); constr_of_staged_spec spec])) + | _ -> CError ("unsupported method " ^ name) + +type certificate_file = out_channel + +let make_certificate_file out = + let prelude = {| +From ShiftReset Require Import Logic Entl Automation Norm Propriety. +From ShiftReset.Mechanized Require Import State Normalization Entail_tactics. + +Local Open Scope string_scope. + +(* Due to deficiencies in the underlying model, this is necessary to get some of the + needed rewrite operations (in particular, those manipulating the body of a [bind]) + to succeed. If this admit is undesired, it may be possible to prove the needed instances + of RewritableBinder individually. *) + +#[global] +Instance RewritableBinder_anything : forall f, RewritableBinder f. +Proof. +Admitted. + +(* primitive function declarations *) + +Definition vplus (a b:val) : val := + match a, b with + | vint a, vint b => vint (a + b) + | _, _ => vunit + end. + +(* end prelude *) + +|} + in + Printf.fprintf out "%s" prelude; + out + +let write_theorem ~out ~program ~name ~statement ~string_of_step log = + (* Printf.printf "writing theorem for %s\n" name; *) + (* Printf.printf "statement: %s\n" (string_of_constr statement); *) + let theorem_params = + program.cp_predicates + |> Utils.Hstdlib.SMap.to_list + |> List.map (fun (_, pred_def) -> + let statement = statement_of_method pred_def.p_name pred_def.p_params pred_def.p_body in + Printf.sprintf "(%s_rewrite_rule : %s)" pred_def.p_name (string_of_constr statement)) + in + Printf.fprintf out "(* begin proof item %s *)\n" name; + Printf.fprintf out "Theorem %s %s\n : %s.\n" name (String.concat "\n " theorem_params) (string_of_constr statement); + Printf.fprintf out "Proof. intros. rew_hprop_to_state.\n"; + begin match log with + | None -> Printf.fprintf out "Admitted.\n" + | Some log -> Printf.fprintf out "%s" (string_of_proof_log log string_of_step); + Printf.fprintf out "Qed.\n" + end; + Printf.fprintf out "(* end proof item %s *)\n\n" name; + Out_channel.flush out + +let write_assumption ~out ~name ~statement = + Printf.fprintf out "Parameter %s: %s.\n\n" name (string_of_constr statement); + Out_channel.flush out; diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli new file mode 100644 index 00000000..81cfac99 --- /dev/null +++ b/lib/hipprover/certificate.mli @@ -0,0 +1,50 @@ + + +(* Complications: + + - In the formalization, all closures must be placed in a separate store, unlike here, + where we can directly embed it into the specification as a TLambda. + + - All primitive functions cannot directly be lifted to coq-level functions. to "assert" + a value is of a given type, we need to either add a (fex (fun typed_val : T => ens_ \[untyped_val = vconstructor typed_val] ;; ...)) + -like condition to the spec, or admit lemmas that state exactly this. and this isn't taking into account + the fact that we won't always have types before smt!!! + + - i feel like it is safe to couple this to work specifically with coq since YAGNI + support for anything else? + + *) + +open Hipcore_typed.Typedhip + +type 'a proof_log + +type 'a partial_proof_log + +val empty_partial_log : 'a partial_proof_log + +val proof_step : 'a -> 'a proof_log + +val append : 'a partial_proof_log -> 'a proof_log -> 'a partial_proof_log + +val open_subproof : 'a partial_proof_log -> 'a partial_proof_log + +val close_subproof : 'a partial_proof_log -> 'a partial_proof_log + +val finalize_proof_log : 'a partial_proof_log -> 'a proof_log + +type constr + +val string_of_constr : constr -> string + +val constr_of_term : term -> constr + +val statement_of_entailment : staged_spec -> staged_spec -> constr + +type certificate_file + +val make_certificate_file : out_channel -> certificate_file + +val write_theorem : out:certificate_file -> program:core_program -> name:string -> statement:constr -> string_of_step:('a -> string) -> 'a proof_log option -> unit + +val write_assumption : out:certificate_file -> name:string -> statement:constr -> unit diff --git a/lib/hipprover/dune b/lib/hipprover/dune index df0de526..23d7b55e 100644 --- a/lib/hipprover/dune +++ b/lib/hipprover/dune @@ -1,6 +1,6 @@ (library (name hipprover) - (modules ProversEx entail forward_rules infer_types normalize rewriting rewriting2 heap biab simpl reduce_shift_reset) + (modules ProversEx entail forward_rules infer_types normalize rewriting rewriting2 heap biab simpl reduce_shift_reset certificate) (libraries debug search hipcore provers utils iter provers_common z3 hipcore_typed) (inline_tests) (preprocess (pps ppx_expect))) diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml index b55c459c..d0a09dc3 100644 --- a/lib/hipprover/entail.ml +++ b/lib/hipprover/entail.ml @@ -14,6 +14,36 @@ open Utils.Hstdlib | `Left -> Format.asprintf "%s, L" f | `Right -> Format.asprintf "%s, R" f *) +type coq_tactic = + | Simplify + | Unfold_nonrec + | Intro_pure_assumption + | Split_disjunction + | Choose_disj_branch of [`Left | `Right] + | Biab + | Match_ens + | Solve_single + | Solve_empty + | Intro_exists of binder + | Inst_exists of term + | Inst_forall of term + +let string_of_coq_tactic tac = + match tac with + | Simplify -> "fsimpl." + | Unfold_nonrec -> "funfold_from_ctx." + | Intro_pure_assumption -> "fpure_assumption." + | Split_disjunction -> "fsplit_disj." + | Choose_disj_branch `Left -> "fdisj_left_state." + | Choose_disj_branch `Right -> "fdisj_right_state." + | Biab -> "fbiab_state." + | Match_ens -> "fmatch_ens." + | Solve_single -> "fsingle_ens." + | Solve_empty -> "fempty." + | Intro_exists t -> "fdestruct " ^ (ident_of_binder t) ^ "." + | Inst_exists t -> "fexists " ^ (Certificate.(string_of_constr (constr_of_term t))) ^ "." + | Inst_forall t -> "finst_lhs_all " ^ Certificate.(string_of_constr (constr_of_term t)) ^ "." + type use = Use of string [@@unboxed] let string_of_use (Use f) = f @@ -27,6 +57,7 @@ type pctx = { lemmas : (string * Rewriting.rule) list; unfolded : use list; assumptions : pi list; + proof_log : coq_tactic Certificate.partial_proof_log } let string_of_pctx ctx = @@ -38,6 +69,7 @@ let string_of_pctx ctx = unfolded; induction_hypotheses; lemmas; + _ } = ctx in @@ -80,8 +112,18 @@ let new_pctx () = unfolded = []; induction_hypotheses = []; lemmas = []; + proof_log = Certificate.empty_partial_log } +let log_proof_step pctx tactic = + { pctx with proof_log = Certificate.(append pctx.proof_log (proof_step tactic)) } + +let open_subproof_log pctx = + { pctx with proof_log = Certificate.open_subproof pctx.proof_log } + +let close_subproof_log pctx = + { pctx with proof_log = Certificate.close_subproof pctx.proof_log } + let has_been_unfolded pctx name _lr = pctx.unfolded |> List.find_opt @@ -392,65 +434,6 @@ end = struct fmt end -type coq_tactic = - | Rewrite of string - | SRReduction - | Simplify - | Biab - | EntDisjL - | EntDisjR - | Focus of coq_tactic list - -type coq_tactics = coq_tactic list - -let rec string_of_coq_tactic t = - match t with - | EntDisjL -> "apply ent_disj_l." - | EntDisjR -> "apply ent_disj_l." - | Focus [] -> "" - | Focus [a] -> Format.asprintf "{ %s }" (string_of_coq_tactic a) - | Focus (a :: rest) -> - Format.asprintf "{ %s\n%s }" (string_of_coq_tactic a) - (string_of_list_ind_lines string_of_coq_tactic rest) - | Simplify -> "fsimpl." - | Biab -> "fbiabduction." - | SRReduction -> "freduction." - | Rewrite r -> Format.asprintf "rewrite %s." r - -and string_of_coq_tactics ts = - ts |> List.map string_of_coq_tactic |> String.concat "\n" - -let%expect_test _ = - Format.printf "%s@." - (string_of_coq_tactics - [ - EntDisjL; - Focus - [ - EntDisjR; - EntDisjL; - EntDisjR; - EntDisjL; - EntDisjR; - EntDisjL; - EntDisjR; - EntDisjL; - ]; - Focus [EntDisjR]; - ]); - [%expect - {| - apply ent_disj_l. - { apply ent_disj_l. - apply ent_disj_l. - apply ent_disj_l. - apply ent_disj_l. - apply ent_disj_l. - apply ent_disj_l. - apply ent_disj_l. - apply ent_disj_l. } - { apply ent_disj_l. } - |}] let rec disj_left () : unit Tactic.t = let open Tactic in @@ -590,6 +573,23 @@ let%expect_test _ = unfolded: |}] +module Entail_result : sig + type entailment_result + val entail_failure : entailment_result + val result_of_pctx : pctx -> staged_spec -> staged_spec -> entailment_result + val entailment_succeeded : entailment_result -> bool + val theorem_of_entailment : entailment_result -> (Certificate.constr * coq_tactic Certificate.proof_log) option +end = struct + type entailment_result = pstate option + let entail_failure = None + let result_of_pctx pctx f1 f2 = Some (pctx, f1, f2) + let entailment_succeeded = Option.is_some + let theorem_of_entailment r = + match r with + | Some (pctx, f1, f2) -> Some (Certificate.(statement_of_entailment f1 f2, finalize_proof_log pctx.proof_log)) + | None -> None +end + type tactic = pstate -> pstate Iter.t let fail = () @@ -679,7 +679,9 @@ let simplify : total = let@ _ = span (fun r -> log_proof_state_total ~title:"simplify" (pctx, f1, f2) r) in + let pctx = log_proof_step pctx Unfold_nonrec in let pctx, f1, f2 = unfold_nonrecursive_definitions (pctx, f1, f2) in + let pctx = log_proof_step pctx Simplify in let f1 = repeat_simplify_lhs f1 in let f2 = Normalize.normalize_spec_rhs f2 in (pctx, f1, f2) @@ -794,6 +796,7 @@ let prove_pure_fact (pctx : pctx) (p : pi) = let rec handle_pure_ens_lhs (pctx : pctx) f = debug ~at:5 ~title:"handle_pure_ens_lhs" "%s " (string_of_staged_spec f); + let pctx = log_proof_step pctx Intro_pure_assumption in match f with | NormalReturn (p, EmptyHeap) when not (Variables.is_eq_res p) -> add_assumption pctx p, NormalReturn (True, EmptyHeap) @@ -849,6 +852,7 @@ let rec apply_ent_rule ?name : tactic = | NormalReturn (True, EmptyHeap), NormalReturn (True, EmptyHeap) | Require (True, EmptyHeap), Require (True, EmptyHeap) -> (* | Require (True, EmptyHeap), Require (True, EmptyHeap) -> *) + let pctx = log_proof_step pctx Solve_empty in k (pctx, ens (), ens ()) (* | ( Sequence (NormalReturn (True, EmptyHeap), f1), Sequence (NormalReturn (True, EmptyHeap), f2) ) @@ -922,6 +926,7 @@ let rec apply_ent_rule ?name : tactic = span (fun _r -> log_proof_state ~title:"ent: pure assumption" (pctx, f1, f2)) in + let pctx = log_proof_step pctx Intro_pure_assumption in { pctx with assumptions = p1 :: pctx.assumptions } in entailment_search ?name (pctx, f3, f2) k @@ -931,6 +936,7 @@ let rec apply_ent_rule ?name : tactic = span (fun _r -> log_proof_state ~title:"ent: pure assumption" (pctx, f1, f2)) in + let pctx = log_proof_step pctx Intro_pure_assumption in { pctx with assumptions = p2 :: pctx.assumptions } in entailment_search ?name (pctx, f1, f4) k @@ -979,7 +985,7 @@ let rec apply_ent_rule ?name : tactic = | Atomic (EQ, t1, t2) when t2.term_desc = Var (ident_of_binder y) -> Some t1 | _ -> None in - let f1 = + let f1, pctx = match Lists.find_delete_map find_equality eqs with | None -> seq @@ -987,7 +993,7 @@ let rec apply_ent_rule ?name : tactic = Require (conj (p2 :: eqs), sep_conj a); NormalReturn (p1, sep_conj f); f3; - ] + ], pctx | Some (t, eqs) -> debug ~at:5 ~title:"ent: biab f inst with" "[%s/%s]" (string_of_term t) (string_of_binder y); seq @@ -995,8 +1001,9 @@ let rec apply_ent_rule ?name : tactic = Require (conj (p2 :: eqs), sep_conj a); NormalReturn (p1, sep_conj f); Subst.subst_free_vars [(ident_of_binder y, t)] f3; - ] + ], log_proof_step pctx (Inst_forall t) in + let pctx = log_proof_step pctx Biab in entailment_search ?name (pctx, f1, f2) k (* | ( Sequence @@ -1023,6 +1030,7 @@ let rec apply_ent_rule ?name : tactic = let@ _ = span (fun _r -> log_proof_state ~title:"ent: ens ens" (pctx, f1, f2)) in + let pctx = log_proof_step pctx Solve_single in let@ (ap, ah), (fp, fh) = biab h1 h2 in let valid = check_pure_obligation @@ -1038,6 +1046,7 @@ let rec apply_ent_rule ?name : tactic = let@ _ = span (fun _r -> log_proof_state ~title:"ent: req req" (pctx, f1, f2)) in + let pctx = log_proof_step pctx Solve_single in apply_ent_rule ?name (pctx, NormalReturn (p2, h2), NormalReturn (p1, h1)) k | Sequence (NormalReturn (p1, h1), f3), Sequence (NormalReturn (p2, h2), f4) -> @@ -1050,6 +1059,7 @@ let rec apply_ent_rule ?name : tactic = (conj (pctx.assumptions @ [p1; Heap.xpure h1])) (conj [p2; ap; Heap.xpure h2]) in + let pctx = log_proof_step pctx Match_ens in if valid then entailment_search ?name (pctx, seq [req ~h:ah (); f3], seq [req ~h:fh (); f4]) @@ -1063,24 +1073,27 @@ let rec apply_ent_rule ?name : tactic = k | Disjunction (f3, f4), f2 -> let tag = Variables.fresh_variable () in + let pctx = log_proof_step pctx Split_disjunction in let@ _ = span (fun _r -> debug ~at:4 ~title:(Format.asprintf "disj on the left [[%s]]" tag) "") in - let@ _ = entailment_search ?name (pctx, f3, f2) in + let@ (pctx, _, _) = entail_subgoal ?name (pctx, f3, f2) in let@ _ = span (fun _r -> debug ~at:4 ~title:(Format.asprintf "right disjunct <<%s>>" tag) "") in - entailment_search ?name (pctx, f4, f2) k + entail_subgoal ?name (pctx, f4, f2) k | f1, Disjunction (f3, f4) -> debug ~at:4 ~title:"disj on the right" ""; or_ (fun k1 -> let@ _ = span (fun _r -> debug ~at:4 ~title:"left disjunct" "") in + let pctx = log_proof_step pctx (Choose_disj_branch `Left) in entailment_search ?name (pctx, f1, f3) k1) (fun k1 -> let@ _ = span (fun _r -> debug ~at:4 ~title:"right disjunct" "") in + let pctx = log_proof_step pctx (Choose_disj_branch `Right) in entailment_search ?name (pctx, f1, f4) k1) k (* two functions with equal terms *) @@ -1114,6 +1127,7 @@ let rec apply_ent_rule ?name : tactic = in { pctx with constants = var_of_binder x :: pctx.constants } in + let pctx = log_proof_step pctx (Intro_exists x) in entailment_search ?name (pctx, f3, f2) k | f1, ForAll (x, f4) -> let pctx = @@ -1145,6 +1159,7 @@ let rec apply_ent_rule ?name : tactic = ~title:(Format.asprintf "ent: exists on the right; [%s/%s]" (string_of_term c) (string_of_binder x)) (pctx, f1, f2)) in + let pctx = log_proof_step pctx (Inst_exists c) in entailment_search ?name (pctx, f1, f4) k1 else (fun _ -> fail)) in @@ -1228,6 +1243,19 @@ let rec apply_ent_rule ?name : tactic = then k (pctx, ens (), ens ()) else (log_proof_state ~title:"STUCK" ps; fail) +(** A wrapper for [entailment_search] that delineates this entailment as a focused subgoal + in the proof log. Note that unlike [entailment_search], the context this tactic outputs + must not be ignored. since the proof log of the subgoal is stored there. *) +and entail_subgoal : ?name:string -> tactic = + fun ?name ps k -> + let (pctx, lhs, rhs) = ps in + let pctx_original = pctx in + let pctx = open_subproof_log pctx in + let@ (pctx, _, _) = entailment_search ?name (pctx, lhs, rhs) in + let pctx = close_subproof_log pctx in + (* preserve the original context, but copy over the proof log *) + k ({pctx_original with proof_log = pctx.proof_log}, lhs, rhs) + and entailment_search : ?name:string -> tactic = let prev_state = ref None in fun ?name ps k -> @@ -1245,10 +1273,12 @@ let check_staged_spec_entailment ?name pctx inferred given = debug ~at:2 ~title:"entailment" "%s\n⊑\n%s\n%s" (string_of_staged_spec inferred) (string_of_staged_spec given) - (string_of_result string_of_bool r)) + (string_of_result (fun x -> string_of_bool (Entail_result.entailment_succeeded x)) r)) in match Iter.head (entailment_search ?name (pctx, inferred, given)) with - | None -> false + | None -> Entail_result.entail_failure | Some ps -> debug ~at:2 ~title:"proof found" "%s" (string_of_pstate ps); - true + let pctx_outcome, _, _ = ps in + let proof_log = pctx_outcome.proof_log in + Entail_result.result_of_pctx { pctx with proof_log } inferred given diff --git a/main/dune b/main/dune index f2f31a4e..33a15539 100644 --- a/main/dune +++ b/main/dune @@ -1,7 +1,7 @@ (executable (name hip) (modules hip) - (libraries unix hiplib provers_native)) + (libraries unix hiplib provers_native cmdliner)) (executable (name hipjs) @@ -11,4 +11,4 @@ (install (section bin) - (files (hip.exe as hip))) \ No newline at end of file + (files (hip.exe as hip))) diff --git a/main/hip.ml b/main/hip.ml index f66fe27e..ee0cfb9f 100644 --- a/main/hip.ml +++ b/main/hip.ml @@ -1,4 +1,7 @@ +open Cmdliner +open Cmdliner.Term.Syntax + let redirect_stdout f = let name = "out.org" in Format.printf "%s@." name; @@ -11,30 +14,67 @@ let redirect_stdout f = Unix.close oldstdout; close_out newstdout -let () = - Hiplib.(test_mode := - (Option.bind (Sys.getenv_opt "TEST") int_of_string_opt - |> Option.value ~default:0) > 0); - Hiplib.(file_mode := - (Option.bind (Sys.getenv_opt "FILE") int_of_string_opt - |> Option.value ~default:0) > 0); - begin - if Option.bind (Sys.getenv_opt "NOTYPES") int_of_string_opt |> Option.value ~default:0 > 0 - then Hipcore_typed.Dynamic_typing.set_dynamic_typing () - end; - let ctf = - Option.bind (Sys.getenv_opt "CTF") int_of_string_opt - |> Option.value ~default:0 > 0 - in +let in_test_mode = + let env = Cmd.Env.info "TEST" in + let doc = "Run in test mode." in + Arg.(value & flag & info ["test"] ~env ~doc ~docv:"TEST") + +let output_to_file = + let env = Cmd.Env.info "FILE" in + let doc = "Redirect all output to a file." in + Arg.(value & flag & info ["debug-file"] ~env ~doc ~docv:"DEBUG_FILE") + +let file_to_prove = + let doc = "The file with code to verify." in + Arg.(required & pos 0 (some string) None & info [] ~doc ~docv:"FILE") + +let show_types = + let env = Cmd.Env.info "SHOW_TYPES" in + let doc = "Insert type annotations in output." in + Arg.(value & flag & info ["show-types"] ~env ~doc ~docv:"SHOW_TYPES") + +let perfetto_trace = + let env = Cmd.Env.info "CTF" in + let doc = "Output a trace file viewable by Perfetto." in + Arg.(value & flag & info ["perfetto-trace"] ~env ~doc ~docv:"TRACE") + +let debug_query = + let env = Cmd.Env.info "DEBUG" in + let doc = "Enable and specify parameters to filter debug output." in + Arg.(value & opt (some string) None & info ["debug"] ~env ~doc ~docv:"DEBUG") + +let run_as_untyped = + let env = Cmd.Env.info "NOTYPES" in + let doc = "Ignore types when proving" in + Arg.(value & flag & info ["notypes"] ~env ~doc ~docv:"DEBUG") + +let certificate_file = + let doc = "Output a Rocq certificate of any proved entailment. (Experimental)" in + Arg.(value & opt (some string) None & info ["certificate"] ~doc ~docv:"CERT_FILE") + +let cmd = + Cmd.make (Cmd.info "heifer" ~version:"0.1") @@ + let+ file_to_prove and+ in_test_mode and+ output_to_file + and+ show_types and+ perfetto_trace and+ debug_query + and+ run_as_untyped and+ certificate_file in + Hiplib.test_mode := in_test_mode; + Hiplib.file_mode := output_to_file; + if show_types then + Hipcore_typed.Pretty.(set_current_config set_types_display); + if run_as_untyped then + Hipcore_typed.Dynamic_typing.set_dynamic_typing (); + Hiplib.Debug.init ~ctf:perfetto_trace ~org:!Hiplib.file_mode debug_query; + let file_to_prove = Sys.getcwd () ^ "/" ^ file_to_prove in begin - if Option.bind (Sys.getenv_opt "SHOW_TYPES") int_of_string_opt - |> Option.value ~default:0 > 0 - then Hipcore_typed.Pretty.(set_current_config set_types_display) - end; - if Unix.isatty Unix.stdout && not !Hiplib.file_mode && not ctf then - Hipcore.Pretty.colours := `Ansi; - Hiplib.Debug.init ~ctf ~org:!Hiplib.file_mode (Sys.getenv_opt "DEBUG"); if !Hiplib.file_mode then - redirect_stdout Hiplib.main - else - Hiplib.main () + redirect_stdout (fun () -> Hiplib.run_file ~certificate_file file_to_prove) + else + Hiplib.run_file ~certificate_file file_to_prove + end; + if !Hiplib.test_mode && not !Hiplib.tests_failed then Format.printf "ALL OK!@."; + let return_code = if !Hiplib.tests_failed then 1 else 0 in + return_code + +let main () = Cmd.eval' cmd + +let () = if !Sys.interactive then () else exit (main ())