diff --git a/src/phl/ecPhlSkip.ml b/src/phl/ecPhlSkip.ml index db7c40e37..2605589e4 100644 --- a/src/phl/ecPhlSkip.ml +++ b/src/phl/ecPhlSkip.ml @@ -1,95 +1,19 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcFol open EcAst open EcCoreGoal open EcLowPhlGoal -open EcLowGoal (* -------------------------------------------------------------------- *) -module LowInternal = struct - (* ------------------------------------------------------------------ *) - let t_hoare_skip_r tc = - let hs = tc1_as_hoareS tc in - - if not (List.is_empty hs.hs_s.s_node) then - tc_error !!tc "instruction list is not empty"; - - let post = POE.lower (hs_po hs) in - let concl = map_ss_inv2 f_imp (hs_pr hs) post in - let concl = EcSubst.f_forall_mems_ss_inv hs.hs_m concl in - - FApi.xmutate1 tc `Skip [concl] - - let t_hoare_skip = FApi.t_low0 "hoare-skip" t_hoare_skip_r - - (* ------------------------------------------------------------------ *) - let t_ehoare_skip_r tc = - let hs = tc1_as_ehoareS tc in - - if not (List.is_empty hs.ehs_s.s_node) then - tc_error !!tc "instruction list is not empty"; - - let concl = map_ss_inv2 f_xreal_le (ehs_po hs) (ehs_pr hs) in - let concl = EcSubst.f_forall_mems_ss_inv hs.ehs_m concl in - - FApi.xmutate1 tc `Skip [concl] - - let t_ehoare_skip = FApi.t_low0 "ehoare-skip" t_ehoare_skip_r - - (* ------------------------------------------------------------------ *) - let t_bdhoare_skip_r_low tc = - let bhs = tc1_as_bdhoareS tc in - - if not (List.is_empty bhs.bhs_s.s_node) then - tc_error !!tc ~who:"skip" "instruction list is not empty"; - if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then - tc_error !!tc ~who:"skip" ""; - - let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in - let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in - let goals = - if f_equal (bhs_bd bhs).inv f_r1 - then [concl] - else [f_eq (bhs_bd bhs).inv f_r1; concl] - in - - FApi.xmutate1 tc `Skip goals - - (* ------------------------------------------------------------------ *) - let t_bdhoare_skip_r tc = - let t_trivial = FApi.t_seqs [t_simplify ~delta:`No; t_split; t_fail] in - let bhs = tc1_as_bdhoareS tc in - let f_r1: EcAst.ss_inv = {m=fst bhs.bhs_m; inv=f_r1} in - let t_conseq = EcPhlConseq.t_bdHoareS_conseq_bd FHeq f_r1 in - FApi.t_internal - (FApi.t_seqsub t_conseq - [FApi.t_try t_trivial; t_bdhoare_skip_r_low]) - tc - - let t_bdhoare_skip = FApi.t_low0 "bdhoare-skip" t_bdhoare_skip_r - - (* ------------------------------------------------------------------ *) - let t_equiv_skip_r tc = - let es = tc1_as_equivS tc in - - if not (List.is_empty es.es_sl.s_node) then - tc_error !!tc ~who:"skip" "left instruction list is not empty"; - if not (List.is_empty es.es_sr.s_node) then - tc_error !!tc ~who:"skip" "right instruction list is not empty"; - - let concl = map_ts_inv2 f_imp (es_pr es) (es_po es) in - let concl = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr concl in - FApi.xmutate1 tc `Skip [concl] - - let t_equiv_skip = FApi.t_low0 "equiv-skip" t_equiv_skip_r -end - -(* -------------------------------------------------------------------- *) -let t_skip = - t_hS_or_bhS_or_eS - ~th: LowInternal.t_hoare_skip - ~teh: LowInternal.t_ehoare_skip - ~tbh:LowInternal.t_bdhoare_skip - ~te: LowInternal.t_equiv_skip +(* The [skip] rules live, one module per logic, in [rules//]. This + module only keeps the logic-agnostic dispatcher. *) +let t_skip (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareSkip.t_hoare_skip tc + | FeHoareS _ -> EcEHoareSkip.t_ehoare_skip tc + | FbdHoareS _ -> EcBdHoareSkip.t_bdhoare_skip_full tc + | FequivS _ -> EcEquivSkip.t_equiv_skip tc + | _ -> + tc_error_noXhl + ~kinds:[`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] + !!tc diff --git a/src/phl/rules/bdhoare/ecBdHoareSkip.ml b/src/phl/rules/bdhoare/ecBdHoareSkip.ml new file mode 100644 index 000000000..46ce26fa6 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSkip.ml @@ -0,0 +1,62 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcFol +open EcAst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [skip] rule has no parameters. *) +type EcCoreGoal.rule += RBdHoareSkip + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + statement is empty, the comparison is [=] or [>=]) are part of it, so the + checker re-validates them. *) +let bdhoare_skip_subgoals (bhs : bdHoareS) : form list = + if not (List.is_empty bhs.bhs_s.s_node) then + failwith "bdhoare-skip: the statement is not empty"; + if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then + failwith "bdhoare-skip: the comparison is not = or >="; + let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in + let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in + if f_equal (bhs_bd bhs).inv f_r1 + then [concl] + else [f_eq (bhs_bd bhs).inv f_r1; concl] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_skip (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + if not (List.is_empty bhs.bhs_s.s_node) then + tc_error !!tc ~who:"skip" "instruction list is not empty"; + if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then + tc_error !!tc ~who:"skip" "the bound must be compared with = or >="; + FApi.xrule1 tc RBdHoareSkip (bdhoare_skip_subgoals bhs) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareSkip -> + Some (EcPlRecheck.checker_of "bdhoare-skip" pf_as_bdhoareS + (fun _hyps bhs -> bdhoare_skip_subgoals bhs)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): first turn the goal into [phoare [...] = 1%r] + with the bound-changing consequence, try to close its side condition, + then apply the rule. + + TEMPORARY: the bound-changing consequence still comes from the + not-yet-migrated [EcPhlConseq]. *) +let t_bdhoare_skip_full (tc : tcenv1) = + let t_trivial = FApi.t_seqs [t_simplify ~delta:`No; t_split; t_fail] in + let bhs = tc1_as_bdhoareS tc in + let f_r1 : ss_inv = { m = fst bhs.bhs_m; inv = f_r1 } in + let t_conseq = EcPhlConseq.t_bdHoareS_conseq_bd FHeq f_r1 in + FApi.t_internal + (FApi.t_seqsub t_conseq [FApi.t_try t_trivial; t_bdhoare_skip]) + tc diff --git a/src/phl/rules/bdhoare/ecBdHoareSkip.mli b/src/phl/rules/bdhoare/ecBdHoareSkip.mli new file mode 100644 index 000000000..c583127ce --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSkip.mli @@ -0,0 +1,31 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoare_skip] — empty statement, with [~] the goal's comparison: + + (d = 1%r) forall &m, P => Q + --------------------------------- ~ is [=] or [>=] + phoare [skip : P ==> Q] ~ d + + The premise [d = 1%r] is omitted when [d] is syntactically [1%r]. + Side conditions: the statement is empty, and [~] is [=] or [>=] + (otherwise fails). + + Node: [RBdHoareSkip]. Checker: "bdhoare-skip". *) +val t_bdhoare_skip : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_skip_full] — on [phoare [skip : P ==> Q] ~ d]: + 1. the bound-changing consequence (currently + [EcPhlConseq.t_bdHoareS_conseq_bd]) to [phoare [skip : P ==> Q] = 1%r], + whose side condition (relating [~ d] to [= 1%r]) is closed when + [simplify; split] does, and left open otherwise; + 2. then [t_bdhoare_skip], whose bound is now syntactically [1%r]. + Visible goals: [forall &m, P => Q], preceded by the bound side condition + if not closed. Emits no node of its own. *) +val t_bdhoare_skip_full : backward diff --git a/src/phl/rules/ehoare/ecEHoareSkip.ml b/src/phl/rules/ehoare/ecEHoareSkip.ml new file mode 100644 index 000000000..04e1c381b --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareSkip.ml @@ -0,0 +1,37 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The ehoare [skip] rule has no parameters. *) +type EcCoreGoal.rule += REHoareSkip + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is empty) is part of it, so the checker re-validates it. *) +let ehoare_skip_subgoals (hs : eHoareS) : form list = + if not (List.is_empty hs.ehs_s.s_node) then + failwith "ehoare-skip: the statement is not empty"; + let concl = map_ss_inv2 f_xreal_le (ehs_po hs) (ehs_pr hs) in + [EcSubst.f_forall_mems_ss_inv hs.ehs_m concl] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_skip (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + if not (List.is_empty hs.ehs_s.s_node) then + tc_error !!tc "instruction list is not empty"; + FApi.xrule1 tc REHoareSkip (ehoare_skip_subgoals hs) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareSkip -> + Some (EcPlRecheck.checker_of "ehoare-skip" pf_as_ehoareS + (fun _hyps hs -> ehoare_skip_subgoals hs)) + | _ -> None) diff --git a/src/phl/rules/ehoare/ecEHoareSkip.mli b/src/phl/rules/ehoare/ecEHoareSkip.mli new file mode 100644 index 000000000..7f0aecedc --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareSkip.mli @@ -0,0 +1,17 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_ehoare_skip] — empty statement: + + forall &m, Q <= P + ------------------------ + ehoare [skip : P ==> Q] + + ([<=] on extended reals.) Side condition: the statement is empty + (otherwise fails). + + Node: [REHoareSkip]. Checker: "ehoare-skip". *) +val t_ehoare_skip : backward diff --git a/src/phl/rules/equiv/ecEquivSkip.ml b/src/phl/rules/equiv/ecEquivSkip.ml new file mode 100644 index 000000000..33a3da6ac --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSkip.ml @@ -0,0 +1,41 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The equiv [skip] rule has no parameters. *) +type EcCoreGoal.rule += REquivSkip + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (both + statements are empty) is part of it, so the checker re-validates it. *) +let equiv_skip_subgoals (es : equivS) : form list = + if not (List.is_empty es.es_sl.s_node) then + failwith "equiv-skip: the left statement is not empty"; + if not (List.is_empty es.es_sr.s_node) then + failwith "equiv-skip: the right statement is not empty"; + let concl = map_ts_inv2 f_imp (es_pr es) (es_po es) in + [EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr concl] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equiv_skip (tc : tcenv1) = + let es = tc1_as_equivS tc in + if not (List.is_empty es.es_sl.s_node) then + tc_error !!tc ~who:"skip" "left instruction list is not empty"; + if not (List.is_empty es.es_sr.s_node) then + tc_error !!tc ~who:"skip" "right instruction list is not empty"; + FApi.xrule1 tc REquivSkip (equiv_skip_subgoals es) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivSkip -> + Some (EcPlRecheck.checker_of "equiv-skip" pf_as_equivS + (fun _hyps es -> equiv_skip_subgoals es)) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivSkip.mli b/src/phl/rules/equiv/ecEquivSkip.mli new file mode 100644 index 000000000..56befdfca --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSkip.mli @@ -0,0 +1,16 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equiv_skip] — empty statements: + + forall &1 &2, P => Q + --------------------------- + equiv [skip ~ skip : P ==> Q] + + Side condition: both statements are empty (otherwise fails). + + Node: [REquivSkip]. Checker: "equiv-skip". *) +val t_equiv_skip : backward diff --git a/src/phl/rules/hoare/ecHoareSkip.ml b/src/phl/rules/hoare/ecHoareSkip.ml new file mode 100644 index 000000000..98c6c943c --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSkip.ml @@ -0,0 +1,38 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [skip] rule has no parameters. *) +type EcCoreGoal.rule += RHoareSkip + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + statement is empty) is part of it, so the checker re-validates it. *) +let hoare_skip_subgoals (hs : sHoareS) : form list = + if not (List.is_empty hs.hs_s.s_node) then + failwith "hoare-skip: the statement is not empty"; + let post = POE.lower (hs_po hs) in + let concl = map_ss_inv2 f_imp (hs_pr hs) post in + [EcSubst.f_forall_mems_ss_inv hs.hs_m concl] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_skip (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + if not (List.is_empty hs.hs_s.s_node) then + tc_error !!tc "instruction list is not empty"; + FApi.xrule1 tc RHoareSkip (hoare_skip_subgoals hs) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareSkip -> + Some (EcPlRecheck.checker_of "hoare-skip" pf_as_hoareS + (fun _hyps hs -> hoare_skip_subgoals hs)) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareSkip.mli b/src/phl/rules/hoare/ecHoareSkip.mli new file mode 100644 index 000000000..134b5e191 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSkip.mli @@ -0,0 +1,17 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_skip] — empty statement: + + forall &m, P => Q + --------------------------- + hoare [skip : P ==> Q | Q_e] + + The exceptional postconditions [Q_e] play no role: [skip] raises nothing. + Side condition: the statement is empty (otherwise fails). + + Node: [RHoareSkip]. Checker: "hoare-skip". *) +val t_hoare_skip : backward diff --git a/tests/skip.ec b/tests/skip.ec new file mode 100644 index 000000000..459018fcb --- /dev/null +++ b/tests/skip.ec @@ -0,0 +1,37 @@ +require import AllCore Xreal. + +module M = { + proc f() : int = { + var x; + x <- 1; + return x; + } +}. + +lemma hoare_skip : hoare [M.f : true ==> res = 1]. +proof. proc; wp; skip => //. qed. + +lemma ehoare_skip : ehoare [M.f : (1%xr) ==> (1%xr)]. +proof. proc; wp; skip => //. qed. + +lemma phoare_skip_eq : phoare [M.f : true ==> res = 1] = 1%r. +proof. proc; wp; skip => //. qed. + +(* A bound other than 1: the side condition is left to the user. *) +lemma phoare_skip_ge : phoare [M.f : true ==> res = 1] >= (1%r/2%r). +proof. proc; wp; skip => //; smt(). qed. + +lemma equiv_skip : equiv [M.f ~ M.f : true ==> ={res}]. +proof. proc; wp; skip => //. qed. + +lemma errors : equiv [M.f ~ M.f : true ==> ={res}]. +proof. +proc. +fail skip. +abort. + +lemma errors_le : phoare [M.f : true ==> res = 1] <= 1%r. +proof. +proc. +fail skip. +abort.