From 4ff34a2f42b044f25234b4f11345973051f64852 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Wed, 6 Dec 2023 18:00:18 +0100 Subject: [PATCH] add tactic weakmem --- src/ecHiTacticals.ml | 1 + src/ecLexer.mll | 1 + src/ecParser.mly | 4 ++++ src/ecParsetree.ml | 1 + src/phl/ecPhlCodeTx.ml | 34 +++++++++++++++++++++++++++++ src/phl/ecPhlCodeTx.mli | 3 +++ theories/distributions/Dexcepted.ec | 1 + 7 files changed, 45 insertions(+) diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 1dc8c50e76..bc30d4b78a 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -194,6 +194,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Pkill info -> EcPhlCodeTx.process_kill info | Palias info -> EcPhlCodeTx.process_alias info | Pset info -> EcPhlCodeTx.process_set info + | Pweakmem info -> EcPhlCodeTx.process_weakmem info | Prnd (side, pos, info) -> EcPhlRnd.process_rnd side pos info | Prndsem (side, pos) -> EcPhlRnd.process_rndsem side pos | Pconseq (opt, info) -> EcPhlConseq.process_conseq_opt opt info diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 2a507a5cd8..4604daff22 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -156,6 +156,7 @@ "inline" , INLINE ; (* KW: tactic *) "interleave" , INTERLEAVE ; (* KW: tactic *) "alias" , ALIAS ; (* KW: tactic *) + "weakmem" , WEAKMEM ; (* KW: tactic *) "fission" , FISSION ; (* KW: tactic *) "fusion" , FUSION ; (* KW: tactic *) "unroll" , UNROLL ; (* KW: tactic *) diff --git a/src/ecParser.mly b/src/ecParser.mly index dac815ce79..83c67827ee 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -600,6 +600,7 @@ %token UNDO %token UNROLL %token VAR +%token WEAKMEM %token WHILE %token WHY3 %token WITH @@ -3235,6 +3236,9 @@ phltactic: | ALIAS s=side? o=codepos x=lident EQ e=expr { Pset (s, o, false, x,e) } +| WEAKMEM h=lident p=param_decl + { Pweakmem(h, p) } + | FISSION s=side? o=codepos AT d1=word COMMA d2=word { Pfission (s, o, (1, (d1, d2))) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 51f26759c5..7bd8af3a52 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -736,6 +736,7 @@ type phltactic = | Prnd of oside * semrndpos option * rnd_tac_info_f | Prndsem of oside * codepos1 | Palias of (oside * codepos * osymbol_r) + | Pweakmem of (psymbol * fun_params) | Pset of (oside * codepos * bool * psymbol * pexpr) | Pconseq of (pcqoptions * (conseq_ppterm option tuple3)) | Pconseqauto of crushmode diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index dabe7bbfc9..85fe7d5dfa 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -232,3 +232,37 @@ let process_alias (side, cpos, id) tc = let process_set (side, cpos, fresh, id, e) tc = let e = TTC.tc1_process_Xhl_exp tc side None e in t_set side cpos (fresh, id) e tc + + +(* -------------------------------------------------------------------- *) + +let process_weakmem (id, params) tc = + let open EcLocation in + let hyps = FApi.tc1_hyps tc in + let env = FApi.tc1_env tc in + let _, f = + try LDecl.hyp_by_name (unloc id) hyps + with LDecl.LdeclError _ -> + tc_lookup_error !!tc ~loc:id.pl_loc `Local ([], unloc id) + in + + let process_decl (x, ty) = + let ty = EcTyping.transty EcTyping.tp_tydecl env (EcUnify.UniEnv.create None) ty in + let x = omap unloc (unloc x) in + { ov_name = x; ov_type = ty } in + + let decls = List.map process_decl params in + + let bind me = + try EcMemory.bindall decls me + with EcMemory.DuplicatedMemoryBinding x -> + tc_error ~loc:id.pl_loc !!tc "variable %s already declared" x in + + match f.f_node with + | FbdHoareS hs -> + let me = bind hs.bhs_m in + let hs = { hs with bhs_m = me } in + let concl = f_imp (f_bdHoareS_r hs) (FApi.tc1_goal tc) in + FApi.xmutate1 tc `WeakenMem [concl] + | _ -> + tc_error ~loc:id.pl_loc !!tc "the hypothesis need to be a phoare" diff --git a/src/phl/ecPhlCodeTx.mli b/src/phl/ecPhlCodeTx.mli index e942187c51..446ea705a7 100644 --- a/src/phl/ecPhlCodeTx.mli +++ b/src/phl/ecPhlCodeTx.mli @@ -14,3 +14,6 @@ val process_kill : oside * codepos * int option -> backward val process_alias : oside * codepos * psymbol option -> backward val process_set : oside * codepos * bool * psymbol * pexpr -> backward val process_cfold : oside * codepos * int option -> backward + +(* -------------------------------------------------------------------- *) +val process_weakmem : (psymbol * fun_params) -> backward diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec index e8ee57cf47..fdbab17561 100644 --- a/theories/distributions/Dexcepted.ec +++ b/theories/distributions/Dexcepted.ec @@ -300,6 +300,7 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)) + smt(). + smt(). + move=> ih. alias 2 r0 = r. + weakmem ih (r0:t) => {ih} ih. (** TRANSITIVITY FOR PHOARE!! **) phoare split (mu (dt x) (predI P (predC (X x)))) (mu (dt x) (X x) * mu (dt x \ X x) P)