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.