From 62db1269bb388d87d02de185d243d9d54f2426b0 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 9 Oct 2026 12:40:06 +0200 Subject: [PATCH] refactor(pl): circuit as recheckable per-logic rules PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `circuit` tactic class (`circuit`, `circuit simplify`, `extens`), which closed or rewrote goals with the opaque `VBdep` validation: - `circuit`: trusted rules without premise `EcHoareCircuit`, `EcEquivCircuit` and, on a goal that is not a statement judgement, `EcFolCircuit` (new `rules/fol/`, for the rules whose conclusion is a plain formula). Parameterless nodes; the checkers ("hoare-circuit", "equiv-circuit", "fol-circuit") re-run the circuit decision, a deterministic function of the goal and its hypotheses (expensive: only under EC_RECHECK). - `circuit simplify`: trusted rule `EcHoareCircuitSimplify`, whose premise has the postcondition simplified by circuits; the checker ("hoare-circuit-simplify") re-runs the simplification. - `extens`: trusted rules `EcHoareExtens` (one premise per value of a program variable of a type bound to a bitstring; node: the resolved variable) and `EcFolExtens` (`all p (iota_ s n)` from its `n` instances); checkers "hoare-extens" and "fol-extens". The tactic is derived: the rule, then the given tactic on each premise, which must close it. The proofs of the instances are now kept in the proof tree (and rechecked), instead of being discarded. - The translation of the precondition and the decision of the postcondition, shared by the hoare and equiv rules, move to `rules/EcPlCircuit`. - `EcPhlBDep` is reduced to the dispatchers and the derived `extens`; its interface is unchanged. Behaviour is preserved, error messages included. Validation: new test tests/circuits/circuit_rules.ec (every rule, every error path), passing with and without the change, the error messages compared; stdlib + unit under EC_RECHECK=1. Each checker, when broken, is caught only under EC_RECHECK; the rules are not used by the stdlib, only by tests/circuits. --- src/phl/README.md | 8 +- src/phl/REFACTORING.md | 17 +- src/phl/ecPhlBDep.ml | 408 ++---------------- src/phl/rules/ecPlCircuit.ml | 108 +++++ src/phl/rules/ecPlCircuit.mli | 36 ++ src/phl/rules/equiv/ecEquivCircuit.ml | 67 +++ src/phl/rules/equiv/ecEquivCircuit.mli | 27 ++ src/phl/rules/fol/ecFolCircuit.ml | 47 ++ src/phl/rules/fol/ecFolCircuit.mli | 24 ++ src/phl/rules/fol/ecFolExtens.ml | 67 +++ src/phl/rules/fol/ecFolExtens.mli | 31 ++ src/phl/rules/hoare/ecHoareCircuit.ml | 65 +++ src/phl/rules/hoare/ecHoareCircuit.mli | 27 ++ src/phl/rules/hoare/ecHoareCircuitSimplify.ml | 68 +++ .../rules/hoare/ecHoareCircuitSimplify.mli | 30 ++ src/phl/rules/hoare/ecHoareExtens.ml | 148 +++++++ src/phl/rules/hoare/ecHoareExtens.mli | 51 +++ tests/circuits/circuit_rules.ec | 158 +++++++ 18 files changed, 1010 insertions(+), 377 deletions(-) create mode 100644 src/phl/rules/ecPlCircuit.ml create mode 100644 src/phl/rules/ecPlCircuit.mli create mode 100644 src/phl/rules/equiv/ecEquivCircuit.ml create mode 100644 src/phl/rules/equiv/ecEquivCircuit.mli create mode 100644 src/phl/rules/fol/ecFolCircuit.ml create mode 100644 src/phl/rules/fol/ecFolCircuit.mli create mode 100644 src/phl/rules/fol/ecFolExtens.ml create mode 100644 src/phl/rules/fol/ecFolExtens.mli create mode 100644 src/phl/rules/hoare/ecHoareCircuit.ml create mode 100644 src/phl/rules/hoare/ecHoareCircuit.mli create mode 100644 src/phl/rules/hoare/ecHoareCircuitSimplify.ml create mode 100644 src/phl/rules/hoare/ecHoareCircuitSimplify.mli create mode 100644 src/phl/rules/hoare/ecHoareExtens.ml create mode 100644 src/phl/rules/hoare/ecHoareExtens.mli create mode 100644 tests/circuits/circuit_rules.ec diff --git a/src/phl/README.md b/src/phl/README.md index d87abc58b..faeac15df 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -141,10 +141,11 @@ src/phl/ hoare/ ehoare/ bdhoare/ equiv/ eager/ Ec: one module per (logic, rule) transforms/ EcTr: catalogue entries of the program transformations + fol/ EcFol: rules whose conclusion is a plain formula ecPl*.ml computations shared by the rules of every logic: EcPlFrame, EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform, EcPlMatch, EcPlFun, EcPlCall, EcPlWeakMem, EcPlExists, - EcPlECall + EcPlECall, EcPlCircuit ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -167,6 +168,11 @@ src/phl/ a precondition (`elim*`); `exists*` / `exlim` (consequence + rule) and `ecall` (`EcECall`: existential rules, `seq` and the `call` rule of the logic) are derived. +- The `circuit` rules (`EcHoareCircuit`, `EcEquivCircuit`, + `EcHoareCircuitSimplify`, `EcHoareExtens`; on formulas `EcFolCircuit`, + `EcFolExtens` in `rules/fol/`) close or rewrite a goal by the circuit + backend; their checkers re-run the decision (only under `EC_RECHECK`). + `extens` is derived (the rule, then the given tactic on each premise). - A rule relating two logics (e.g. the `pr` bridges) lives with the logic of its conclusion. - A rule concluding a probability statement from a judgement (`byphoare`, diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index e45b5ff33..31a788ab0 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -148,6 +148,8 @@ src/phl/ node, pure builder, checker, derived forms, elaboration transforms/ EcTr: the catalogue entries of the program transformations (§7f) + fol/ EcFol: rules of program-logic tactics whose + conclusion is a plain formula (EcFolCircuit, EcFolExtens) ecPl*.ml logic-agnostic computations shared by the rules of every logic: EcPlFrame (framing conditions), EcPlSp (strongest postcondition), EcPlWp (weakest precondition), EcPlRndSem @@ -162,7 +164,9 @@ src/phl/ variables), EcPlExists (pulling the existentials of a precondition to the front, quantifying a precondition over values), EcPlECall (the elaboration of `ecall`: - typing the contract, abstracting its program variables) + typing the contract, abstracting its program variables), + EcPlCircuit (translation of a precondition to circuits + and decision of a postcondition) ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -203,6 +207,17 @@ uniform across logics or relate several judgements: the contract abstracted by the existential rules, `seq`, then the `call` rule of the logic; the forward hoare form frames the precondition with the split and frame rules); +- the `circuit` rules — `EcHoareCircuit`, `EcEquivCircuit` (the judgement + decided by the circuit backend, no premise), `EcHoareCircuitSimplify` + (`circuit simplify`: the postcondition simplified by circuits) and + `EcHoareExtens` (`extens [x]`: one premise per value of a program + variable of a type bound to a bitstring) — live in `rules//`; + their forms on plain formulas (`EcFolCircuit`; `EcFolExtens`: + `all p (iota_ s n)` from its `n` instances) live in `rules/fol/`. The + nodes record nothing but the resolved variable of `extens`; the + checkers re-run the circuit decision on the goal (deterministic, but + expensive: it only runs under `EC_RECHECK`). `extens` is derived: the + rule, then the given tactic on each premise, which must close it; - a rule relating judgements of two logics (the `pr` bridges, `hoare` from `phoare`, …) lives with the logic of its conclusion; - a rule concluding a statement on probabilities from a judgement diff --git a/src/phl/ecPhlBDep.ml b/src/phl/ecPhlBDep.ml index dad290982..98924cd41 100644 --- a/src/phl/ecPhlBDep.ml +++ b/src/phl/ecPhlBDep.ml @@ -1,392 +1,50 @@ (* -------------------------------------------------------------------- *) -open EcUtils open EcAst -open EcEnv -open EcTypes open EcCoreGoal -open EcFol -open EcLowCircuits -open EcCircuits -open LDecl -open FApi (* -------------------------------------------------------------------- *) -module Map = Batteries.Map -module Hashtbl = Batteries.Hashtbl -module Set = Batteries.Set -module Option = Batteries.Option - -(* -------------------------------------------------------------------- *) -let form_list_from_iota (hyps : hyps) (f : form) : form list = - match sform_of_form f with - | SFop ((p, _), [n; m]) when EcPath.p_equal p EcCoreLib.CI_List.p_iota -> - let n = int_of_form hyps n in - let m = int_of_form hyps m in - List.init (BI.to_int m) (fun i -> f_int BI.(add n (of_int i))) - | _ -> raise (DestrError "iota") - -let rec form_list_of_form (f : form) : form list = - match sform_of_form f with - | SFop ((p, _), []) when EcPath.p_equal p EcCoreLib.CI_List.p_empty -> [] - | SFop ((p, _), [h; t]) when EcPath.p_equal p EcCoreLib.CI_List.p_cons -> - h :: form_list_of_form t - | _ -> raise (DestrError "list") - -(* -------------------------------------------------------------------- *) -let rec destr_conjunction (hyps : hyps) (f : form) : form list = - let redmode = { (circ_red hyps) with zeta = false } in - - match sform_of_form (EcCallbyValue.norm_cbv redmode hyps f) with - | SFand (_, (f1, f2)) -> - destr_conjunction hyps f1 @ destr_conjunction hyps f2 - - | SFop ((p, _), [pred; lst]) when EcPath.p_equal p EcCoreLib.CI_List.p_all -> begin - match form_list_from_iota hyps lst with - | fs -> List.map (fun farg -> f_app pred [farg] tbool) fs - | exception DestrError _ -> [f] - end - - | _ -> [f] - -(* -------------------------------------------------------------------- *) -(* Should return a list of circuits corresponding to the atomic parts of the pre *) -(* - This means: - /\ p_i => [p_i]_i, - a = b => [a.[i] = b.[i]]_i -*) -(* Returns _open_ circuits *) -let process_pre ?(st : state option) (tc : tcenv1) (f : form) : - state * circuit list = - let hyps = FApi.tc1_hyps tc in - - (* Maybe move this to be a parameter and just supply it from outside *) - let st = - match st with - | Some st -> st - | None -> circuit_state_of_hyps hyps - in - - (* Takes in a form of the form /\_i f_i - and returns a list of the conjunction terms [ f_i ]*) - - let fs = destr_conjunction hyps f in - - (* If f is of the form (a_ = a) (aka prog_var = log_var) - then add it to the state, otherwise do nothing *) - (* Processes explicit equations *) - let process_equality (s : state) (f : form) : state = - let f = EcCallbyValue.norm_cbv (circ_red hyps) hyps f in - match sform_of_form f with - | SFeq (a, b) -> begin - match - ( EcCallbyValue.norm_cbv (circ_red hyps) hyps a, - EcCallbyValue.norm_cbv (circ_red hyps) hyps b ) - with - | {f_node = Fpvar (PVloc pv, m); _}, fv - | fv, {f_node = Fpvar (PVloc pv, m); _} -> - update_state_pv s m pv (circuit_of_form st hyps fv) - | _ -> s - end - | _ -> s - in - - let st = List.fold_left process_equality st fs in - - (* If convertible to circuit then add to precondition conjunction. - Use state from previous as well *) - let process_form (f : form) : circuit list = - match sform_of_form f with - | SFeq (f1, f2) -> - let c1 = - circuit_of_form st hyps (EcCallbyValue.norm_cbv (circ_red hyps) hyps f1) - in - let c2 = - circuit_of_form st hyps (EcCallbyValue.norm_cbv (circ_red hyps) hyps f2) - in - circuit_eqs c1 c2 - | _ -> begin - try - [ - circuit_of_form st hyps (EcCallbyValue.norm_cbv (circ_red hyps) hyps f); - ] - with _ -> [] - end - in - - let cs = - List.fold_left (fun acc f -> List.rev_append (process_form f) acc) [] fs - |> List.rev - in - st, cs - -(* -------------------------------------------------------------------- *) -let solve_post ~(st : state) ~(pres : circuit list) (hyps : hyps) (post : form) - : bool = - let env = toenv hyps in - let lap = EcCircuits.stopwatch env in - let posts = destr_conjunction hyps post in - lap "Done with postcondition normalization (destr_conj)"; - let pres = List.map (state_close_circuit st) pres in - - posts |> List.to_seq - |> Seq.concat_map (fun post -> - match sform_of_form post with - | SFeq (f1, f2) -> circuits_of_equality ~st ~hyps f1 f2 |> List.to_seq - | _ -> - Seq.return (circuit_of_form st hyps post |> state_close_circuit st)) - |> List.of_seq - |> circuit_check_posts ~env ~pres - +(* The [circuit] rules live in [rules//] ([EcHoareCircuit], + [EcEquivCircuit], [EcHoareCircuitSimplify], [EcHoareExtens]) and, for + the ones on formulas, in [rules/fol/] ([EcFolCircuit], [EcFolExtens]). + This module only keeps the dispatchers and the derived [extens]. *) let t_bdep_solve (tc : tcenv1) = - let hyps = FApi.tc1_hyps tc in - let goal = FApi.tc1_goal tc in - let env = FApi.tc1_env tc in - match goal.f_node with - | FhoareS hs -> begin - try - let lap = EcCircuits.stopwatch env in - let st = create_state (EcEnv.gstate env) in - let st = circuit_state_of_hyps ~st hyps in - let st = circuit_state_of_memenv ~st env hs.hs_m in - let st, cpres = process_pre ~st tc (hs_pr hs).inv in - lap "Done with precondition processing"; - - (* Get open state *) - let st = state_of_prog hyps (fst hs.hs_m) ~st hs.hs_s.s_node in - lap "Done with program circuit gen"; - - if not (POE.is_empty (hs_po hs).hsi_inv) then - tc_error !!tc "exception not supported"; - - let res = solve_post ~st ~pres:cpres hyps (POE.lower (hs_po hs)).inv in - EcCircuits.clear_translation_caches (); - if res then FApi.close !@tc VBdep - else tc_error (FApi.tc1_penv tc) "failed to verify postcondition" - with CircError err -> - tc_error (FApi.tc1_penv tc) "circuit solve failed with error: %a" - (pp_circ_error EcPrinting.PPEnv.(ofenv env)) - err - end - | FequivS es -> begin - try - let lap = EcCircuits.stopwatch env in - - let st = create_state (EcEnv.gstate env) in - - let st = circuit_state_of_hyps ~st hyps in - let st = circuit_state_of_memenv ~st (FApi.tc1_env tc) es.es_ml in - let st = circuit_state_of_memenv ~st (FApi.tc1_env tc) es.es_mr in - - let st, cpres = process_pre ~st tc (es_pr es).inv in - lap "Done with precondition processing"; - - (* Circuits from pvars are tagged by memory so we can just put everything in one state *) - let st = state_of_prog hyps (fst es.es_ml) ~st es.es_sl.s_node in - lap "Done with left program circuit gen"; - - let st = state_of_prog hyps (fst es.es_mr) ~st es.es_sr.s_node in - lap "Done with right program circuit gen"; - - if solve_post ~st ~pres:cpres hyps (es_po es).inv then - FApi.close !@tc VBdep - else tc_error (FApi.tc1_penv tc) "failed to verify postcondition" - with CircError err -> - tc_error (FApi.tc1_penv tc) "circuit solve failed with error: %a" - (pp_circ_error EcPrinting.PPEnv.(ofenv env)) - err - end - | _ -> begin - try - let ctxt = tohyps hyps in - assert (ctxt.h_tvar = []); - let st = circuit_state_of_hyps hyps in - let cgoal = circuit_of_form st hyps goal |> state_close_circuit st in - if circ_valid cgoal then FApi.close !@tc VBdep - else - tc_error (FApi.tc1_penv tc) - "Failed to solve goal through circuit reasoning@\n" - with CircError err -> - tc_error (FApi.tc1_penv tc) "circuit solve failed with error: %a" - (pp_circ_error EcPrinting.PPEnv.(ofenv env)) - err - end + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareCircuit.t_hoare_circuit tc + | FequivS _ -> EcEquivCircuit.t_equiv_circuit tc + | _ -> EcFolCircuit.t_fol_circuit tc (* -------------------------------------------------------------------- *) let t_bdep_simplify (tc : tcenv1) = - let hyps = FApi.tc1_hyps tc in - let goal = FApi.tc1_goal tc in - let env = FApi.tc1_env tc in - match goal.f_node with - | FhoareS hs -> begin - if not (POE.is_empty (hs_po hs).hsi_inv) then - tc_error !!tc "exceptions not supported"; - try - let m = fst hs.hs_m in - let lap = EcCircuits.stopwatch env in - let st = circuit_state_of_hyps hyps in - let st = circuit_state_of_memenv ~st env hs.hs_m in - let st, pres = process_pre ~st tc (hs_pr hs).inv in - lap "Done with precondition processing"; - - let st = EcCircuits.state_of_prog ~st hyps (fst hs.hs_m) hs.hs_s.s_node in - let post = - EcCallbyValue.norm_cbv (circ_red hyps) hyps (POE.lower (hs_po hs)).inv - in - - lap "Done with first simplify"; - let f = - EcCircuits.circ_simplify_form_bitstring_equality ~st ~pres hyps post - in - lap "Done with circuit simplify"; - let f = EcCallbyValue.norm_cbv EcReduction.full_red hyps f in - lap "Done with second simplify"; - let new_goal = - f_hoareS (snd hs.hs_m) {inv = (hs_pr hs).inv; m} hs.hs_s - (POE.lift {inv = f; m}) - in - - FApi.mutate1 tc (fun _ -> VBdep) new_goal |> FApi.tcenv_of_tcenv1 - with CircError err -> - tc_error (FApi.tc1_penv tc) "Circuit simplify failed with error: %a" - (pp_circ_error EcPrinting.PPEnv.(ofenv env)) - err - end + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareCircuitSimplify.t_hoare_circuit_simplify tc | _ -> assert false - (* -------------------------------------------------------------------- *) -let t_extens (v : string option) (tt : backward) (tc : tcenv1) = - (* Find goal shape - -> generate one goal for each value - -> solve goal by applying the tactic - *) - let lap = EcCircuits.stopwatch (tc1_env tc) in +(* Derived (no proof-node): the [extens] rule of the goal (enumeration of + the values of a program variable, or of an [all p (iota_ s n)]), then + [tt] on each of its premises, in order, which must close it. *) +let t_extens (v : string option) (tt : FApi.backward) (tc : tcenv1) = + let lap = EcCircuits.stopwatch (FApi.tc1_env tc) in - let rec do_all (goals : form list) = - match goals with - | [] -> None - | goal :: goals -> ( - let new_tc = mutate1 tc (fun _ -> VBdep) goal in - match t_try_base tt new_tc with - | `Failure e -> tc_error_exn (tc1_penv tc) e - | `Success new_tc -> ( - match tc_opened new_tc with - | [] -> - do_all goals - | hd :: _ -> Some (get_pregoal_by_id hd (tc_penv new_tc)).g_concl)) + let t_rule = + match (FApi.tc1_goal tc).f_node, v with + | FhoareS _, Some v -> EcHoareExtens.t_hoare_extens { her_var = v } + | _, None -> EcFolExtens.t_fol_extens + | _ -> tc_error !!tc "Wrong goal shape" in - let subst_pv_stmt - ?(redmode : EcReduction.reduction_info option) - (hyps : LDecl.hyps) - (mem : memory) - (sb : EcPV.PVM.subst) - (s : stmt) = - let redmode = Option.default (circ_red hyps) redmode in - let env = LDecl.toenv hyps in - stmt - (List.map - (fun i -> - match i.i_node with - | Sasgn (lv, e) -> - let f = ss_inv_of_expr mem e in - let fi = EcPV.PVM.subst env sb f.inv in - let fi = EcCallbyValue.norm_cbv redmode hyps fi in - let e = expr_of_ss_inv {f with inv = fi} in - EcCoreModules.i_asgn (lv, e) - | _ -> raise CannotTranslate) - s.s_node) - in - - let goals = - match sform_of_form (tc1_goal tc), v with - | SFop ((p, [tp]), [fpred; flist]), None - when EcPath.p_equal p EcCoreLib.CI_List.p_all && tp = tint -> - begin - match sform_of_form flist with - | SFop ((p, []), [fstart; flen]) - when EcPath.p_equal p EcCoreLib.CI_List.p_iota -> - let start = - match sform_of_form fstart with - | SFint i -> EcBigInt.to_int i - | _ -> tc_error (tc1_penv tc) "Iota start should be constant" - in - - let len = - match sform_of_form flen with - | SFint i -> EcBigInt.to_int i - | _ -> tc_error (tc1_penv tc) "Iota length should be constant" - in - - List.init len (fun i -> - EcTypesafeFol.f_app (tc1_hyps tc) fpred - [f_int EcBigInt.(of_int (i + start))]) - | _ -> tc_error (tc1_penv tc) "Unsupported List pattern" - end - | SFhoareS hs, Some v -> - if not (POE.is_empty (hs_po hs).hsi_inv) then - tc_error !!tc "exceptions not supported"; - - let m, mt = hs.hs_m in - let v = - match EcMemory.lookup v mt with - | Some (v, _, _) -> v - | None -> - tc_error (tc1_penv tc) "Failed to find var %s in memory %s" v - (EcIdent.name m) - in - let size = - match EcEnv.Circuit.lookup_bitstring_size (tc1_env tc) v.v_type with - | Some size -> size - | None -> - tc_error (tc1_penv tc) - "Failed to get size for type %a (is it finite and does it have a \ - binding to a bistring type (arrays unsupported)?)" - EcPrinting.(pp_type PPEnv.(ofenv (tc1_env tc))) - v.v_type - in - let tpath = - match v.v_type.ty_node with - | Tconstr (p, _) -> p - | _ -> tc_error (tc1_penv tc) "Failed to destructure var type" - in - let of_int = - match EcEnv.Circuit.reverse_type (tc1_env tc) tpath with - | [] -> tc_error (tc1_penv tc) "No bindings found for type of var" - | `Bitstring {ofint} :: _ -> ofint - | _ -> tc_error (tc1_penv tc) "Only finite size bitstring supported" - in - (* Each instance replaces [v] by a constant in the program, the - precondition and the postcondition. The postcondition reads [v] - in the final memory: this is only sound if the program does not - write [v]. *) - if EcPV.PV.mem_pv (tc1_env tc) (pv_loc v.v_name) - (EcPV.s_write (tc1_env tc) hs.hs_s) then - tc_error (tc1_penv tc) - "extens: the program writes the variable %s" v.v_name; - let ngoals = 1 lsl size in - List.init ngoals (fun i -> - let subst = - EcPV.PVM.( - add (tc1_env tc) (PVloc v.v_name) (fst hs.hs_m) - (EcTypesafeFol.f_op_app (tc1_env tc) of_int - [f_int BI.(of_int i)]) - empty) - in - let s = subst_pv_stmt (tc1_hyps tc) m subst hs.hs_s in - let subst = EcPV.PVM.subst (tc1_env tc) subst in - let pr = subst (hs_pr hs).inv in - let po = subst (POE.lower (hs_po hs)).inv in - f_hoareS mt {inv = pr; m} s (POE.lift {inv = po; m})) - | _ -> tc_error (tc1_penv tc) "Wrong goal shape" + let t_close (g : tcenv1) = + match FApi.t_try_base tt g with + | `Failure e -> tc_error_exn !!tc e + | `Success g -> begin + match FApi.tc_opened g with + | [] -> g + | hd :: _ -> + tc_error !!tc "Failed to close goal:@. %a" + EcPrinting.(pp_form PPEnv.(ofenv (FApi.tc1_env tc))) + (FApi.get_pregoal_by_id hd (FApi.tc_penv g)).g_concl + end in - match do_all goals with - | None -> - lap "Extens"; - close (tcenv_of_tcenv1 tc) VBdep - | Some gfail -> - tc_error (tc1_penv tc) "Failed to close goal:@. %a" - EcPrinting.(pp_form PPEnv.(ofenv (tc1_env tc))) - gfail false + let tc = FApi.t_onall t_close (t_rule tc) in + lap "Extens"; tc diff --git a/src/phl/rules/ecPlCircuit.ml b/src/phl/rules/ecPlCircuit.ml new file mode 100644 index 000000000..f594cc159 --- /dev/null +++ b/src/phl/rules/ecPlCircuit.ml @@ -0,0 +1,108 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv +open EcTypes +open EcFol +open EcLowCircuits +open EcCircuits + +(* -------------------------------------------------------------------- *) +exception CircuitInvalid +exception CircuitExceptions + +(* -------------------------------------------------------------------- *) +let form_list_from_iota (hyps : LDecl.hyps) (f : form) : form list = + match sform_of_form f with + | SFop ((p, _), [n; m]) when EcPath.p_equal p EcCoreLib.CI_List.p_iota -> + let n = int_of_form hyps n in + let m = int_of_form hyps m in + List.init (BI.to_int m) (fun i -> f_int BI.(add n (of_int i))) + | _ -> raise (DestrError "iota") + +(* -------------------------------------------------------------------- *) +let rec destr_conjunction (hyps : LDecl.hyps) (f : form) : form list = + let redmode = { (circ_red hyps) with zeta = false } in + + match sform_of_form (EcCallbyValue.norm_cbv redmode hyps f) with + | SFand (_, (f1, f2)) -> + destr_conjunction hyps f1 @ destr_conjunction hyps f2 + + | SFop ((p, _), [pred; lst]) when EcPath.p_equal p EcCoreLib.CI_List.p_all -> begin + match form_list_from_iota hyps lst with + | fs -> List.map (fun farg -> f_app pred [farg] tbool) fs + | exception DestrError _ -> [f] + end + + | _ -> [f] + +(* -------------------------------------------------------------------- *) +(* The atomic parts of the precondition, as _open_ circuits: + /\ p_i => [p_i]_i, + a = b => [a.[i] = b.[i]]_i + The explicit equations [pv = v] (program variable = value) are first + recorded in the state. *) +let process_pre (hyps : LDecl.hyps) ~(st : state) (f : form) : + state * circuit list = + let fs = destr_conjunction hyps f in + + let process_equality (s : state) (f : form) : state = + let f = EcCallbyValue.norm_cbv (circ_red hyps) hyps f in + match sform_of_form f with + | SFeq (a, b) -> begin + match + ( EcCallbyValue.norm_cbv (circ_red hyps) hyps a, + EcCallbyValue.norm_cbv (circ_red hyps) hyps b ) + with + | {f_node = Fpvar (PVloc pv, m); _}, fv + | fv, {f_node = Fpvar (PVloc pv, m); _} -> + update_state_pv s m pv (circuit_of_form st hyps fv) + | _ -> s + end + | _ -> s + in + + let st = List.fold_left process_equality st fs in + + (* The conjuncts convertible to circuits, in the state above. *) + let process_form (f : form) : circuit list = + match sform_of_form f with + | SFeq (f1, f2) -> + let c1 = + circuit_of_form st hyps (EcCallbyValue.norm_cbv (circ_red hyps) hyps f1) + in + let c2 = + circuit_of_form st hyps (EcCallbyValue.norm_cbv (circ_red hyps) hyps f2) + in + circuit_eqs c1 c2 + | _ -> begin + try + [ + circuit_of_form st hyps (EcCallbyValue.norm_cbv (circ_red hyps) hyps f); + ] + with _ -> [] + end + in + + let cs = + List.fold_left (fun acc f -> List.rev_append (process_form f) acc) [] fs + |> List.rev + in + st, cs + +(* -------------------------------------------------------------------- *) +let solve_post ~(st : state) ~(pres : circuit list) (hyps : LDecl.hyps) (post : form) + : bool = + let env = LDecl.toenv hyps in + let lap = EcCircuits.stopwatch env in + let posts = destr_conjunction hyps post in + lap "Done with postcondition normalization (destr_conj)"; + let pres = List.map (state_close_circuit st) pres in + + posts |> List.to_seq + |> Seq.concat_map (fun post -> + match sform_of_form post with + | SFeq (f1, f2) -> circuits_of_equality ~st ~hyps f1 f2 |> List.to_seq + | _ -> + Seq.return (circuit_of_form st hyps post |> state_close_circuit st)) + |> List.of_seq + |> circuit_check_posts ~env ~pres diff --git a/src/phl/rules/ecPlCircuit.mli b/src/phl/rules/ecPlCircuit.mli new file mode 100644 index 000000000..3769903c7 --- /dev/null +++ b/src/phl/rules/ecPlCircuit.mli @@ -0,0 +1,36 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv +open EcLowCircuits + +(* -------------------------------------------------------------------- *) +(* Circuit reasoning on statement judgements, shared by the [circuit] + rules of every logic: the precondition and the program are translated + to circuits, and the postcondition is decided by the circuit backend + ([EcCircuits]). The translation and the decision are deterministic + functions of the judgement and of its hypotheses (the bindings of the + environment included), so that a checker can re-run them. *) + +(* Raised by the builders of the [circuit] rules when the circuit backend + does not establish the goal. *) +exception CircuitInvalid + +(* Raised by the builders of the hoare [circuit] rules when the + exceptional postconditions are not empty. *) +exception CircuitExceptions + +(* [process_pre hyps ~st P] records in [st] the conjuncts of [P] of the + form [x = v] ([x] a local program variable) as the value of [x], and + returns the conjuncts of [P] translatable to circuits, as open circuits + in that state. The conjuncts of [P] are its top-level conjunctions, + [all p (iota_ n m)] being the conjunction of [p n], ..., [p (n+m-1)] + (for [n] and [m] integer literals). *) +val process_pre : + LDecl.hyps -> st:state -> form -> state * circuit list + +(* [solve_post ~st ~pres hyps Q] decides whether each conjunct of [Q] + (as in [process_pre]; equalities compared bit-wise) holds in the state + [st] under the assumptions [pres]. Raises [EcCircuits.CircError] when + a conjunct cannot be translated. *) +val solve_post : + st:state -> pres:circuit list -> LDecl.hyps -> form -> bool diff --git a/src/phl/rules/equiv/ecEquivCircuit.ml b/src/phl/rules/equiv/ecEquivCircuit.ml new file mode 100644 index 000000000..5ae9030b5 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivCircuit.ml @@ -0,0 +1,67 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcLowCircuits +open EcCircuits +open EcPlCircuit + +(* -------------------------------------------------------------------- *) +(* The equiv [circuit] rule has no parameters: the decision is a function + of the goal. *) +type EcCoreGoal.rule += REquivCircuit + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: it runs the circuit + decision (no subgoal), raising [CircuitInvalid] (or [CircError]) when + it does not establish the judgement, so the checker re-runs the + decision. *) +let equiv_circuit_subgoals (hyps : LDecl.hyps) (es : equivS) : form list = + let env = LDecl.toenv hyps in + let lap = stopwatch env in + + let st = create_state (EcEnv.gstate env) in + + let st = circuit_state_of_hyps ~st hyps in + let st = circuit_state_of_memenv ~st env es.es_ml in + let st = circuit_state_of_memenv ~st env es.es_mr in + + let st, cpres = process_pre hyps ~st (es_pr es).inv in + lap "Done with precondition processing"; + + (* Circuits from pvars are tagged by memory so we can just put + everything in one state *) + let st = state_of_prog hyps (fst es.es_ml) ~st es.es_sl.s_node in + lap "Done with left program circuit gen"; + + let st = state_of_prog hyps (fst es.es_mr) ~st es.es_sr.s_node in + lap "Done with right program circuit gen"; + + if not (solve_post ~st ~pres:cpres hyps (es_po es).inv) then + raise CircuitInvalid; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equiv_circuit (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_circuit_subgoals (FApi.tc1_hyps tc) es with + | CircuitInvalid -> + tc_error !!tc "failed to verify postcondition" + | CircError err -> + tc_error !!tc "circuit solve failed with error: %a" + (pp_circ_error EcPrinting.PPEnv.(ofenv (FApi.tc1_env tc))) + err + in FApi.xrule1 tc REquivCircuit sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivCircuit -> + Some (EcPlRecheck.checker_of "equiv-circuit" pf_as_equivS + equiv_circuit_subgoals) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivCircuit.mli b/src/phl/rules/equiv/ecEquivCircuit.mli new file mode 100644 index 000000000..53961af3c --- /dev/null +++ b/src/phl/rules/equiv/ecEquivCircuit.mli @@ -0,0 +1,27 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equiv_circuit] — decision by circuits ([circuit]): + + ---------------------------- (no premise) + equiv [c1 ~ c2 : P ==> Q] + + Side conditions (otherwise fails): [c1] and [c2] only contain + assignments to local program variables, translatable to circuits; + every conjunct of [Q] (as in [EcPlCircuit.solve_post]) is valid, as + decided by the circuit backend, in the state obtained by running [c1] + (on the left memory) then [c2] (on the right memory) on the inputs, + under the conjuncts of [P] that translate to circuits + ([EcPlCircuit.process_pre]), the equations [x = v] of [P] and of the + hypotheses fixing the initial value of [x], the local definitions of + the context fixing their values, and the other locals of the context + and the program variables of both memories as inputs ("failed to + verify postcondition" otherwise, "circuit solve failed with error: + ..." when a translation fails). + + Node: [REquivCircuit]. Checker: "equiv-circuit" (re-runs the + decision: expensive, only under [EC_RECHECK]). *) +val t_equiv_circuit : backward diff --git a/src/phl/rules/fol/ecFolCircuit.ml b/src/phl/rules/fol/ecFolCircuit.ml new file mode 100644 index 000000000..46407deb1 --- /dev/null +++ b/src/phl/rules/fol/ecFolCircuit.ml @@ -0,0 +1,47 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcEnv + +open EcCoreGoal +open EcLowCircuits +open EcCircuits +open EcPlCircuit + +(* -------------------------------------------------------------------- *) +(* The [circuit] rule on formulas has no parameters: the decision is a + function of the goal. *) +type EcCoreGoal.rule += RFolCircuit + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: it runs the circuit + decision (no subgoal), raising [CircuitInvalid] (or [CircError]) when + it does not establish the goal, so the checker re-runs the decision. *) +let fol_circuit_subgoals (hyps : LDecl.hyps) (f : form) : form list = + let ctxt = LDecl.tohyps hyps in + assert (ctxt.h_tvar = []); + let st = circuit_state_of_hyps hyps in + let cgoal = circuit_of_form st hyps f |> state_close_circuit st in + if not (circ_valid cgoal) then raise CircuitInvalid; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_fol_circuit (tc : tcenv1) = + let sg = + try fol_circuit_subgoals (FApi.tc1_hyps tc) (FApi.tc1_goal tc) with + | CircuitInvalid -> + tc_error !!tc "Failed to solve goal through circuit reasoning@\n" + | CircError err -> + tc_error !!tc "circuit solve failed with error: %a" + (pp_circ_error EcPrinting.PPEnv.(ofenv (FApi.tc1_env tc))) + err + in FApi.xrule1 tc RFolCircuit sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RFolCircuit -> + Some (EcPlRecheck.checker_of "fol-circuit" (fun _ f -> f) + fol_circuit_subgoals) + | _ -> None) diff --git a/src/phl/rules/fol/ecFolCircuit.mli b/src/phl/rules/fol/ecFolCircuit.mli new file mode 100644 index 000000000..65ff790e0 --- /dev/null +++ b/src/phl/rules/fol/ecFolCircuit.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_fol_circuit] — decision of a formula by circuits ([circuit] on a + goal that is not a hoare or equiv judgement on statements): + + ------------ (no premise) + Γ ⊢ φ + + Side conditions (otherwise fails): [Γ] binds no type variable + (assertion); [φ] translates to a circuit (the local definitions of + [Γ] fixing the values of their locals, the equations [x{m} = v] of + [Γ] the values of the program variables, the other locals of [Γ] and + the program variables of its memories being inputs) that the circuit + backend decides valid ("Failed to solve goal through circuit + reasoning" otherwise, "circuit solve failed with error: ..." when the + translation fails). + + Node: [RFolCircuit]. Checker: "fol-circuit" (re-runs the decision: + expensive, only under [EC_RECHECK]). *) +val t_fol_circuit : backward diff --git a/src/phl/rules/fol/ecFolExtens.ml b/src/phl/rules/fol/ecFolExtens.ml new file mode 100644 index 000000000..053973f28 --- /dev/null +++ b/src/phl/rules/fol/ecFolExtens.ml @@ -0,0 +1,67 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* The [extens] rule on [all p (iota_ s n)] has no parameters: [s] and [n] + are integer literals read from the goal. *) +type EcCoreGoal.rule += RFolExtens + +(* -------------------------------------------------------------------- *) +exception InvalidExtens of string + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + goal is [all p (iota_ s n)], [s] and [n] integer literals) is part of + it, so the checker re-validates it. Raises [InvalidExtens] + otherwise. *) +let fol_extens_subgoals (hyps : LDecl.hyps) (f : form) : form list = + let invalid msg = raise (InvalidExtens msg) in + match sform_of_form f with + | SFop ((p, [tp]), [fpred; flist]) + when EcPath.p_equal p EcCoreLib.CI_List.p_all + && EcTypes.ty_equal tp EcTypes.tint + -> begin + match sform_of_form flist with + | SFop ((p, []), [fstart; flen]) + when EcPath.p_equal p EcCoreLib.CI_List.p_iota -> + let start = + match sform_of_form fstart with + | SFint i -> EcBigInt.to_int i + | _ -> invalid "Iota start should be constant" + in + + let len = + match sform_of_form flen with + | SFint i -> EcBigInt.to_int i + | _ -> invalid "Iota length should be constant" + in + + List.init len (fun i -> + EcTypesafeFol.f_app hyps fpred + [f_int EcBigInt.(of_int (i + start))]) + + | _ -> invalid "Unsupported List pattern" + end + + | _ -> invalid "Wrong goal shape" + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_fol_extens (tc : tcenv1) = + let sg = + try fol_extens_subgoals (FApi.tc1_hyps tc) (FApi.tc1_goal tc) + with InvalidExtens msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RFolExtens sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RFolExtens -> + Some (EcPlRecheck.checker_of "fol-extens" (fun _ f -> f) + fol_extens_subgoals) + | _ -> None) diff --git a/src/phl/rules/fol/ecFolExtens.mli b/src/phl/rules/fol/ecFolExtens.mli new file mode 100644 index 000000000..8965a0c5a --- /dev/null +++ b/src/phl/rules/fol/ecFolExtens.mli @@ -0,0 +1,31 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_fol_extens] — enumeration of a bounded quantification over the + integers ([extens] on a formula): + + Γ ⊢ p s Γ ⊢ p (s+1) ... Γ ⊢ p (s+n-1) + ------------------------------------------------- s, n integer + Γ ⊢ all p (iota_ s n) literals + + [p (s+i)] being [p] applied to the literal [s+i], head-reduced + ([EcTypesafeFol.f_app]). Side conditions (otherwise fails): the goal + is [all p l], [p] a predicate on [int] ("Wrong goal shape"), [l] is + [iota_ s n] ("Unsupported List pattern"), [s] and [n] are integer + literals ("Iota start should be constant", "Iota length should be + constant"). + + Node: [RFolExtens]. Checker: "fol-extens". *) +val t_fol_extens : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [EcPhlBDep.t_extens None tt] — [extens : tt]: [t_fol_extens], then + [tt] on each premise, in order, which must close it (otherwise fails + with the error of [tt], or with "Failed to close goal: ..." and the + first goal [tt] leaves). No visible goal. Emits no node of its own: + the proofs of the premises are kept (and rechecked). *) diff --git a/src/phl/rules/hoare/ecHoareCircuit.ml b/src/phl/rules/hoare/ecHoareCircuit.ml new file mode 100644 index 000000000..0eb636eb8 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCircuit.ml @@ -0,0 +1,65 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcLowCircuits +open EcCircuits +open EcPlCircuit + +(* -------------------------------------------------------------------- *) +(* The hoare [circuit] rule has no parameters: the decision is a function + of the goal. *) +type EcCoreGoal.rule += RHoareCircuit + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: it runs the circuit + decision (no subgoal), raising [CircuitExceptions] / [CircuitInvalid] + (or [CircError]) when it does not establish the judgement, so the + checker re-runs the decision. *) +let hoare_circuit_subgoals (hyps : LDecl.hyps) (hs : sHoareS) : form list = + let env = LDecl.toenv hyps in + let lap = stopwatch env in + let st = create_state (EcEnv.gstate env) in + let st = circuit_state_of_hyps ~st hyps in + let st = circuit_state_of_memenv ~st env hs.hs_m in + let st, cpres = process_pre hyps ~st (hs_pr hs).inv in + lap "Done with precondition processing"; + + (* Get open state *) + let st = state_of_prog hyps (fst hs.hs_m) ~st hs.hs_s.s_node in + lap "Done with program circuit gen"; + + if not (POE.is_empty (hs_po hs).hsi_inv) then + raise CircuitExceptions; + + let res = solve_post ~st ~pres:cpres hyps (POE.lower (hs_po hs)).inv in + clear_translation_caches (); + if not res then raise CircuitInvalid; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_circuit (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_circuit_subgoals (FApi.tc1_hyps tc) hs with + | CircuitExceptions -> + tc_error !!tc "exception not supported" + | CircuitInvalid -> + tc_error !!tc "failed to verify postcondition" + | CircError err -> + tc_error !!tc "circuit solve failed with error: %a" + (pp_circ_error EcPrinting.PPEnv.(ofenv (FApi.tc1_env tc))) + err + in FApi.xrule1 tc RHoareCircuit sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareCircuit -> + Some (EcPlRecheck.checker_of "hoare-circuit" pf_as_hoareS + hoare_circuit_subgoals) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareCircuit.mli b/src/phl/rules/hoare/ecHoareCircuit.mli new file mode 100644 index 000000000..7387a5785 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCircuit.mli @@ -0,0 +1,27 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_circuit] — decision by circuits ([circuit]): + + --------------------------- (no premise) + hoare [c : P ==> Q | E] + + Side conditions (otherwise fails): [c] only contains assignments to + local program variables, translatable to circuits; [E] is empty + ("exception not supported", checked after the translation of [P] and + [c]); every conjunct of [Q] (as in [EcPlCircuit.solve_post]) is + valid, as decided by the circuit backend, in the state obtained by + running [c] on the inputs, under the conjuncts of [P] that translate + to circuits ([EcPlCircuit.process_pre]), the equations [x = v] of [P] + and of the hypotheses fixing the initial value of [x], the local + definitions of the context fixing their values, and the other locals + of the context and the program variables of the memory as inputs + ("failed to verify postcondition" otherwise, "circuit solve failed + with error: ..." when a translation fails). + + Node: [RHoareCircuit]. Checker: "hoare-circuit" (re-runs the + decision: expensive, only under [EC_RECHECK]). *) +val t_hoare_circuit : backward diff --git a/src/phl/rules/hoare/ecHoareCircuitSimplify.ml b/src/phl/rules/hoare/ecHoareCircuitSimplify.ml new file mode 100644 index 000000000..e9a0a8593 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCircuitSimplify.ml @@ -0,0 +1,68 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcCircuits +open EcPlCircuit + +(* -------------------------------------------------------------------- *) +(* The hoare [circuit simplify] rule has no parameters: the simplified + postcondition is a function of the goal. *) +type EcCoreGoal.rule += RHoareCircuitSimplify + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: it re-runs the circuit + simplification of the postcondition, so the checker compares the + recorded premise with its result. Raises [CircuitExceptions] when the + exceptional postconditions are not empty. *) +let hoare_circuit_simplify_subgoals (hyps : LDecl.hyps) (hs : sHoareS) : + form list = + if not (POE.is_empty (hs_po hs).hsi_inv) then + raise CircuitExceptions; + + let env = LDecl.toenv hyps in + let m = fst hs.hs_m in + let lap = stopwatch env in + let st = circuit_state_of_hyps hyps in + let st = circuit_state_of_memenv ~st env hs.hs_m in + let st, pres = process_pre hyps ~st (hs_pr hs).inv in + lap "Done with precondition processing"; + + let st = state_of_prog ~st hyps m hs.hs_s.s_node in + let post = + EcCallbyValue.norm_cbv (circ_red hyps) hyps (POE.lower (hs_po hs)).inv + in + + lap "Done with first simplify"; + let f = circ_simplify_form_bitstring_equality ~st ~pres hyps post in + lap "Done with circuit simplify"; + let f = EcCallbyValue.norm_cbv EcReduction.full_red hyps f in + lap "Done with second simplify"; + [f_hoareS (snd hs.hs_m) {inv = (hs_pr hs).inv; m} hs.hs_s + (POE.lift {inv = f; m})] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_circuit_simplify (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + if not (POE.is_empty (hs_po hs).hsi_inv) then + tc_error !!tc "exceptions not supported"; + let sg = + try hoare_circuit_simplify_subgoals (FApi.tc1_hyps tc) hs with + | CircError err -> + tc_error !!tc "Circuit simplify failed with error: %a" + (pp_circ_error EcPrinting.PPEnv.(ofenv (FApi.tc1_env tc))) + err + in FApi.xrule1 tc RHoareCircuitSimplify sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareCircuitSimplify -> + Some (EcPlRecheck.checker_of "hoare-circuit-simplify" pf_as_hoareS + hoare_circuit_simplify_subgoals) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareCircuitSimplify.mli b/src/phl/rules/hoare/ecHoareCircuitSimplify.mli new file mode 100644 index 000000000..a71421d0b --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCircuitSimplify.mli @@ -0,0 +1,30 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_circuit_simplify] — simplification of the postcondition by + circuits ([circuit simplify]): + + hoare [c : P ==> Q'] + ------------------------ Q' = simpl(Q) + hoare [c : P ==> Q] + + where [simpl(Q)] is [Q] (normalized, operators bound to circuits + being kept folded) in which every equality [a = b] between values of + a type bound to a bitstring or an array is replaced by [true] when + the circuit backend decides it valid, in the state obtained by + running [c] on the inputs, under the conjuncts of [P] that translate + to circuits ([EcPlCircuit.process_pre]), and kept otherwise (it may + still hold in some states: replacing it by [false] would be unsound + under a negation); the result is then normalized. Side conditions (otherwise fails): the + exceptional postconditions of the goal are empty ("exceptions not + supported"); [c] only contains assignments to local program + variables, translatable to circuits, and so are the replaced + equalities ("Circuit simplify failed with error: ..."). The premise + has no exceptional postcondition. + + Node: [RHoareCircuitSimplify]. Checker: "hoare-circuit-simplify" + (re-runs the simplification: expensive, only under [EC_RECHECK]). *) +val t_hoare_circuit_simplify : backward diff --git a/src/phl/rules/hoare/ecHoareExtens.ml b/src/phl/rules/hoare/ecHoareExtens.ml new file mode 100644 index 000000000..262b508ab --- /dev/null +++ b/src/phl/rules/hoare/ecHoareExtens.ml @@ -0,0 +1,148 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Argument of the hoare [extens] rule: the enumerated variable, by name. + The node records it resolved in the memory of the goal. *) +type hoare_extens_rule = { + her_var : symbol; +} + +type hoare_extens_node = { + hen_var : variable; +} + +type EcCoreGoal.rule += RHoareExtens of hoare_extens_node + +(* -------------------------------------------------------------------- *) +exception InvalidExtens of string + +let invalid fmt = Format.kasprintf (fun msg -> raise (InvalidExtens msg)) fmt + +(* -------------------------------------------------------------------- *) +(* The size and the [of_int] operator of the bitstring bound to [ty]. *) +let bitstring_binding (env : env) (ty : ty) : int * EcPath.path = + let size = + match EcEnv.Circuit.lookup_bitstring_size env ty with + | Some size -> size + | None -> + invalid + "Failed to get size for type %a (is it finite and does it have a \ + binding to a bistring type (arrays unsupported)?)" + EcPrinting.(pp_type PPEnv.(ofenv env)) + ty + in + let tpath = + match ty.ty_node with + | Tconstr (p, _) -> p + | _ -> invalid "Failed to destructure var type" + in + let of_int = + match EcEnv.Circuit.reverse_type env tpath with + | [] -> invalid "No bindings found for type of var" + | `Bitstring {ofint} :: _ -> ofint + | _ -> invalid "Only finite size bitstring supported" + in + size, of_int + +(* -------------------------------------------------------------------- *) +(* [s] in which the program variables are substituted by [sb] in the + right-hand sides of its assignments (normalized); [s] contains only + assignments. *) +let subst_pv_stmt + (hyps : LDecl.hyps) (mem : memory) (sb : EcPV.PVM.subst) (s : stmt) += + let redmode = EcCircuits.circ_red hyps in + let env = LDecl.toenv hyps in + stmt + (List.map + (fun i -> + match i.i_node with + | Sasgn (lv, e) -> + let f = ss_inv_of_expr mem e in + let fi = EcPV.PVM.subst env sb f.inv in + let fi = EcCallbyValue.norm_cbv redmode hyps fi in + let e = expr_of_ss_inv {f with inv = fi} in + EcCoreModules.i_asgn (lv, e) + | _ -> raise CannotTranslate) + s.s_node) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (no + exceptional postcondition, [x] a variable of the memory whose type is + bound to a bitstring, not written by the program) are part of it, so + the checker re-validates them. Raises [InvalidExtens] when they do not hold, [CannotTranslate] + when the statement is not made of assignments. *) +let hoare_extens_subgoals + (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_extens_node) += + let env = LDecl.toenv hyps in + if not (POE.is_empty (hs_po hs).hsi_inv) then + invalid "exceptions not supported"; + + let m, mt = hs.hs_m in + let v = n.hen_var in + begin match EcMemory.lookup v.v_name mt with + | Some (v', _, _) when v'.v_name = v.v_name + && EcTypes.ty_equal v'.v_type v.v_type -> () + | _ -> + invalid "Failed to find var %s in memory %s" v.v_name (EcIdent.name m) + end; + + let size, of_int = bitstring_binding env v.v_type in + + (* Each instance replaces [v] by a constant in the program, the + precondition and the postcondition. The postcondition reads [v] in + the final memory: this is only sound if the program does not write + [v]. *) + if EcPV.PV.mem_pv env (EcTypes.pv_loc v.v_name) (EcPV.s_write env hs.hs_s) then + invalid "extens: the program writes the variable %s" v.v_name; + + List.init (1 lsl size) (fun i -> + let subst = + EcPV.PVM.( + add env (PVloc v.v_name) m + (EcTypesafeFol.f_op_app env of_int [f_int BI.(of_int i)]) + empty) + in + let s = subst_pv_stmt hyps m subst hs.hs_s in + let subst = EcPV.PVM.subst env subst in + let pr = subst (hs_pr hs).inv in + let po = subst (POE.lower (hs_po hs)).inv in + f_hoareS mt {inv = pr; m} s (POE.lift {inv = po; m})) + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_extens (r : hoare_extens_rule) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + if not (POE.is_empty (hs_po hs).hsi_inv) then + tc_error !!tc "exceptions not supported"; + + let m, mt = hs.hs_m in + let v = + match EcMemory.lookup r.her_var mt with + | Some (v, _, _) -> v + | None -> + tc_error !!tc "Failed to find var %s in memory %s" r.her_var + (EcIdent.name m) + in + let n = { hen_var = v } in + let sg = + try hoare_extens_subgoals (FApi.tc1_hyps tc) hs n + with InvalidExtens msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RHoareExtens n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareExtens n -> + Some (EcPlRecheck.checker_of "hoare-extens" pf_as_hoareS + (fun hyps hs -> hoare_extens_subgoals hyps hs n)) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareExtens.mli b/src/phl/rules/hoare/ecHoareExtens.mli new file mode 100644 index 000000000..7c2418beb --- /dev/null +++ b/src/phl/rules/hoare/ecHoareExtens.mli @@ -0,0 +1,51 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcAst +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_extens_rule = { + her_var : symbol; (* the enumerated program variable, by name *) +} + +type hoare_extens_node = { + hen_var : variable; (* the enumerated program variable, resolved in + the memory of the goal *) +} + +(* [t_hoare_extens { her_var = x }] — enumeration of the values of a + program variable ([extens [x]] on a hoare goal): + + hoare [c_0 : P_0 ==> Q_0] ... hoare [c_(2^k-1) : P_(2^k-1) ==> Q_(2^k-1)] + ------------------------------------------------------------------------------ + hoare [c : P ==> Q | E] + + where [x] is a local program variable of the memory [m] of the goal, + of a type bound to a bitstring of size [k] with operator [of_int], and, + for each [i], with [w_i = of_int i]: [P_i = P[x{m} := w_i]], + [Q_i = Q[x{m} := w_i]], and [c_i] is [c] in which [x] is replaced by + [w_i] in the right-hand side of every assignment (normalized), the + left-hand sides being kept. Side conditions (otherwise fails): [E] is + empty ("exceptions not supported"); [x] is a variable of [m] ("Failed + to find var x in memory m"); its type is bound to a bitstring ("Failed + to get size for type ...", "Failed to destructure var type", "No + bindings found for type of var", "Only finite size bitstring + supported"); [c] does not write [x] ("extens: the program writes the + variable x": [Q] reads [x] in the final memory); [c] only contains + assignments (raises [EcCoreFol.CannotTranslate]). The premises have + no exceptional postcondition. + + Node: [RHoareExtens { hen_var = x (resolved) }] ([k] and [of_int] are + read from the binding of its type). Checker: "hoare-extens". *) +val t_hoare_extens : hoare_extens_rule -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [EcPhlBDep.t_extens (Some x) tt] — [extens [x] : tt]: [t_hoare_extens + { her_var = x }], then [tt] on each premise, in order, which must close + it (otherwise fails with the error of [tt], or with "Failed to close + goal: ..." and the first goal [tt] leaves). No visible goal. Emits no + node of its own: the proofs of the premises are kept (and rechecked). *) diff --git a/tests/circuits/circuit_rules.ec b/tests/circuits/circuit_rules.ec new file mode 100644 index 000000000..3bc726bd6 --- /dev/null +++ b/tests/circuits/circuit_rules.ec @@ -0,0 +1,158 @@ +(* The [circuit], [circuit simplify] and [extens] rules: every form and + the error paths. *) + +require import AllCore List QFABV. + +type W8. + +op to_bits : W8 -> bool list. +op from_bits : bool list -> W8. +op of_int : int -> W8. +op to_uint : W8 -> int. +op to_sint : W8 -> int. + +bind bitstring to_bits from_bits to_uint to_sint of_int W8 8. +realize gt0_size by admit. +realize tolistP by admit. +realize oflistP by admit. +realize touintP by admit. +realize tosintP by admit. +realize ofintP by admit. +realize size_tolist by admit. + +op (+^) : W8 -> W8 -> W8. +bind op W8 (+^) "xor". +realize bvxorP by admit. + +op "_.[_]" : W8 -> int -> bool. + +exception oops. + +module M = { + proc test (a : W8, b : W8) = { + var c : W8; + c <- a +^ b; + return c; + } + + proc swp (a : W8, b : W8) = { + var c : W8; + c <- b +^ a; + return c; + } + + proc cnt (a : W8, n : int) = { + var c : W8; + c <- a; + n <- n + 1; + return c; + } + + proc rse (a : W8) = { + if (a = of_int 0) { raise oops; } + return a; + } +}. + +(* -------------------------------------------------------------------- *) +(* [circuit]: hoare, equiv and formulas. *) +lemma hoare_circuit (a_ b_ : W8) : + hoare[M.test : a_ = a /\ b_ = b ==> res = a_ +^ b_]. +proof. by proc; circuit. qed. + +lemma equiv_circuit : equiv[M.test ~ M.swp : ={a, b} ==> ={res}]. +proof. by proc; circuit. qed. + +lemma fol_circuit (w1 w2 : W8) : w1 +^ w2 = w2 +^ w1. +proof. by circuit. qed. + +(* The decision fails. *) +lemma hoare_circuit_invalid (a_ b_ : W8) : + hoare[M.test : a_ = a /\ b_ = b ==> res = a_]. +proof. proc. fail circuit. abort. + +lemma equiv_circuit_invalid : equiv[M.test ~ M.swp : ={a} ==> ={res}]. +proof. proc. fail circuit. abort. + +lemma fol_circuit_invalid (w1 w2 : W8) : w1 +^ w2 = w1. +proof. fail circuit. abort. + +(* The translation fails ([int] is not bound). *) +lemma hoare_circuit_untranslatable (a_ : W8) : + hoare[M.cnt : a_ = a ==> res = a_]. +proof. proc. fail circuit. abort. + +lemma fol_circuit_untranslatable (w : W8) : w.[0] = w.[1]. +proof. fail circuit. abort. + +(* Exceptional postconditions are not supported. *) +lemma hoare_circuit_exn (a_ : W8) : + hoare[M.test : a_ = a ==> true | oops => true]. +proof. proc. fail circuit. abort. + +(* -------------------------------------------------------------------- *) +(* [circuit simplify]. *) +lemma hoare_circuit_simplify (a_ b_ : W8) : + hoare[M.test : a_ = a /\ b_ = b ==> res = a_ +^ b_ /\ (res = a_ \/ true)]. +proof. by proc; circuit simplify. qed. + +lemma hoare_circuit_simplify_exn (a_ : W8) : + hoare[M.test : a_ = a ==> true | oops => true]. +proof. proc. fail circuit simplify. abort. + +lemma hoare_circuit_simplify_untranslatable (a_ : W8) : + hoare[M.cnt : a_ = a ==> res = a_]. +proof. proc. fail circuit simplify. abort. + +(* -------------------------------------------------------------------- *) +(* [extens]: hoare (enumeration of a program variable) and formulas + ([all p (iota_ s n)]). *) +lemma hoare_extens (a_ b_ : W8) : + hoare[M.test : a_ = a /\ b_ = b ==> res = a_ +^ b_]. +proof. by proc; extens [a] : circuit. qed. + +lemma fol_extens : all (fun i => 0 <= i) (iota_ 3 5). +proof. by extens : trivial. qed. + +lemma fol_extens_empty : all (fun (i : int) => false) (iota_ 3 0). +proof. by extens : trivial. qed. + +(* Wrong goal shapes. *) +lemma hoare_extens_novar (a_ b_ : W8) : + hoare[M.test : a_ = a /\ b_ = b ==> res = a_ +^ b_]. +proof. proc. fail extens : circuit. abort. + +lemma fol_extens_var : all (fun i => 0 <= i) (iota_ 3 5). +proof. fail extens [a] : trivial. abort. + +lemma fol_extens_notint : all (fun (b : bool) => b \/ !b) [true; false]. +proof. fail extens : trivial. abort. + +lemma fol_extens_list : all (fun i => 0 <= i) [1; 2]. +proof. fail extens : trivial. abort. + +lemma fol_extens_start (s : int) : all (fun i => 0 <= i - s) (iota_ s 5). +proof. fail extens : trivial. abort. + +lemma fol_extens_len (n : int) : all (fun i => 0 <= i) (iota_ 0 n). +proof. fail extens : trivial. abort. + +(* The variable is not in the memory, or its type is not bound. *) +lemma hoare_extens_unknown (a_ b_ : W8) : + hoare[M.test : a_ = a /\ b_ = b ==> res = a_ +^ b_]. +proof. proc. fail extens [z] : circuit. abort. + +lemma hoare_extens_unbound (a_ : W8) : + hoare[M.cnt : a_ = a ==> res = a_]. +proof. proc. fail extens [n] : circuit. abort. + +lemma hoare_extens_exn (a_ : W8) : + hoare[M.test : a_ = a ==> true | oops => true]. +proof. proc. fail extens [a] : circuit. abort. + +(* The tactic fails on, or does not close, an instance. *) +lemma fol_extens_fails : all (fun i => i <> 5) (iota_ 3 5). +proof. fail extens : (move=> /=; done). abort. + +lemma fol_extens_open : all (fun i => i <> 5) (iota_ 3 5). +proof. fail extens : idtac. abort.