From 6631ebeec1f793b34136e118012dbc1144d457c7 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@mpi-sp.org>
Date: Wed, 9 Sep 2026 14:56:49 +0200
Subject: [PATCH] Add support of exception in Hoare logic for command rnd

---
 src/phl/ecPhlRnd.ml              |  7 ++-----
 tests/exception/exception_rnd.ec | 36 ++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 5 deletions(-)
 create mode 100644 tests/exception/exception_rnd.ec

diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml
index f8f7bed8a..7943b9a82 100644
--- a/src/phl/ecPhlRnd.ml
+++ b/src/phl/ecPhlRnd.ml
@@ -34,14 +34,11 @@ module Core = struct
     let x_id = EcIdent.create (symbol_of_lv lv) in
     let x = {m; inv=f_local x_id ty_distr} in
     let distr = EcFol.ss_inv_of_expr m distr in
-    if (not (POE.is_empty (hs_po hs).hsi_inv)) then
-      tc_error !!tc "exceptions are not supported";
-    let post = (hs_po hs).hsi_inv.main  in
-    let post = { m = (hs_po hs).hsi_m; inv = post} in
+    let post = POE.lower (hs_po hs) in
     let post = subst_form_lv env lv x post in
     let post = map_ss_inv2 f_imp (map_ss_inv2 f_in_supp x distr) post in
     let post = map_ss_inv1 (f_forall_simpl [(x_id,GTty ty_distr)]) post in
-    let post = POE.lift post in
+    let post = update_hs_ss post (hs_po hs) in
     let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
     FApi.xmutate1 tc `Rnd [concl]
 
diff --git a/tests/exception/exception_rnd.ec b/tests/exception/exception_rnd.ec
new file mode 100644
index 000000000..6e0281cf0
--- /dev/null
+++ b/tests/exception/exception_rnd.ec
@@ -0,0 +1,36 @@
+require import AllCore Distr DBool.
+
+exception exn1.
+
+module M = {
+  var b : bool
+  var i : int
+
+  proc f () : unit = {
+    i <- 1;
+    if (i < 0) raise exn1;
+    b <$ dbool;
+  }
+
+  proc g () : unit = {
+    b <- true;
+    raise exn1;
+    b <$ dunit false;
+  }
+  proc h () : unit = {
+    b <$ dunit true;
+    raise exn1;
+  }
+}.
+
+lemma f_ok : hoare [M.f : true ==> true | exn1 => M.i = 1].
+proof. proc. rnd. wp. skip => />. qed.
+
+lemma g_ok : hoare [M.g : true ==> false | exn1 => M.b].
+proof. proc. rnd. wp. skip. done. qed.
+
+lemma h_ok : hoare [M.h : true ==> false | exn1 => M.b].
+proof. proc. wp. rnd. skip => />. smt(supp_dunit). qed.
+
+lemma g_wrong : hoare [M.g : true ==> false | exn1 => !M.b].
+proof. proc. fail (rnd; wp; skip;done). abort.