From 23aa72a79468f354163150aaa08bfbc3f132d3c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Umut=20Yi=C4=9Fit=20Dural?= Date: Thu, 20 Feb 2025 15:05:43 +0100 Subject: [PATCH] pgcl2heyvl: add annotation support, regenerate examples with annotations instead of direct encodings --- pgcl/examples-heyvl/2drwalk.heyvl | 14 +- pgcl/examples-heyvl/C4B_t303.heyvl | 52 +- pgcl/examples-heyvl/ast-rule.heyvl | 66 +- pgcl/examples-heyvl/ast-rule2.heyvl | 74 +- pgcl/examples-heyvl/bayesian_network.heyvl | 14 +- pgcl/examples-heyvl/brp1.heyvl | 58 +- pgcl/examples-heyvl/brp2.heyvl | 124 +-- pgcl/examples-heyvl/brp3.heyvl | 256 +---- pgcl/examples-heyvl/condand.heyvl | 14 +- pgcl/examples-heyvl/esc_spline_ast.heyvl | 58 +- pgcl/examples-heyvl/fcall.heyvl | 14 +- pgcl/examples-heyvl/geo1.heyvl | 23 +- pgcl/examples-heyvl/hyper.heyvl | 14 +- pgcl/examples-heyvl/linear01.heyvl | 14 +- pgcl/examples-heyvl/nested-rabin.heyvl | 25 +- pgcl/examples-heyvl/prdwalk.heyvl | 14 +- pgcl/examples-heyvl/prspeed.heyvl | 14 +- pgcl/examples-heyvl/rabin1.heyvl | 14 +- pgcl/examples-heyvl/rabin1_wlp.heyvl | 14 +- pgcl/examples-heyvl/rabin2.heyvl | 94 +- pgcl/examples-heyvl/rabin2_wlp.heyvl | 94 +- pgcl/examples-heyvl/rabin3_wlp.heyvl | 274 +---- pgcl/examples-heyvl/rdspeed.heyvl | 14 +- pgcl/examples-heyvl/rdwalk.heyvl | 14 +- pgcl/examples-heyvl/refute-brp5_bmc.heyvl | 141 +-- pgcl/examples-heyvl/refute-geo2_bmc.heyvl | 99 +- pgcl/examples-heyvl/refute-geo3.heyvl | 23 +- pgcl/examples-heyvl/refute-geo3_bmc.heyvl | 377 +------ pgcl/examples-heyvl/refute-rabin3_bmc.heyvl | 87 +- pgcl/examples-heyvl/refute-rabin4_bmc.heyvl | 87 +- pgcl/examples-heyvl/refute-rabin5_bmc.heyvl | 163 +-- .../examples-heyvl/refute-unif_gen1_bmc.heyvl | 31 +- pgcl/examples-heyvl/sprdwalk.heyvl | 14 +- pgcl/examples-heyvl/test_ost.heyvl | 87 +- pgcl/examples-heyvl/test_past.heyvl | 24 +- pgcl/examples-heyvl/unif_gen1.heyvl | 35 +- pgcl/examples-heyvl/unif_gen1_wlp.heyvl | 35 +- pgcl/examples-heyvl/unif_gen2.heyvl | 56 +- pgcl/examples-heyvl/unif_gen2_wlp.heyvl | 56 +- pgcl/examples-heyvl/unif_gen3.heyvl | 56 +- pgcl/examples-heyvl/unif_gen3_wlp.heyvl | 56 +- pgcl/examples-heyvl/unif_gen4.heyvl | 98 +- pgcl/examples-heyvl/unif_gen4_wlp.heyvl | 98 +- pgcl/pgcl2heyvl/pgcl2heyvl/cmd.py | 82 +- pgcl/pgcl2heyvl/pgcl2heyvl/direct_encode.py | 948 ++++++++++++++++++ pgcl/pgcl2heyvl/pgcl2heyvl/encode.py | 380 +++---- pgcl/pgcl2heyvl/pgcl2heyvl/heyvl.py | 58 ++ .../pgcl2heyvl/tests/test_encodings.py | 22 +- pgcl/pgcl2heyvl/pgcl2heyvl/utils.py | 2 - pgcl/pgcl2heyvl/pyproject.toml | 2 - 50 files changed, 1408 insertions(+), 3075 deletions(-) create mode 100644 pgcl/pgcl2heyvl/pgcl2heyvl/direct_encode.py diff --git a/pgcl/examples-heyvl/2drwalk.heyvl b/pgcl/examples-heyvl/2drwalk.heyvl index e460e57a..8a44a845 100644 --- a/pgcl/examples-heyvl/2drwalk.heyvl +++ b/pgcl/examples-heyvl/2drwalk.heyvl @@ -190,7 +190,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x: UInt, y: UInt, d: UInt, n: UInt) +@ert +coproc main(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x: UInt, y: UInt, d: UInt, n: UInt) pre 2 * ((init_n + 1) - init_d) post 0 { @@ -199,11 +200,8 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x y = init_y d = init_d n = init_n - coassert 2 * ((n + 1) - d) - cohavoc d, x, y - covalidate - coassume 2 * ((n + 1) - d) - if d < n { + @k_induction(1, 2 * ((n + 1) - d)) + while d < n { if 0 < x { if 0 < y { prob_choice = flip((1/4)) @@ -409,7 +407,5 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x } } tick 1 - assert 2 * ((n + 1) - d) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/C4B_t303.heyvl b/pgcl/examples-heyvl/C4B_t303.heyvl index 719e0a2e..1cd25034 100644 --- a/pgcl/examples-heyvl/C4B_t303.heyvl +++ b/pgcl/examples-heyvl/C4B_t303.heyvl @@ -26,7 +26,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x: UInt, y: UInt, t: UInt, r: UInt) +@ert +coproc main(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x: UInt, y: UInt, t: UInt, r: UInt) pre (0.5 * (init_x + 2)) + (0.5 * (init_y + 2)) post 0 { @@ -35,11 +36,8 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x y = init_y t = init_t r = init_r - coassert (0.5 * (x + 2)) + (0.5 * (y + 2)) - cohavoc r, t, x, y - covalidate - coassume (0.5 * (x + 2)) + (0.5 * (y + 2)) - if 0 < x { + @k_induction(3, (0.5 * (x + 2)) + (0.5 * (y + 2))) + while 0 < x { prob_choice = flip((1/3)) if prob_choice { r = 1 @@ -56,45 +54,5 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x x = y y = t tick 1 - assert (0.5 * (x + 2)) + (0.5 * (y + 2)) - if 0 < x { - prob_choice = flip((1/3)) - if prob_choice { - r = 1 - } else { - prob_choice = flip((1/2)) - if prob_choice { - r = 2 - } else { - r = 3 - } - } - x = x - r - t = x - x = y - y = t - tick 1 - assert (0.5 * (x + 2)) + (0.5 * (y + 2)) - if 0 < x { - prob_choice = flip((1/3)) - if prob_choice { - r = 1 - } else { - prob_choice = flip((1/2)) - if prob_choice { - r = 2 - } else { - r = 3 - } - } - x = x - r - t = x - x = y - y = t - tick 1 - assert (0.5 * (x + 2)) + (0.5 * (y + 2)) - assume 0 - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/ast-rule.heyvl b/pgcl/examples-heyvl/ast-rule.heyvl index d46f73e6..db183443 100644 --- a/pgcl/examples-heyvl/ast-rule.heyvl +++ b/pgcl/examples-heyvl/ast-rule.heyvl @@ -18,26 +18,12 @@ // } // } -// forall l. (v <= l) ==> (prob(l) <= prob(v)) -proc prob_antitone(x: UInt, v: UReal) -> () -{ - assert ?(forall l: UReal. (v <= l) ==> (0.5 <= 0.5)) -} - -// forall l. (v <= l) ==> (decrease(l) <= decrease(v)) -proc decrease_antitone(x: UInt, v: UReal) -> () -{ - assert ?(forall l: UReal. (v <= l) ==> (2 <= 2)) -} - -// [I] <= \Phi_{[I]}([I]) -proc I_wp_subinvariant(init_x: UInt) -> (x: UInt) - pre [true] - post [true] +proc main(init_x: UInt) -> (x: UInt) { var prob_choice: Bool x = init_x - if !(x == 10) { + @ast(true, (3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x))), v, 0.5, 2) + while !(x == 10) { if (x % 2) == 0 { prob_choice = flip((1/2)) if prob_choice { @@ -48,51 +34,5 @@ proc I_wp_subinvariant(init_x: UInt) -> (x: UInt) } else { x = x + 1 } - } else {} -} - -// !G iff V = 0 -proc termination_condition(x: UInt) -> () -{ - assert ?(!(!(x == 10)) == ((3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x))) == 0)) -} - -// \Phi_{V}(V) <= V -coproc V_wp_superinvariant(init_x: UInt) -> (x: UInt) - pre (3 * [!((init_x % 2) == 0)]) + (([10 <= init_x] * (init_x - 10)) + ([!(10 <= init_x)] * (10 - init_x))) - post (3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x))) -{ - var prob_choice: Bool - x = init_x - if !(x == 10) { - if (x % 2) == 0 { - prob_choice = flip((1/2)) - if prob_choice { - x = x - 2 - } else { - x = x + 2 - } - } else { - x = x + 1 - } - } else {} -} - -// [I] * [G] * (p o V) <= \s. wp[P]([V <= V(s) - d(V(s))])(s) -proc progress_condition(init_x: UInt) -> (x: UInt) - pre [true] * ([!(init_x == 10)] * 0.5) - post [((3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x)))) <= (((3 * [!((init_x % 2) == 0)]) + (([10 <= init_x] * (init_x - 10)) + ([!(10 <= init_x)] * (10 - init_x)))) - 2)] -{ - var prob_choice: Bool - x = init_x - if (x % 2) == 0 { - prob_choice = flip((1/2)) - if prob_choice { - x = x - 2 - } else { - x = x + 2 - } - } else { - x = x + 1 } } diff --git a/pgcl/examples-heyvl/ast-rule2.heyvl b/pgcl/examples-heyvl/ast-rule2.heyvl index 1f093744..9f3e39b5 100644 --- a/pgcl/examples-heyvl/ast-rule2.heyvl +++ b/pgcl/examples-heyvl/ast-rule2.heyvl @@ -22,26 +22,12 @@ // } // } -// forall l. (v <= l) ==> (prob(l) <= prob(v)) -proc prob_antitone(x: UInt, v: UReal) -> () -{ - assert ?(forall l: UReal. (v <= l) ==> (0.5 <= 0.5)) -} - -// forall l. (v <= l) ==> (decrease(l) <= decrease(v)) -proc decrease_antitone(x: UInt, v: UReal) -> () -{ - assert ?(forall l: UReal. (v <= l) ==> (1 <= 1)) -} - -// [I] <= \Phi_{[I]}([I]) -proc I_wp_subinvariant(init_x: UInt) -> (x: UInt) - pre [true] - post [true] +proc main(init_x: UInt) -> (x: UInt) { var prob_choice: Bool x = init_x - if 0 < x { + @ast(true, [0 < x] + [(1 <= x) && (x <= 2)], v, 0.5, 1) + while 0 < x { if x == 1 { prob_choice = flip((1/2)) if prob_choice { @@ -56,59 +42,5 @@ proc I_wp_subinvariant(init_x: UInt) -> (x: UInt) x = x + 1 } } - } else {} -} - -// !G iff V = 0 -proc termination_condition(x: UInt) -> () -{ - assert ?(!(0 < x) == ([0 < x] + [(1 <= x) && (x <= 2)] == 0)) -} - -// \Phi_{V}(V) <= V -coproc V_wp_superinvariant(init_x: UInt) -> (x: UInt) - pre [0 < init_x] + [(1 <= init_x) && (init_x <= 2)] - post [0 < x] + [(1 <= x) && (x <= 2)] -{ - var prob_choice: Bool - x = init_x - if 0 < x { - if x == 1 { - prob_choice = flip((1/2)) - if prob_choice { - x = 0 - } else { - x = x + 1 - } - } else { - if 3 <= x { - x = 0 - } else { - x = x + 1 - } - } - } else {} -} - -// [I] * [G] * (p o V) <= \s. wp[P]([V <= V(s) - d(V(s))])(s) -proc progress_condition(init_x: UInt) -> (x: UInt) - pre [true] * ([0 < init_x] * 0.5) - post [([0 < x] + [(1 <= x) && (x <= 2)]) <= (([0 < init_x] + [(1 <= init_x) && (init_x <= 2)]) - 1)] -{ - var prob_choice: Bool - x = init_x - if x == 1 { - prob_choice = flip((1/2)) - if prob_choice { - x = 0 - } else { - x = x + 1 - } - } else { - if 3 <= x { - x = 0 - } else { - x = x + 1 - } } } diff --git a/pgcl/examples-heyvl/bayesian_network.heyvl b/pgcl/examples-heyvl/bayesian_network.heyvl index 27f12d0d..75751821 100644 --- a/pgcl/examples-heyvl/bayesian_network.heyvl +++ b/pgcl/examples-heyvl/bayesian_network.heyvl @@ -90,7 +90,8 @@ // n := n - 1; // } -coproc k_induction(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_g: UInt, init_n: UInt) -> (i: UInt, d: UInt, s: UInt, l: UInt, g: UInt, n: UInt) +@ert +coproc main(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_g: UInt, init_n: UInt) -> (i: UInt, d: UInt, s: UInt, l: UInt, g: UInt, n: UInt) pre 5 * init_n post 0 { @@ -101,11 +102,8 @@ coproc k_induction(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_ l = init_l g = init_g n = init_n - coassert 5 * n - cohavoc d, g, i, l, n, s - covalidate - coassume 5 * n - if 0 < n { + @k_induction(1, 5 * n) + while 0 < n { prob_choice = flip(0.3) if prob_choice { i = 1 @@ -192,7 +190,5 @@ coproc k_induction(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_ tick 1 } n = n - 1 - assert 5 * n - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/brp1.heyvl b/pgcl/examples-heyvl/brp1.heyvl index 9c647499..c384d58c 100644 --- a/pgcl/examples-heyvl/brp1.heyvl +++ b/pgcl/examples-heyvl/brp1.heyvl @@ -20,7 +20,8 @@ // } // } -coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) +@wp +coproc main(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) pre ([init_toSend <= 4] * (init_totalFailed + 1)) + ([!(init_toSend <= 4)] * ∞) post totalFailed { @@ -30,11 +31,8 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini maxFailed = init_maxFailed failed = init_failed totalFailed = init_totalFailed - coassert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - cohavoc failed, sent, totalFailed - covalidate - coassume ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - if (failed < maxFailed) && (sent < toSend) { + @k_induction(5, ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)) + while (failed < maxFailed) && (sent < toSend) { prob_choice = flip(0.9) if prob_choice { failed = 0 @@ -43,51 +41,5 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini failed = failed + 1 totalFailed = totalFailed + 1 } - assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/brp2.heyvl b/pgcl/examples-heyvl/brp2.heyvl index b260ec8e..6212e9cd 100644 --- a/pgcl/examples-heyvl/brp2.heyvl +++ b/pgcl/examples-heyvl/brp2.heyvl @@ -20,7 +20,8 @@ // } // } -coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) +@wp +coproc main(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) pre ([init_toSend <= 10] * (init_totalFailed + 3)) + ([!(init_toSend <= 10)] * ∞) post totalFailed { @@ -30,11 +31,8 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini maxFailed = init_maxFailed failed = init_failed totalFailed = init_totalFailed - coassert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - cohavoc failed, sent, totalFailed - covalidate - coassume ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { + @k_induction(11, ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞)) + while (failed < maxFailed) && (sent < toSend) { prob_choice = flip(0.9) if prob_choice { failed = 0 @@ -43,117 +41,5 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini failed = failed + 1 totalFailed = totalFailed + 1 } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 10] * (totalFailed + 3)) + ([!(toSend <= 10)] * ∞) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/brp3.heyvl b/pgcl/examples-heyvl/brp3.heyvl index a3342b6a..763af3d9 100644 --- a/pgcl/examples-heyvl/brp3.heyvl +++ b/pgcl/examples-heyvl/brp3.heyvl @@ -20,7 +20,8 @@ // } // } -coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) +@wp +coproc main(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) pre ([init_toSend <= 20] * (init_totalFailed + 3)) + ([!(init_toSend <= 20)] * ∞) post totalFailed { @@ -30,11 +31,8 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini maxFailed = init_maxFailed failed = init_failed totalFailed = init_totalFailed - coassert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - cohavoc failed, sent, totalFailed - covalidate - coassume ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { + @k_induction(23, ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞)) + while (failed < maxFailed) && (sent < toSend) { prob_choice = flip(0.9) if prob_choice { failed = 0 @@ -43,249 +41,5 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini failed = failed + 1 totalFailed = totalFailed + 1 } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert ([toSend <= 20] * (totalFailed + 3)) + ([!(toSend <= 20)] * ∞) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/condand.heyvl b/pgcl/examples-heyvl/condand.heyvl index f168600e..32253bff 100644 --- a/pgcl/examples-heyvl/condand.heyvl +++ b/pgcl/examples-heyvl/condand.heyvl @@ -16,18 +16,16 @@ // tick(1); // } -coproc k_induction(init_n: UInt, init_m: UInt) -> (n: UInt, m: UInt) +@ert +coproc main(init_n: UInt, init_m: UInt) -> (n: UInt, m: UInt) pre init_m + init_n post 0 { var prob_choice: Bool n = init_n m = init_m - coassert m + n - cohavoc m, n - covalidate - coassume m + n - if (0 < n) && (0 < m) { + @k_induction(1, m + n) + while (0 < n) && (0 < m) { prob_choice = flip((1/2)) if prob_choice { n = n - 1 @@ -35,7 +33,5 @@ coproc k_induction(init_n: UInt, init_m: UInt) -> (n: UInt, m: UInt) m = m - 1 } tick 1 - assert m + n - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/esc_spline_ast.heyvl b/pgcl/examples-heyvl/esc_spline_ast.heyvl index bafb9f16..d0f2505b 100644 --- a/pgcl/examples-heyvl/esc_spline_ast.heyvl +++ b/pgcl/examples-heyvl/esc_spline_ast.heyvl @@ -14,69 +14,17 @@ // } // } -// forall l. (v <= l) ==> (prob(l) <= prob(v)) -proc prob_antitone(x: UInt, v: UReal) -> () -{ - assert ?(forall l: UReal. (v <= l) ==> (1 / (l + 1) <= 1 / (v + 1))) -} - -// forall l. (v <= l) ==> (decrease(l) <= decrease(v)) -proc decrease_antitone(x: UInt, v: UReal) -> () -{ - assert ?(forall l: UReal. (v <= l) ==> (1 <= 1)) -} - -// [I] <= \Phi_{[I]}([I]) -proc I_wp_subinvariant(init_x: UInt) -> (x: UInt) - pre [true] - post [true] +proc main(init_x: UInt) -> (x: UInt) { var prob_choice: Bool x = init_x - if 0 < x { + @ast(true, x, v, 1/(v+1), 1) + while 0 < x { prob_choice = flip(1 / (x + 1)) if prob_choice { x = 0 } else { x = x + 1 } - } else {} -} - -// !G iff V = 0 -proc termination_condition(x: UInt) -> () -{ - assert ?(!(0 < x) == (x == 0)) -} - -// \Phi_{V}(V) <= V -coproc V_wp_superinvariant(init_x: UInt) -> (x: UInt) - pre init_x - post x -{ - var prob_choice: Bool - x = init_x - if 0 < x { - prob_choice = flip(1 / (x + 1)) - if prob_choice { - x = 0 - } else { - x = x + 1 - } - } else {} -} - -// [I] * [G] * (p o V) <= \s. wp[P]([V <= V(s) - d(V(s))])(s) -proc progress_condition(init_x: UInt) -> (x: UInt) - pre [true] * ([0 < init_x] * (1 / (init_x + 1))) - post [x <= (init_x - 1)] -{ - var prob_choice: Bool - x = init_x - prob_choice = flip(1 / (x + 1)) - if prob_choice { - x = 0 - } else { - x = x + 1 } } diff --git a/pgcl/examples-heyvl/fcall.heyvl b/pgcl/examples-heyvl/fcall.heyvl index 3758dcaf..0c74410f 100644 --- a/pgcl/examples-heyvl/fcall.heyvl +++ b/pgcl/examples-heyvl/fcall.heyvl @@ -18,7 +18,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) +@ert +coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) pre 2 * (init_n - init_x) post 0 { @@ -26,11 +27,8 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn x = init_x n = init_n r = init_r - coassert 2 * (n - x) - cohavoc r, x - covalidate - coassume 2 * (n - x) - if x < n { + @k_induction(1, 2 * (n - x)) + while x < n { prob_choice = flip((1/2)) if prob_choice { r = 0 @@ -39,7 +37,5 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn } x = x + r tick 1 - assert 2 * (n - x) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/geo1.heyvl b/pgcl/examples-heyvl/geo1.heyvl index f3a0a792..5bf730fc 100644 --- a/pgcl/examples-heyvl/geo1.heyvl +++ b/pgcl/examples-heyvl/geo1.heyvl @@ -15,34 +15,21 @@ // } // } -coproc k_induction(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) +@wp +coproc main(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) pre init_c + 1 post c { var prob_choice: Bool c = init_c f = init_f - coassert c + 1 - cohavoc c, f - covalidate - coassume c + 1 - if f == 1 { + @k_induction(2, c + 1) + while f == 1 { prob_choice = flip(0.5) if prob_choice { f = 0 } else { c = c + 1 } - assert c + 1 - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - assert c + 1 - assume 0 - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/hyper.heyvl b/pgcl/examples-heyvl/hyper.heyvl index 692269f6..d92edc66 100644 --- a/pgcl/examples-heyvl/hyper.heyvl +++ b/pgcl/examples-heyvl/hyper.heyvl @@ -22,7 +22,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) +@ert +coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) pre 5 * (init_n - init_x) post 0 { @@ -30,11 +31,8 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn x = init_x n = init_n r = init_r - coassert 5 * (n - x) - cohavoc r, x - covalidate - coassume 5 * (n - x) - if (x + 2) <= n { + @k_induction(1, 5 * (n - x)) + while (x + 2) <= n { prob_choice = flip((117/145)) if prob_choice { r = 0 @@ -48,7 +46,5 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn } x = x + r tick 1 - assert 5 * (n - x) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/linear01.heyvl b/pgcl/examples-heyvl/linear01.heyvl index 8fb2a5a7..bf2e73bf 100644 --- a/pgcl/examples-heyvl/linear01.heyvl +++ b/pgcl/examples-heyvl/linear01.heyvl @@ -15,17 +15,15 @@ // tick(1); // } -coproc k_induction(init_x: UInt) -> (x: UInt) +@ert +coproc main(init_x: UInt) -> (x: UInt) pre 0.6 * init_x post 0 { var prob_choice: Bool x = init_x - coassert 0.6 * x - cohavoc x - covalidate - coassume 0.6 * x - if 2 <= x { + @k_induction(1, 0.6 * x) + while 2 <= x { prob_choice = flip((1/3)) if prob_choice { x = x - 1 @@ -33,7 +31,5 @@ coproc k_induction(init_x: UInt) -> (x: UInt) x = x - 2 } tick 1 - assert 0.6 * x - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/nested-rabin.heyvl b/pgcl/examples-heyvl/nested-rabin.heyvl index 32802e8d..f79f6bca 100644 --- a/pgcl/examples-heyvl/nested-rabin.heyvl +++ b/pgcl/examples-heyvl/nested-rabin.heyvl @@ -25,7 +25,8 @@ // } // } -proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt) -> (i: UInt, n: UInt, d: UInt) +@wlp +proc main(init_i: UInt, init_n: UInt, init_d: UInt) -> (i: UInt, n: UInt, d: UInt) pre [(init_n <= 5) && (init_i <= 5)] * ([1 == init_i] + ([1 < init_i] * (2/3))) post [(n <= 5) && (i <= 5)] * [i == 1] { @@ -33,17 +34,11 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt) -> (i: UInt, n: UInt, i = init_i n = init_n d = init_d - assert [(n <= 5) && (i <= 5)] * ([1 == i] + ([1 < i] * (2/3))) - havoc d, i, n - validate - assume [(n <= 5) && (i <= 5)] * ([1 == i] + ([1 < i] * (2/3))) - if 1 < i { + @k_induction(1, [(n <= 5) && (i <= 5)] * ([1 == i] + ([1 < i] * (2/3)))) + while 1 < i { n = i - assert ([(n <= 5) && (i <= 5)] * [(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + ((([i == n] * n) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))))) - havoc d, i, n - validate - assume ([(n <= 5) && (i <= 5)] * [(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + ((([i == n] * n) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))))) - if 0 < n { + @k_induction(1, ([(n <= 5) && (i <= 5)] * [(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + ((([i == n] * n) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + while 0 < n { prob_choice = flip(0.5) if prob_choice { d = 0 @@ -52,10 +47,6 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt) -> (i: UInt, n: UInt, } i = i - d n = n - 1 - assert ([(n <= 5) && (i <= 5)] * [(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + ((([i == n] * n) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))))) - assume 0 - } else {} - assert [(n <= 5) && (i <= 5)] * ([1 == i] + ([1 < i] * (2/3))) - assume 0 - } else {} + } + } } diff --git a/pgcl/examples-heyvl/prdwalk.heyvl b/pgcl/examples-heyvl/prdwalk.heyvl index 675dd9a7..3f24179b 100644 --- a/pgcl/examples-heyvl/prdwalk.heyvl +++ b/pgcl/examples-heyvl/prdwalk.heyvl @@ -47,7 +47,8 @@ // tick(2); // } -coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) +@ert +coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) pre 1.14286 * ((init_n + 4) - init_x) post 0 { @@ -55,11 +56,8 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn x = init_x n = init_n r = init_r - coassert 1.14286 * ((n + 4) - x) - cohavoc r, x - covalidate - coassume 1.14286 * ((n + 4) - x) - if x < n { + @k_induction(1, 1.14286 * ((n + 4) - x)) + while x < n { prob_choice = flip((1/2)) if prob_choice { prob_choice = flip((1/3)) @@ -104,7 +102,5 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn x = x + r } tick 2 - assert 1.14286 * ((n + 4) - x) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/prspeed.heyvl b/pgcl/examples-heyvl/prspeed.heyvl index 75200448..f8bef663 100644 --- a/pgcl/examples-heyvl/prspeed.heyvl +++ b/pgcl/examples-heyvl/prspeed.heyvl @@ -34,7 +34,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt) -> (x: UInt, y: UInt, m: UInt, n: UInt) +@ert +coproc main(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt) -> (x: UInt, y: UInt, m: UInt, n: UInt) pre (2 * (init_m - init_y)) + (0.6666667 * (init_n - init_x)) post 0 { @@ -43,11 +44,8 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt) -> (x y = init_y m = init_m n = init_n - coassert (2 * (m - y)) + (0.6666667 * (n - x)) - cohavoc x, y - covalidate - coassume (2 * (m - y)) + (0.6666667 * (n - x)) - if (x + 3) <= n { + @k_induction(1, (2 * (m - y)) + (0.6666667 * (n - x))) + while (x + 3) <= n { if y < m { prob_choice = flip((1/2)) if prob_choice { @@ -74,7 +72,5 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt) -> (x } } tick 1 - assert (2 * (m - y)) + (0.6666667 * (n - x)) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/rabin1.heyvl b/pgcl/examples-heyvl/rabin1.heyvl index 54ae02e5..890b0bd7 100644 --- a/pgcl/examples-heyvl/rabin1.heyvl +++ b/pgcl/examples-heyvl/rabin1.heyvl @@ -28,7 +28,8 @@ // } // } -coproc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +@wp +coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre ([((1 < init_i) && (init_i < 2)) && (init_phase == 0)] * (2/3)) + ([!(((1 < init_i) && (init_i < 2)) && (init_phase == 0))] * 1) post [i == 1] { @@ -37,11 +38,8 @@ coproc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) - n = init_n d = init_d phase = init_phase - coassert ([((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 2)) && (phase == 0))] * 1) - cohavoc d, i, n, phase - covalidate - coassume ([((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 2)) && (phase == 0))] * 1) - if (1 < i) || (phase == 1) { + @k_induction(1, ([((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 2)) && (phase == 0))] * 1)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -59,7 +57,5 @@ coproc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) - phase = 0 } } - assert ([((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 2)) && (phase == 0))] * 1) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/rabin1_wlp.heyvl b/pgcl/examples-heyvl/rabin1_wlp.heyvl index 696f60d6..0929dbff 100644 --- a/pgcl/examples-heyvl/rabin1_wlp.heyvl +++ b/pgcl/examples-heyvl/rabin1_wlp.heyvl @@ -28,7 +28,8 @@ // } // } -proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +@wlp +proc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre [((1 < init_i) && (init_i < 2)) && (init_phase == 0)] * (2/3) post [i == 1] { @@ -37,11 +38,8 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> n = init_n d = init_d phase = init_phase - assert [((1 < i) && (i < 2)) && (phase == 0)] * (2/3) - havoc d, i, n, phase - validate - assume [((1 < i) && (i < 2)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { + @k_induction(1, [((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -59,7 +57,5 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> phase = 0 } } - assert [((1 < i) && (i < 2)) && (phase == 0)] * (2/3) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/rabin2.heyvl b/pgcl/examples-heyvl/rabin2.heyvl index dff65d84..d18f53ae 100644 --- a/pgcl/examples-heyvl/rabin2.heyvl +++ b/pgcl/examples-heyvl/rabin2.heyvl @@ -28,7 +28,8 @@ // } // } -coproc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +@wp +coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre ([((1 < init_i) && (init_i < 3)) && (init_phase == 0)] * (2/3)) + ([!(((1 < init_i) && (init_i < 3)) && (init_phase == 0))] * 1) post [i == 1] { @@ -37,11 +38,8 @@ coproc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) - n = init_n d = init_d phase = init_phase - coassert ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - cohavoc d, i, n, phase - covalidate - coassume ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - if (1 < i) || (phase == 1) { + @k_induction(5, ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -59,87 +57,5 @@ coproc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) - phase = 0 } } - assert ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert ([((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 3)) && (phase == 0))] * 1) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/rabin2_wlp.heyvl b/pgcl/examples-heyvl/rabin2_wlp.heyvl index c6e10cb1..bc098dfb 100644 --- a/pgcl/examples-heyvl/rabin2_wlp.heyvl +++ b/pgcl/examples-heyvl/rabin2_wlp.heyvl @@ -28,7 +28,8 @@ // } // } -proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +@wlp +proc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre [((1 < init_i) && (init_i < 3)) && (init_phase == 0)] * (2/3) post [i == 1] { @@ -37,11 +38,8 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> n = init_n d = init_d phase = init_phase - assert [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - havoc d, i, n, phase - validate - assume [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { + @k_induction(5, [((1 < i) && (i < 3)) && (phase == 0)] * (2/3)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -59,87 +57,5 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> phase = 0 } } - coassert [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert [((1 < i) && (i < 3)) && (phase == 0)] * (2/3) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/rabin3_wlp.heyvl b/pgcl/examples-heyvl/rabin3_wlp.heyvl index 31595516..e3f6664b 100644 --- a/pgcl/examples-heyvl/rabin3_wlp.heyvl +++ b/pgcl/examples-heyvl/rabin3_wlp.heyvl @@ -28,7 +28,8 @@ // } // } -proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +@wlp +proc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre [((1 < init_i) && (init_i < 12)) && (init_phase == 0)] * (2/3) post [i == 1] { @@ -37,11 +38,8 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> n = init_n d = init_d phase = init_phase - assert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - havoc d, i, n, phase - validate - assume [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { + @k_induction(14, [((1 < i) && (i < 12)) && (phase == 0)] * (2/3)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -59,267 +57,5 @@ proc k_induction(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> phase = 0 } } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - coassert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert [((1 < i) && (i < 12)) && (phase == 0)] * (2/3) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/rdspeed.heyvl b/pgcl/examples-heyvl/rdspeed.heyvl index 7fae2a1a..93656905 100644 --- a/pgcl/examples-heyvl/rdspeed.heyvl +++ b/pgcl/examples-heyvl/rdspeed.heyvl @@ -37,7 +37,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, y: UInt, m: UInt, n: UInt, r: UInt) +@ert +coproc main(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, y: UInt, m: UInt, n: UInt, r: UInt) pre (2 * (init_m - init_y)) + (0.666667 * (init_n - init_x)) post 0 { @@ -47,11 +48,8 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt, init_ m = init_m n = init_n r = init_r - coassert (2 * (m - y)) + (0.666667 * (n - x)) - cohavoc r, x, y - covalidate - coassume (2 * (m - y)) + (0.666667 * (n - x)) - if (x + 3) <= n { + @k_induction(1, (2 * (m - y)) + (0.666667 * (n - x))) + while (x + 3) <= n { if y < m { prob_choice = flip((1/2)) if prob_choice { @@ -80,7 +78,5 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt, init_ x = x + r } tick 1 - assert (2 * (m - y)) + (0.666667 * (n - x)) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/rdwalk.heyvl b/pgcl/examples-heyvl/rdwalk.heyvl index 64d41963..1eadcfaf 100644 --- a/pgcl/examples-heyvl/rdwalk.heyvl +++ b/pgcl/examples-heyvl/rdwalk.heyvl @@ -16,18 +16,16 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_n: UInt) -> (x: UInt, n: UInt) +@ert +coproc main(init_x: UInt, init_n: UInt) -> (x: UInt, n: UInt) pre 2 * ((init_n + 1) - init_x) post 0 { var prob_choice: Bool x = init_x n = init_n - coassert 2 * ((n + 1) - x) - cohavoc x - covalidate - coassume 2 * ((n + 1) - x) - if x < n { + @k_induction(1, 2 * ((n + 1) - x)) + while x < n { prob_choice = flip((1/2)) if prob_choice { x = x + 2 @@ -35,7 +33,5 @@ coproc k_induction(init_x: UInt, init_n: UInt) -> (x: UInt, n: UInt) x = x - 1 } tick 1 - assert 2 * ((n + 1) - x) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-brp5_bmc.heyvl b/pgcl/examples-heyvl/refute-brp5_bmc.heyvl index c37af756..2aa25799 100644 --- a/pgcl/examples-heyvl/refute-brp5_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-brp5_bmc.heyvl @@ -1,4 +1,4 @@ -// Auto-generated by pgcl2heyvl from fail-brp5_bmc.pgcl +// Auto-generated by pgcl2heyvl from refute-brp5_bmc.pgcl // // HeyVL file to show that // totalFailed + 1 >= wp[C](totalFailed) @@ -21,7 +21,7 @@ // } // } -coproc bounded_model_checking(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) +coproc main(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt) pre init_totalFailed + 1 post totalFailed { @@ -31,7 +31,8 @@ coproc bounded_model_checking(init_toSend: UInt, init_sent: UInt, init_maxFailed maxFailed = init_maxFailed failed = init_failed totalFailed = init_totalFailed - if (failed < maxFailed) && (sent < toSend) { + @unroll(14, totalFailed + 1) + while (failed < maxFailed) && (sent < toSend) { prob_choice = flip(0.9) if prob_choice { failed = 0 @@ -40,137 +41,5 @@ coproc bounded_model_checking(init_toSend: UInt, init_sent: UInt, init_maxFailed failed = failed + 1 totalFailed = totalFailed + 1 } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - if (failed < maxFailed) && (sent < toSend) { - prob_choice = flip(0.9) - if prob_choice { - failed = 0 - sent = sent + 1 - } else { - failed = failed + 1 - totalFailed = totalFailed + 1 - } - assert 0 - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-geo2_bmc.heyvl b/pgcl/examples-heyvl/refute-geo2_bmc.heyvl index 52e2a88a..df6de9c5 100644 --- a/pgcl/examples-heyvl/refute-geo2_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-geo2_bmc.heyvl @@ -1,4 +1,4 @@ -// Auto-generated by pgcl2heyvl from fail-geo2_bmc.pgcl +// Auto-generated by pgcl2heyvl from refute-geo2_bmc.pgcl // // HeyVL file to show that // c + 0.99 >= wp[C](c) @@ -16,109 +16,20 @@ // } // } -coproc bounded_model_checking(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) +coproc main(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) pre init_c + 0.99 post c { var prob_choice: Bool c = init_c f = init_f - if f == 1 { + @unroll(12, c + 0.99) + while f == 1 { prob_choice = flip(0.5) if prob_choice { f = 0 } else { c = c + 1 } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - assert 0 - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-geo3.heyvl b/pgcl/examples-heyvl/refute-geo3.heyvl index 3510d637..119cfe61 100644 --- a/pgcl/examples-heyvl/refute-geo3.heyvl +++ b/pgcl/examples-heyvl/refute-geo3.heyvl @@ -15,34 +15,21 @@ // } // } -coproc k_induction(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) +@wp +coproc main(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) pre init_c + 0.999999999999 post c { var prob_choice: Bool c = init_c f = init_f - coassert c + 0.999999999999 - cohavoc c, f - covalidate - coassume c + 0.999999999999 - if f == 1 { + @k_induction(2, c + 0.999999999999) + while f == 1 { prob_choice = flip(0.5) if prob_choice { f = 0 } else { c = c + 1 } - assert c + 0.999999999999 - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - assert c + 0.999999999999 - assume 0 - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-geo3_bmc.heyvl b/pgcl/examples-heyvl/refute-geo3_bmc.heyvl index ac68de7e..459230e2 100644 --- a/pgcl/examples-heyvl/refute-geo3_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-geo3_bmc.heyvl @@ -16,389 +16,20 @@ // } // } -coproc bounded_model_checking(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) +coproc main(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt) pre init_c + 0.999999999999 post c { var prob_choice: Bool c = init_c f = init_f - if f == 1 { + @unroll(47, c + 0.999999999999) + while f == 1 { prob_choice = flip(0.5) if prob_choice { f = 0 } else { c = c + 1 } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - if f == 1 { - prob_choice = flip(0.5) - if prob_choice { - f = 0 - } else { - c = c + 1 - } - assert 0 - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-rabin3_bmc.heyvl b/pgcl/examples-heyvl/refute-rabin3_bmc.heyvl index 22da3d00..d925e9f7 100644 --- a/pgcl/examples-heyvl/refute-rabin3_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-rabin3_bmc.heyvl @@ -1,4 +1,4 @@ -// Auto-generated by pgcl2heyvl from fail-rabin3_bmc.pgcl +// Auto-generated by pgcl2heyvl from refute-rabin3_bmc.pgcl // // HeyVL file to show that // ([((1 < i) && (i < 4)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 4)) && (phase == 0))] * 1) >= wp[C]([i == 1]) @@ -29,7 +29,7 @@ // } // } -coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre ([((1 < init_i) && (init_i < 4)) && (init_phase == 0)] * (2/3)) + ([!(((1 < init_i) && (init_i < 4)) && (init_phase == 0))] * 1) post [i == 1] { @@ -38,7 +38,8 @@ coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_pha n = init_n d = init_d phase = init_phase - if (1 < i) || (phase == 1) { + @unroll(5, ([((1 < i) && (i < 4)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 4)) && (phase == 0))] * 1)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -56,83 +57,5 @@ coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_pha phase = 0 } } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert 0 - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-rabin4_bmc.heyvl b/pgcl/examples-heyvl/refute-rabin4_bmc.heyvl index 27bd907c..7ce03065 100644 --- a/pgcl/examples-heyvl/refute-rabin4_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-rabin4_bmc.heyvl @@ -1,4 +1,4 @@ -// Auto-generated by pgcl2heyvl from fail-rabin4_bmc.pgcl +// Auto-generated by pgcl2heyvl from refute-rabin4_bmc.pgcl // // HeyVL file to show that // ([(1 < i) && (phase == 0)] * (1/3)) + ([!((1 < i) && (phase == 0))] * 1) >= wp[C]([i == 1]) @@ -29,7 +29,7 @@ // } // } -coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre ([(1 < init_i) && (init_phase == 0)] * (1/3)) + ([!((1 < init_i) && (init_phase == 0))] * 1) post [i == 1] { @@ -38,7 +38,8 @@ coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_pha n = init_n d = init_d phase = init_phase - if (1 < i) || (phase == 1) { + @unroll(5, ([(1 < i) && (phase == 0)] * (1/3)) + ([!((1 < i) && (phase == 0))] * 1)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -56,83 +57,5 @@ coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_pha phase = 0 } } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert 0 - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-rabin5_bmc.heyvl b/pgcl/examples-heyvl/refute-rabin5_bmc.heyvl index fb9458f0..6ce9dbed 100644 --- a/pgcl/examples-heyvl/refute-rabin5_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-rabin5_bmc.heyvl @@ -1,4 +1,4 @@ -// Auto-generated by pgcl2heyvl from fail-rabin5_bmc.pgcl +// Auto-generated by pgcl2heyvl from refute-rabin5_bmc.pgcl // // HeyVL file to show that // ([(1 < i) && (phase == 0)] * 0.6) + ([!((1 < i) && (phase == 0))] * 1) >= wp[C]([i == 1]) @@ -29,7 +29,7 @@ // } // } -coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) +coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UInt, n: UInt, d: UInt, phase: UInt) pre ([(1 < init_i) && (init_phase == 0)] * 0.6) + ([!((1 < init_i) && (init_phase == 0))] * 1) post [i == 1] { @@ -38,7 +38,8 @@ coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_pha n = init_n d = init_d phase = init_phase - if (1 < i) || (phase == 1) { + @unroll(9, ([(1 < i) && (phase == 0)] * 0.6) + ([!((1 < i) && (phase == 0))] * 1)) + while (1 < i) || (phase == 1) { if phase == 0 { n = i phase = 1 @@ -56,159 +57,5 @@ coproc bounded_model_checking(init_i: UInt, init_n: UInt, init_d: UInt, init_pha phase = 0 } } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - if (1 < i) || (phase == 1) { - if phase == 0 { - n = i - phase = 1 - } else { - if 0 < n { - prob_choice = flip(0.5) - if prob_choice { - d = 0 - } else { - d = 1 - } - i = i - d - n = n - 1 - } else { - phase = 0 - } - } - assert 0 - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/refute-unif_gen1_bmc.heyvl b/pgcl/examples-heyvl/refute-unif_gen1_bmc.heyvl index 462c280f..6053c716 100644 --- a/pgcl/examples-heyvl/refute-unif_gen1_bmc.heyvl +++ b/pgcl/examples-heyvl/refute-unif_gen1_bmc.heyvl @@ -1,4 +1,4 @@ -// Auto-generated by pgcl2heyvl from unif_gen1_bmc.pgcl +// Auto-generated by pgcl2heyvl from refute-unif_gen1_bmc.pgcl // // HeyVL file to show that // ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * 0.49) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) >= wp[C]([c == i]) @@ -37,7 +37,7 @@ // } // } -coproc bounded_model_checking(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +coproc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre ([(((((((init_elow + 1) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * 0.49) + ([!((((((((init_elow + 1) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh))] * 1) post [c == i] { @@ -49,7 +49,8 @@ coproc bounded_model_checking(init_elow: UInt, init_ehigh: UInt, init_n: UInt, i c = init_c running = init_running i = init_i - if running == 0 { + @unroll(2, ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * 0.49) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -68,27 +69,5 @@ coproc bounded_model_checking(init_elow: UInt, init_ehigh: UInt, init_n: UInt, i if !(running == 0) { c = elow + c } else {} - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert 0 - assume 0 - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/sprdwalk.heyvl b/pgcl/examples-heyvl/sprdwalk.heyvl index a9a3d37c..5ad4429b 100644 --- a/pgcl/examples-heyvl/sprdwalk.heyvl +++ b/pgcl/examples-heyvl/sprdwalk.heyvl @@ -18,7 +18,8 @@ // tick(1); // } -coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) +@ert +coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: UInt) pre 2 * (init_n - init_x) post 0 { @@ -26,11 +27,8 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn x = init_x n = init_n r = init_r - coassert 2 * (n - x) - cohavoc r, x - covalidate - coassume 2 * (n - x) - if x < n { + @k_induction(1, 2 * (n - x)) + while x < n { prob_choice = flip((1/2)) if prob_choice { r = 0 @@ -39,7 +37,5 @@ coproc k_induction(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UIn } x = x + r tick 1 - assert 2 * (n - x) - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/test_ost.heyvl b/pgcl/examples-heyvl/test_ost.heyvl index c6e02919..3df9d302 100644 --- a/pgcl/examples-heyvl/test_ost.heyvl +++ b/pgcl/examples-heyvl/test_ost.heyvl @@ -20,22 +20,14 @@ // k := k + 1; // } -// past_I < ∞ -proc lt_infinity(a: Bool, b: UInt, k: UInt) -> () -{ - assert ?(2 * [a] < ?(true)) -} - -// \Phi_{0}(past_I) <= past_I, so ert[P](0) <= past_I -coproc past(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: UInt) - pre 2 * [init_a] - post 0 +proc main(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: UInt) { var prob_choice: Bool a = init_a b = init_b k = init_k - if a { + @ost(b + [a], 2 * [a], 1, b) + while a { prob_choice = flip(0.5) if prob_choice { a = false @@ -43,78 +35,5 @@ coproc past(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: U b = b + 1 } k = k + 1 - tick 1 - assert 2 * [a] - assume 0 - } else {} -} - -// wp[P](|I(s)-I|)(s) <= c -coproc conditional_difference_bounded(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: UInt) - pre 1 - post ite((init_b + [init_a]) <= (b + [a]),(b + [a]) - (init_b + [init_a]),(init_b + [init_a]) - (b + [a])) -{ - var prob_choice: Bool - a = init_a - b = init_b - k = init_k - prob_choice = flip(0.5) - if prob_choice { - a = false - } else { - b = b + 1 } - k = k + 1 -} - -// I <= \Phi_{post}(I) -proc lower_bound(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: UInt) - pre init_b + [init_a] - post b -{ - var prob_choice: Bool - a = init_a - b = init_b - k = init_k - if a { - prob_choice = flip(0.5) - if prob_choice { - a = false - } else { - b = b + 1 - } - k = k + 1 - assert b + [a] - assume 0 - } else {} -} - -// !guard ==> (I = f) -proc harmonize_I_f(a: Bool, b: UInt, k: UInt) -> () -{ - assert ?(!a ==> (b + [a] == b)) -} - -// \Phi_f(I) < ∞ -coproc loopiter_lt_infty(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: UInt) - pre 0 - post b -{ - validate - assume \infty - var prob_choice: Bool - a = init_a - b = init_b - k = init_k - if a { - prob_choice = flip(0.5) - if prob_choice { - a = false - } else { - b = b + 1 - } - k = k + 1 - assert b + [a] - assume 0 - } else {} } diff --git a/pgcl/examples-heyvl/test_past.heyvl b/pgcl/examples-heyvl/test_past.heyvl index 5a5c72cf..79bf4667 100644 --- a/pgcl/examples-heyvl/test_past.heyvl +++ b/pgcl/examples-heyvl/test_past.heyvl @@ -12,31 +12,15 @@ // } [0.5] { } // } -// [!G] * I <= K -proc condition_1(x: UInt) -> () -{ - assert ?(([!(0 < x)] * (x + 1)) <= 1) -} - -// [G] * K <= [G] * I + [!G] -proc condition_2(x: UInt) -> () -{ - assert ?(([0 < x] * 1) <= (([0 < x] * (x + 1)) + [!(0 < x)])) -} - -// \Phi_0(I) <= [G] * (I - eps) -coproc condition_3(init_x: UInt) -> (x: UInt) - pre [0 < init_x] * ((init_x + 1) - 0.5) - post 0 +proc main(init_x: UInt) -> (x: UInt) { var prob_choice: Bool x = init_x - if 0 < x { + @past(x + 1, 0.5, 1) + while 0 < x { prob_choice = flip(0.5) if prob_choice { x = x - 1 } else {} - assert x + 1 - assume 0 - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen1.heyvl b/pgcl/examples-heyvl/unif_gen1.heyvl index 8fb295ea..48fd54e5 100644 --- a/pgcl/examples-heyvl/unif_gen1.heyvl +++ b/pgcl/examples-heyvl/unif_gen1.heyvl @@ -36,7 +36,8 @@ // } // } -coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wp +coproc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre ([(((((((init_elow + 1) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/2)) + ([!((((((((init_elow + 1) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh))] * 1) post [c == i] { @@ -48,11 +49,8 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt c = init_c running = init_running i = init_i - coassert ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2)) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - cohavoc c, running, v - covalidate - coassume ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2)) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { + @k_induction(2, ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2)) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,28 +69,5 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt if !(running == 0) { c = elow + c } else {} - assert ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2)) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2)) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - assume 0 - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen1_wlp.heyvl b/pgcl/examples-heyvl/unif_gen1_wlp.heyvl index 6644d97c..4e57c6ed 100644 --- a/pgcl/examples-heyvl/unif_gen1_wlp.heyvl +++ b/pgcl/examples-heyvl/unif_gen1_wlp.heyvl @@ -36,7 +36,8 @@ // } // } -proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wlp +proc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre [(((((((init_elow + 1) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/2) post [c == i] { @@ -48,11 +49,8 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, c = init_c running = init_running i = init_i - assert [(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2) - havoc c, running, v - validate - assume [(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2) - if running == 0 { + @k_induction(2, [(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,28 +69,5 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, if !(running == 0) { c = elow + c } else {} - coassert [(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert [(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/2) - assume 0 - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen2.heyvl b/pgcl/examples-heyvl/unif_gen2.heyvl index 57d1c8e5..84c3a560 100644 --- a/pgcl/examples-heyvl/unif_gen2.heyvl +++ b/pgcl/examples-heyvl/unif_gen2.heyvl @@ -36,7 +36,8 @@ // } // } -coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wp +coproc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre ([(((((((init_elow + 2) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/3)) + ([!((((((((init_elow + 2) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh))] * 1) post [c == i] { @@ -48,11 +49,8 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt c = init_c running = init_running i = init_i - coassert ([(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + ([!((((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - cohavoc c, running, v - covalidate - coassume ([(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + ([!((((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { + @k_induction(3, ([(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + ([!((((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,49 +69,5 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt if !(running == 0) { c = elow + c } else {} - assert ([(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + ([!((((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + ([!((((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + ([!((((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - assume 0 - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen2_wlp.heyvl b/pgcl/examples-heyvl/unif_gen2_wlp.heyvl index 1348a8aa..af285790 100644 --- a/pgcl/examples-heyvl/unif_gen2_wlp.heyvl +++ b/pgcl/examples-heyvl/unif_gen2_wlp.heyvl @@ -36,7 +36,8 @@ // } // } -proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wlp +proc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre [(((((((init_elow + 2) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/3) post [c == i] { @@ -48,11 +49,8 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, c = init_c running = init_running i = init_i - assert [(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3) - havoc c, running, v - validate - assume [(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3) - if running == 0 { + @k_induction(3, [(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,49 +69,5 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, if !(running == 0) { c = elow + c } else {} - coassert [(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - coassert [(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert [(((((((elow + 2) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/3) - assume 0 - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen3.heyvl b/pgcl/examples-heyvl/unif_gen3.heyvl index b7e80776..24116a31 100644 --- a/pgcl/examples-heyvl/unif_gen3.heyvl +++ b/pgcl/examples-heyvl/unif_gen3.heyvl @@ -36,7 +36,8 @@ // } // } -coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wp +coproc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre ([(((((((init_elow + 3) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/4)) + ([!((((((((init_elow + 3) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh))] * 1) post [c == i] { @@ -48,11 +49,8 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt c = init_c running = init_running i = init_i - coassert ([(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + ([!((((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - cohavoc c, running, v - covalidate - coassume ([(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + ([!((((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { + @k_induction(3, ([(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + ([!((((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,49 +69,5 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt if !(running == 0) { c = elow + c } else {} - assert ([(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + ([!((((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + ([!((((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + ([!((((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - assume 0 - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen3_wlp.heyvl b/pgcl/examples-heyvl/unif_gen3_wlp.heyvl index 4ba4575e..177bbcc7 100644 --- a/pgcl/examples-heyvl/unif_gen3_wlp.heyvl +++ b/pgcl/examples-heyvl/unif_gen3_wlp.heyvl @@ -36,7 +36,8 @@ // } // } -proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wlp +proc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre [(((((((init_elow + 3) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/4) post [c == i] { @@ -48,11 +49,8 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, c = init_c running = init_running i = init_i - assert [(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4) - havoc c, running, v - validate - assume [(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4) - if running == 0 { + @k_induction(3, [(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,49 +69,5 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, if !(running == 0) { c = elow + c } else {} - coassert [(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - coassert [(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert [(((((((elow + 3) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/4) - assume 0 - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen4.heyvl b/pgcl/examples-heyvl/unif_gen4.heyvl index 69ec45d5..97ab32bd 100644 --- a/pgcl/examples-heyvl/unif_gen4.heyvl +++ b/pgcl/examples-heyvl/unif_gen4.heyvl @@ -36,7 +36,8 @@ // } // } -coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wp +coproc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre ([(((((((init_elow + 4) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/5)) + ([!((((((((init_elow + 4) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh))] * 1) post [c == i] { @@ -48,11 +49,8 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt c = init_c running = init_running i = init_i - coassert ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - cohavoc c, running, v - covalidate - coassume ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { + @k_induction(5, ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,91 +69,5 @@ coproc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt if !(running == 0) { c = elow + c } else {} - assert ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert ([(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + ([!((((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/examples-heyvl/unif_gen4_wlp.heyvl b/pgcl/examples-heyvl/unif_gen4_wlp.heyvl index 6756aeb8..09c956a6 100644 --- a/pgcl/examples-heyvl/unif_gen4_wlp.heyvl +++ b/pgcl/examples-heyvl/unif_gen4_wlp.heyvl @@ -36,7 +36,8 @@ // } // } -proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) +@wlp +proc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_c: UInt, init_running: UInt, init_i: UInt) -> (elow: UInt, ehigh: UInt, n: UInt, v: UInt, c: UInt, running: UInt, i: UInt) pre [(((((((init_elow + 4) == init_ehigh) && (init_n == ((init_ehigh - init_elow) + 1))) && (init_v == 1)) && (init_c == 0)) && (init_running == 0)) && !(init_i < init_elow)) && (init_i <= init_ehigh)] * (1/5) post [c == i] { @@ -48,11 +49,8 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, c = init_c running = init_running i = init_i - assert [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - havoc c, running, v - validate - assume [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - if running == 0 { + @k_induction(5, [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5)) + while running == 0 { v = 2 * v prob_choice = flip(0.5) if prob_choice { @@ -71,91 +69,5 @@ proc k_induction(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, if !(running == 0) { c = elow + c } else {} - coassert [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - coassert [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - coassert [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - coassert [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - if running == 0 { - v = 2 * v - prob_choice = flip(0.5) - if prob_choice { - c = (2 * c) + 1 - } else { - c = 2 * c - } - if !(v < n) { - if !(n == c) && !(n < c) { - running = 1 - } else { - v = v - n - c = c - n - } - } else {} - if !(running == 0) { - c = elow + c - } else {} - assert [(((((((elow + 4) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * (1/5) - assume 0 - } else {} - } else {} - } else {} - } else {} - } else {} + } } diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/cmd.py b/pgcl/pgcl2heyvl/pgcl2heyvl/cmd.py index 48b32766..7f7733d2 100644 --- a/pgcl/pgcl2heyvl/pgcl2heyvl/cmd.py +++ b/pgcl/pgcl2heyvl/pgcl2heyvl/cmd.py @@ -3,6 +3,14 @@ from typing import List, Union import click +from pgcl2heyvl.direct_encode import ( + direct_encode_ast_mciver, + direct_encode_bounded_mc, + direct_encode_k_ind, + direct_encode_omega_inv, + direct_encode_optional_stopping, + direct_encode_past, +) import probably.pgcl.substitute as substitute from pgcl2heyvl.encode import ( encode_ast_mciver, @@ -20,6 +28,10 @@ from probably.util.ref import Mut +# If this is set to True, the direct encoding will be used. +# The direct encoding does not use HeyVL encoding annotations and directly encodes the proof rules. +_direct = False + @click.group(cls=CommentArgsCommand, help=""" Convert a pGCL program into a HeyVL program. @@ -121,14 +133,16 @@ def encode_omega_invariant(file, calculus: str, invariant: str, post: str): print("Error: unsupported calculus type") sys.exit(1) + encoded = encode_omega_inv(program, calculus_type, invariant_expr, post_expr) + + + global _direct + if _direct: + encoded = direct_encode_omega_inv(program, calculus_type, invariant_expr, post_expr) + print( _auto_gen_comment(file) + hey_objects_str( - encode_omega_inv( - program, - calculus_type, - invariant_expr, - post_expr, - ))) + encoded)) @main.command(help=""" @@ -186,10 +200,17 @@ def encode_past_rule(file, invariant: str, eps: str, k: str): if isinstance(k_expr, CheckFail): print("Error: Cannot parse k:", k_expr) return + + + encoded = encode_past(program, invariant_expr, eps_expr, k_expr) + + global _direct + if _direct: + encoded = direct_encode_past(program, invariant_expr, eps_expr, k_expr) print( _auto_gen_comment(file) + - hey_objects_str(encode_past(program, invariant_expr, eps_expr, k_expr)) + hey_objects_str(encoded) ) @@ -270,10 +291,16 @@ def encode_ost_rule(file, post: str, invariant: str, past_invariant: str, print("Error: Cannot parse c:", c_expr) return + encoded = encode_optional_stopping(program, post_expr, invariant_expr, + past_invariant_expr, c_expr) + + global _direct + if _direct: + encoded = direct_encode_optional_stopping(program, post_expr, invariant_expr, + past_invariant_expr, c_expr) print( - _auto_gen_comment(file) + hey_objects_str( - encode_optional_stopping(program, post_expr, invariant_expr, - past_invariant_expr, c_expr))) + _auto_gen_comment(file) + hey_objects_str(encoded + )) @main.command(help=""" @@ -348,10 +375,17 @@ def encode_ast(file, invariant: str, variant: str, prob: str, decrease: str): print("Error: Cannot parse decrease expression:", decrease_expr) return + + encoded = encode_ast_mciver(program, invariant_expr, variant_expr, prob_expr, + decrease_expr) + + global _direct + if _direct: + encoded = direct_encode_ast_mciver(program, invariant_expr, variant_expr, prob_expr, + decrease_expr) print( _auto_gen_comment(file) + hey_objects_str( - encode_ast_mciver(program, invariant_expr, variant_expr, prob_expr, - decrease_expr))) + encoded)) @main.command(help=""" @@ -377,7 +411,7 @@ def encode_ast(file, invariant: str, variant: str, prob: str, decrease: str): @click.option('--calculus', type=click.STRING, help="The calculus for the encoding.", - metavar="EXPR") + metavar="STRING") @click.option('--k', type=click.INT, multiple=True, @@ -444,10 +478,17 @@ def encode_k_induction(file, post: str, pre: str, k: List[int], calculus: str, loop_annotations = list(zip(k, invariant_expr)) + encoded = encode_k_ind(program, post_expr, pre_expr, calculus_type, + loop_annotations) + + global _direct + if _direct: + encoded = direct_encode_k_ind(program, post_expr, pre_expr, calculus_type, + loop_annotations) + print( _auto_gen_comment(file) + hey_objects_str( - encode_k_ind(program, post_expr, pre_expr, calculus_type, - loop_annotations))) + encoded)) @main.command(help=""" @@ -542,10 +583,17 @@ def encode_bmc(file, post: str, pre: str, k: List[int], calculus: str, loop_annotations = list(zip(k, invariant_expr)) + + encoded = encode_bounded_mc(program, post_expr, pre_expr, calculus_type, + loop_annotations) + global _direct + if _direct: + encoded = direct_encode_bounded_mc(program, post_expr, pre_expr, calculus_type, + loop_annotations) + print( _auto_gen_comment(file) + hey_objects_str( - encode_bounded_mc(program, post_expr, pre_expr, calculus_type, - loop_annotations))) + encoded)) def parse_expectation_with_constants(program: Program, diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/direct_encode.py b/pgcl/pgcl2heyvl/pgcl2heyvl/direct_encode.py new file mode 100644 index 00000000..94293213 --- /dev/null +++ b/pgcl/pgcl2heyvl/pgcl2heyvl/direct_encode.py @@ -0,0 +1,948 @@ +import copy +from fractions import Fraction +from textwrap import indent +from typing import Dict, List, Set, Tuple, Union + +# trunk-ignore(flake8/F401) +from pgcl2heyvl.heyvl import ( + Calculus, + Direction, + HeyAssert, + HeyAssign, + HeyAssume, + HeyBlock, + HeyBoolType, + HeyComment, + HeyCompare, + HeyDecl, + HeyEURealType, + HeyExpr, + HeyHavoc, + HeyInstr, + HeyIte, + HeyNegate, + HeyNondet, + HeyObjects, + HeyProc, + HeySkip, + HeyTick, + HeyType, + HeyUIntType, + HeyURealType, + HeyValidate, +) +from probably.pgcl.ast import ( + AsgnInstr, + Binop, + BinopExpr, + BoolLitExpr, + BoolType, + CategoricalExpr, + ChoiceInstr, + CUniformExpr, + DUniformExpr, + Expr, + IfInstr, + Instr, + NatLitExpr, + NatType, + Program, + RealLitExpr, + RealType, + SkipInstr, + SubstExpr, + TickInstr, + Type, + Unop, + UnopExpr, + Var, + VarExpr, + WhileInstr, +) +from probably.pgcl.substitute import substitute_expr +from probably.pgcl.ast.walk import Walk, walk_expr, walk_instrs +from probably.util.ref import Mut + +_encode_direction: Direction = Direction.DOWN +_loop_annotation_stack: List[Tuple[int, Expr]] = [] +_bmc: bool = False + + +def direct_encode_k_ind(program: Program, post: Expr, pre: Expr, calculus: Calculus, + loop_annotations: List[Tuple[int, Expr]]) -> HeyObjects: + """ + Encode the proof for a lower/upper bound of an expectation of a pGCL loop using k-induction. + + Parameters + ---------- + + program: Program + The pGCL Program to be encoded. + invariant: Expr + The loop invariant. + post: Expr + The post expectation. + pre: Expr + The pre expectation. + direction: Direction + loop_annotations: List[Tupe[int,Expr]] + + Returns + ------- + HeyObjects + Encoding of the proof using k-induction. + + """ + hey_post = _encode_expr(post) + + # Replace the variables with their initial versions before encoding + hey_init_pre = _encode_expr(_to_init_expr(pre)) + + global _encode_direction + + if calculus == Calculus.WLP: + _encode_direction = Direction.DOWN + elif calculus == Calculus.WP or calculus == Calculus.ERT: + _encode_direction = Direction.UP + else: + raise Exception("unsupported calculus.") + + global _loop_annotation_stack + assert len(_loop_annotation_stack) == 0 + _loop_annotation_stack = [(k, _encode_expr(inv)) + for (k, inv) in loop_annotations] + + prob_choice_decl = [] + if _has_prob_choices(program): + prob_choice_decl = [HeyDecl("prob_choice", BoolType())] + + if calculus != Calculus.ERT: + _remove_tick_instrs(program) + + return [ + HeyComment( + "HeyVL file to show\n" + + f" {str(_encode_expr(pre))} {'>=' if _encode_direction == Direction.UP else '<='} {calculus}[C]({str(hey_post)})\n" + + + f"using k-induction with {', '.join([f'k = {k} and invariant = {_encode_expr(inv)}' for (k,inv) in loop_annotations])}\n" + + "for the pGCL program C:\n\n" + + f"{indent(str(program), ' ')}"), + _encode_proc(name="k_induction", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_instrs(program.instructions), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + pre=hey_init_pre, + post=hey_post) + ] + + +def direct_encode_bounded_mc(program: Program, post: Expr, pre: Expr, + calculus: Calculus, + loop_annotations: List[Tuple[int, Expr]]) -> HeyObjects: + """ + Encode the proof for refuting a lower/upper bound of an expectation of a pGCL loop using bounded model checking. + + Parameters + ---------- + + program: Program + The pGCL Program to be encoded. + invariant: Expr + The loop invariant. + post: Expr + The post expectation. + pre: Expr + The pre expectation. + direction: Direction + loop_annotations: List[Tupe[int,Expr]] + + Returns + ------- + HeyObjects + Encoding of the proof using k-induction. + + """ + hey_post = _encode_expr(post) + + # Replace the variables with their initial versions before encoding + hey_init_pre = _encode_expr(_to_init_expr(pre)) + + global _encode_direction + + if calculus == Calculus.WLP: + _encode_direction = Direction.DOWN + elif calculus == Calculus.WP or calculus == Calculus.ERT: + _encode_direction = Direction.UP + else: + raise Exception("unsupported calculus.") + + # Set the bmc flag to true, the rest is the same as k-induction + global _bmc + _bmc = True + + global _loop_annotation_stack + assert len(_loop_annotation_stack) == 0 + _loop_annotation_stack = [(k, _encode_expr(inv)) + for (k, inv) in loop_annotations] + + prob_choice_decl = [] + if _has_prob_choices(program): + prob_choice_decl = [HeyDecl("prob_choice", BoolType())] + + if calculus != Calculus.ERT: + _remove_tick_instrs(program) + + return [ + HeyComment( + "HeyVL file to show that\n" + + f" {str(_encode_expr(pre))} {'>=' if _encode_direction == Direction.UP else '<='} {calculus}[C]({str(hey_post)})\n" + + "DOES NOT HOLD\n" + + f"using bounded model checking with {', '.join([f'k = {k} and invariant = {_encode_expr(inv)}' for (k,inv) in loop_annotations])}\n" + + "for the pGCL program C:\n\n" + + f"{indent(str(program), ' ')}"), + _encode_proc(name="bounded_model_checking", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_instrs(program.instructions), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + pre=hey_init_pre, + post=hey_post) + ] + + +def direct_encode_ast_mciver(program: Program, invariant: Expr, variant: Expr, + prob: Expr, decrease: Expr) -> HeyObjects: + """ + Encode the proof rule for almost-sure termination of a pGCL loop + by McIver et al. (2018) + + Parameters + ---------- + + program: Program + The pGCL Program to be encoded. + invariant: Expr + The loop invariant. + variant: Expr + The variant function. + prob: Expr + The antitone probability function. + decrease: Expr + The antitone decrease function. + + Returns + ------- + HeyObjects + Encoding of the proof using the proof rule from McIver (2018). + + + """ + + # There should be only one loop in the program + loops_in_program = [ + loop for loop in program.instructions if isinstance(loop, WhileInstr) + ] + assert len(loops_in_program) == 1 + loop = loops_in_program[0] + + prob_choice_decl = [] + if _has_prob_choices(program): + prob_choice_decl = [HeyDecl("prob_choice", BoolType())] + + if "v" in program.variables or "l" in program.variables: + raise Exception("Program mustn't include a variable named 'v' and 'l'") + + # Encode expressions into HeyLo expressions + hey_variant = _encode_expr(variant) + hey_loop_cond = _encode_expr(loop.cond) + + # Substitute variables with their init versions for the progress condition + init_variant = _to_init_expr(variant) + + # [I] * [phi] * (p o V) + progress_pre_expr = _times( + _iverson(invariant), + _times(_iverson(loop.cond), _substitute_vars(prob, {"v": variant}))) + + # Replace all variables with their init versions for the preexpectation + progress_pre_expr = _to_init_expr(progress_pre_expr) + + # V <= V(s) - d(V(s)) + progress_post_expr = _iverson( + _leq( + variant, + _minus(init_variant, _substitute_vars(decrease, + {"v": init_variant})))) + + free_var_name = "l" + hey_prob_free_var = _encode_expr( + _substitute_vars(prob, {"v": VarExpr(free_var_name)})) + hey_decrease_free_var = _encode_expr( + _substitute_vars(decrease, {"v": VarExpr(free_var_name)})) + + hey_prob = _encode_expr(prob) + hey_decrease = _encode_expr(decrease) + + return [ + HeyComment( + "HeyVL file to show that C is almost-surely terminating\n" + + "using AST rule by McIver et al. (2018) with\n" + + f"invariant = {_encode_expr(invariant)}, variant = {hey_variant}, probability function p(v) = {_encode_expr(prob)}, decrease function d(v) = {_encode_expr(decrease)}\n" + + "for the pGCL program C:\n\n" + + f"{indent(str(program), ' ')}"), + # Check if prob is antitone + _encode_proc( + name="prob_antitone", + body=[ + HeyAssert( + Direction.DOWN, + HeyExpr( + f"forall {free_var_name}: UReal. (v <= {free_var_name}) ==> ({hey_prob_free_var} <= {hey_prob})" + ).embed()) + ], + input=_encode_var_dict(program.variables) | {"v": HeyURealType()}, + direction=Direction.DOWN, + comment= + f"forall {free_var_name}. (v <= {free_var_name}) ==> (prob({free_var_name}) <= prob(v))" + ), + # Check if decrease is antitone + _encode_proc( + name="decrease_antitone", + body=[ + HeyAssert( + Direction.DOWN, + HeyExpr( + f"forall {free_var_name}: UReal. (v <= {free_var_name}) ==> ({hey_decrease_free_var} <= {hey_decrease})" + ).embed()) + ], + input=_encode_var_dict(program.variables) | {"v": HeyURealType()}, + direction=Direction.DOWN, + comment= + f"forall {free_var_name}. (v <= {free_var_name}) ==> (decrease({free_var_name}) <= decrease(v))" + ), + # Check that [I] is a wp-subinvariant of the loop w.r.t. [I] + _encode_proc(name="I_wp_subinvariant", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, None, []), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.DOWN, + pre=_encode_expr(_to_init_expr(_iverson(invariant))), + post=_encode_expr(_iverson(invariant)), + comment="[I] <= \\Phi_{[I]}([I])"), + # Check that V = 0 indicates termination, i.e. !G iff V = 0 + _encode_proc( + name="termination_condition", + body=[ + HeyAssert( + Direction.DOWN, + HeyExpr(f"?(!({hey_loop_cond}) == ({hey_variant} == 0))")) + ], + input=_encode_var_dict(program.variables), + direction=Direction.DOWN, + comment="!G iff V = 0"), + # Check that V is a wp-superinvariant of the loop w.r.t V + _encode_proc(name="V_wp_superinvariant", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, None, []), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.UP, + pre=_encode_expr(init_variant), + post=_encode_expr(variant), + comment="\\Phi_{V}(V) <= V"), + # Check that V satisfies the progress condition + _encode_proc( + name="progress_condition", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_instrs(loop.body), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.DOWN, + pre=_encode_expr(progress_pre_expr), + post=_encode_expr(progress_post_expr), + comment="[I] * [G] * (p o V) <= \\s. wp[P]([V <= V(s) - d(V(s))])(s)" + ) + ] + + +def direct_encode_past(program: Program, invariant: Expr, eps: Expr, + k: Expr) -> HeyObjects: + """ + Encode the proof rule for positive almost-sure termination + by Chakarov et al. (2013) + + Parameters + ---------- + program: Program + The pGCL Program to be encoded. + invariant: Expr + The loop invariant. + eps:Expr + k:Expr + + Returns + ------- + HeyObjects + Encoding of the proof using the proof rule from Chakarov (2013). + + """ + + loops_in_program = [ + loop for loop in program.instructions if isinstance(loop, WhileInstr) + ] + assert len(loops_in_program) == 1 + loop = loops_in_program[0] + + if isinstance(eps, (RealLitExpr, NatLitExpr)) and isinstance( + k, (RealLitExpr, NatLitExpr)): + if eps.value >= k.value: + raise Exception("eps must be smaller than k.") + else: + raise Exception("k and eps must be constant positive numbers.") + + prob_choice_decl = [] + if _has_prob_choices(program): + prob_choice_decl = [HeyDecl("prob_choice", BoolType())] + + # [!G] * I <= K + hey_cond1_expr = _encode_expr( + _leq(_times(_iverson(_neg(loop.cond)), invariant), k)).embed() + + # [G] * K <= [G] * I + [!G] + hey_cond2_expr = _encode_expr( + _leq( + _times(_iverson(loop.cond), k), + _plus(_times(_iverson(loop.cond), invariant), + _iverson(_neg(loop.cond))))).embed() + # [G] * (I - eps) + hey_cond3_pre = _encode_expr( + _to_init_expr(_times(_iverson(loop.cond), _minus(invariant, eps)))) + + return [ + HeyComment( + "HeyVL file to show that C is positively almost-surely terminating\n" + + "using PAST rule by Chakarov et al. (2013) with\n" + + f"invariant = {_encode_expr(invariant)} eps = {_encode_expr(eps)} and k = {_encode_expr(k)}\n" + + "for the pGCL program C:\n\n" + + f"{indent(str(program), ' ')}"), + # Condition 1: [!G] * I <= K + _encode_proc(name="condition_1", + body=[HeyAssert(Direction.DOWN, hey_cond1_expr)], + input=_encode_var_dict(program.variables), + direction=Direction.DOWN, + comment="[!G] * I <= K"), + # Condition 2: [G] * K <= [G] * I + [!G] + _encode_proc(name="condition_2", + body=[HeyAssert(Direction.DOWN, hey_cond2_expr)], + input=_encode_var_dict(program.variables), + direction=Direction.DOWN, + comment="[G] * K <= [G] * I + [!G]"), + # Condition 3: \Phi_0(I) <= [G] * (I - eps) + _encode_proc(name="condition_3", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, _encode_expr(invariant), + _hey_const(_encode_expr(invariant))), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.UP, + pre=hey_cond3_pre, + post=HeyExpr("0"), + comment="\\Phi_0(I) <= [G] * (I - eps)") + ] + + +def direct_encode_optional_stopping(program: Program, post: Expr, invariant: Expr, + past_inv: Expr, c: Expr) -> HeyObjects: + """ + Encodes the proof for a lower bound to the wp of a pGCL program using + the optional stopping theorem from Aiming Low is Harder paper. + + Parameters + ---------- + program: Program + The pGCL Program to be encoded. + invariant: Expr + The loop invariant. + past_inv: Expr + The invariant for proving PAST of the loop. + c:Expr + The upperbound to the conditional difference boundedness condition. + + Returns + ------- + HeyObjects + Encoding of the proof using the optional stopping theorem. + + """ + loops_in_program = [ + loop for loop in program.instructions if isinstance(loop, WhileInstr) + ] + assert len(loops_in_program) == 1 + loop = loops_in_program[0] + + prob_choice_decl = [] + if _has_prob_choices(program): + prob_choice_decl = [HeyDecl("prob_choice", BoolType())] + + init_invariant = _to_init_expr(invariant) + + return [ + HeyComment( + "HeyVL file to show that\n" + + f" {_encode_expr(invariant)} <= wp[C]({_encode_expr(post)})\n" + + "using the Optional Stopping Theorem from Aiming Low is Harder paper with\n" + + + f"invariant = {_encode_expr(invariant)}, c = {_encode_expr(c)} and\n" + + + f"past-invariant = {_encode_expr(past_inv)} is used to show that C is PAST by showing\n " + + f" {_encode_expr(past_inv)} >= ert[C](0)\n" + + "for the pGCL program C:\n\n" + f"{indent(str(program), ' ')}"), + _encode_proc( + name="lt_infinity", + body=[ + HeyAssert( + Direction.DOWN, + HeyExpr(f"{_encode_expr(past_inv)} < ?(true)").embed()) + ], + input=_encode_var_dict(program.variables), + direction=Direction.DOWN, + comment="past_I < ∞"), + _encode_proc( + name="past", + body=prob_choice_decl + _encode_init_assign(program) + + # Inserted tick instruction to argue about ERT of the loop instead of WP/WLP + _encode_iter(loop, _encode_expr(past_inv), [HeyTick(HeyExpr("1"))] + + _hey_const(_encode_expr(past_inv))), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.UP, + pre=_encode_expr(_to_init_expr(past_inv)), + post=HeyExpr("0"), + comment="\\Phi_{0}(past_I) <= past_I, so ert[P](0) <= past_I"), + _encode_proc( + name="conditional_difference_bounded", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_instrs(loop.body), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.UP, + pre=_encode_expr(c), + post=HeyExpr( + f"ite({_encode_expr(_leq(init_invariant, invariant))}," + + f"{_encode_expr(_minus(invariant, init_invariant))}," + + f"{_encode_expr(_minus(init_invariant, invariant))})"), + comment="wp[P](|I(s)-I|)(s) <= c"), + _encode_proc(name="lower_bound", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, _encode_expr(invariant), + _hey_const(_encode_expr(invariant))), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.DOWN, + pre=_encode_expr(_to_init_expr(invariant)), + post=_encode_expr(post), + comment="I <= \\Phi_{post}(I)"), + _encode_proc( + name="harmonize_I_f", + body=[ + HeyAssert( + Direction.DOWN, + HeyExpr( + f"!{_encode_expr(loop.cond)} ==> ({_encode_expr(invariant)} == {_encode_expr(post)})" + ).embed()) + ], + input=_encode_var_dict(program.variables), + direction=Direction.DOWN, + comment="!guard ==> (I = f)", + ), + # Check if \Phi_f(I) < ∞, + _encode_proc(name="loopiter_lt_infty", + body=[ + HeyValidate(Direction.DOWN), + HeyAssume(Direction.DOWN, HeyExpr("\\infty")) + ] + prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, invariant, _hey_const(invariant)), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=Direction.UP, + pre=HeyExpr("0"), + post=_encode_expr(post), + comment="\\Phi_f(I) < ∞") + ] + + +def direct_encode_omega_inv(program: Program, calculus: Calculus, invariant: Expr, + post: Expr) -> HeyObjects: + """ + Encodes the proof for a lower/upper bound of an expectation of a pGCL loop using omega invariants. + + Parameters + ---------- + program: Program + The pGCL Program to be encoded. + invariant: Expr + The omega invariant sequence bound by a parameter 'n' + post: Expr + The post expectation. + + Returns + ------- + HeyObjects + Encoding of the proof using omega invariant. + + """ + loops_in_program = [ + loop for loop in program.instructions if isinstance(loop, WhileInstr) + ] + assert len(loops_in_program) == 1 + loop = loops_in_program[0] + + global _encode_direction + + if calculus == Calculus.WLP: + _encode_direction = Direction.UP + elif calculus == Calculus.WP or calculus == Calculus.ERT: + _encode_direction = Direction.DOWN + else: + raise Exception("unsupported calculus.") + + prob_choice_decl = [] + if _has_prob_choices(program): + prob_choice_decl = [HeyDecl("prob_choice", BoolType())] + + if "n" in program.variables: + raise Exception("Program shouldn't include a variable named n") + + program.variables["n"] = NatType(bounds=None) + + if calculus != Calculus.ERT: + _remove_tick_instrs(program) + + n_plus_1 = _plus(VarExpr("n"), NatLitExpr(1)) + # I_{n+1} + next_invariant = _substitute_vars(copy.deepcopy(invariant), + {"n": n_plus_1}) + # I_0 + null_invariant = _substitute_vars(copy.deepcopy(invariant), + {"n": NatLitExpr(0)}) + + operator = '>=' if _encode_direction == Direction.UP else '<=' + + char_func_name = 'Psi' if _encode_direction == Direction.UP else 'Phi' + + if calculus == Calculus.WLP: + top_or_bottom = 1 + elif calculus == Calculus.WP or calculus == Calculus.ERT: + top_or_bottom = 0 + else: + raise Exception("unsupported calculus.") + + return [ + HeyComment( + "HeyVL file to show\n" + + f" (sup n. {_encode_expr(invariant)}) <= {calculus}[C]({_encode_expr(post)})\n" + + + f"using omega-invariant = {_encode_expr(invariant)} for the pGCL program C:\n\n" + + f"{indent(str(program), ' ')}"), + # I_0 <= Phi_{post}(0) or Psi_{post}(1) <= I_0 + _encode_proc(name="condition_1", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, "0", _hey_const(top_or_bottom)), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + pre=_encode_expr(_to_init_expr(null_invariant)), + post=_encode_expr(post), + comment="I_0 " + operator + f" {char_func_name}" + + "_{post}" + f"({top_or_bottom})"), + # for all n. I_{n+1} <= Phi_{post}(I_n) + _encode_proc(name="condition_2", + body=prob_choice_decl + _encode_init_assign(program) + + _encode_iter(loop, _encode_expr(invariant), + _hey_const(_encode_expr(invariant))), + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + pre=_encode_expr(_to_init_expr(next_invariant)), + post=_encode_expr(post), + comment="for all n. I_{n+1} " + operator + + f" {char_func_name}" + "_{post}(I_n)"), + ] + + +def _encode_decls(program: Program) -> HeyBlock: + return [HeyDecl(name, typ) for (name, typ) in program.variables.items()] + + +def _get_init_vars(program: Program) -> Dict[Var, Type]: + return {f"init_{name}": typ for (name, typ) in program.variables.items()} + + +def _encode_init_assign(program: Program) -> HeyBlock: + return [ + HeyAssign(name, f"init_{name}") + for (name, typ) in program.variables.items() + ] + + +def _to_init_expr(expr: Expr) -> Expr: + return _substitute_vars( + expr, {var: VarExpr(f"init_{var}") + for var in _expr_vars(expr)}) + + +def _encode_expr(expr: Expr) -> HeyExpr: + + def inner_encode(expr: Expr): + res = _encode_expr(expr) + if isinstance( + expr, + (VarExpr, BoolLitExpr, NatLitExpr, RealLitExpr, UnopExpr)): + return res + else: + return f"({res})" + + if isinstance(expr, VarExpr): + return HeyExpr(expr.var) + elif isinstance(expr, BoolLitExpr): + return HeyExpr(str(expr)) + elif isinstance(expr, NatLitExpr): + return HeyExpr(str(expr)) + elif isinstance(expr, RealLitExpr): + if expr.is_infinite(): + return HeyExpr("∞") + else: + return HeyExpr(f"({str(expr)})" if "/" in str(expr) else str(expr)) + elif isinstance(expr, UnopExpr): + if expr.operator == Unop.NEG: + return HeyExpr(f"!{inner_encode(expr.expr)}") + elif expr.operator == Unop.IVERSON: + return HeyExpr(f"[{_encode_expr(expr.expr)}]") + elif isinstance(expr, BinopExpr): + operator = { + Binop.OR: "||", + Binop.AND: "&&", + Binop.LEQ: "<=", + Binop.LT: "<", + Binop.EQ: "==", + Binop.GT: ">", + Binop.GEQ: ">=", + Binop.PLUS: "+", + Binop.MINUS: "-", + Binop.TIMES: "*", + Binop.DIVIDE: "/", + Binop.MODULO: "%" + }[expr.operator] + return HeyExpr( + f"{inner_encode(expr.lhs)} {operator} {inner_encode(expr.rhs)}") + else: + raise Exception(f"unsupported expr : {expr}") + + +def _encode_loop(loop: WhileInstr, invariant: HeyExpr, k: int) -> HeyBlock: + global _bmc + global _encode_direction + + modified_vars = _collect_modified_vars(loop.body) + spec_or_empty = _encode_spec(invariant, modified_vars, + invariant) if not _bmc else [] + + if k <= 0: + return spec_or_empty + + if _bmc: + if _encode_direction == Direction.UP: + const_prog = _hey_const(HeyExpr("0")) + else: + const_prog = _hey_const(HeyExpr("1")) + next_iter = _encode_bmc(loop, invariant, k - 1, const_prog) + else: + const_prog = _hey_const(invariant) + next_iter = _encode_extend(loop, invariant, k - 1, const_prog) + + return spec_or_empty + _encode_iter(loop, invariant, next_iter) + + +def _encode_iter(loop: WhileInstr, invariant: HeyExpr, + next_iter: HeyBlock) -> HeyBlock: + return [ + HeyIte(_encode_expr(loop.cond), + _encode_instrs(loop.body) + next_iter, []) + ] + + +def _encode_var_typ(typ: Type) -> HeyType: + if isinstance(typ, BoolType): + return HeyBoolType() + if isinstance(typ, NatType): + assert typ.bounds is None + return HeyUIntType() + if isinstance(typ, RealType): + return HeyEURealType() + raise Exception("unsupported type") + + +def _encode_var_dict(vars: Dict[Var, Type]) -> Dict[Var, HeyType]: + return {var: _encode_var_typ(typ) for (var, typ) in vars.items()} + + +def _encode_proc(name: str, + body: HeyBlock, + input: Dict[Var, HeyType], + direction: Direction, + pre: HeyExpr = None, + post: HeyExpr = None, + output: Dict[Var, HeyType] = {}, + comment: str = "") -> HeyProc: + global _encode_direction + _encode_direction = direction + return HeyProc(_encode_direction, name, input, output, body, pre, post, + comment) + + +def _hey_const(expr: HeyExpr) -> HeyBlock: + return [ + HeyAssert(Direction.DOWN, expr), + HeyAssume(Direction.DOWN, HeyExpr("0")) + ] + + +def _encode_bmc(loop: WhileInstr, invariant: HeyExpr, k: int, + next_iter: HeyBlock): + if k == 0: + return next_iter + next_iter = _encode_bmc(loop, invariant, k - 1, next_iter) + global _encode_direction + return _encode_iter(loop, invariant, next_iter) + + +def _encode_extend(loop: WhileInstr, invariant: HeyExpr, k: int, + next_iter: HeyBlock) -> HeyBlock: + if k == 0: + return next_iter + next_iter = _encode_extend(loop, invariant, k - 1, next_iter) + global _encode_direction + return [HeyAssert(_encode_direction.flip(), invariant)] + _encode_iter( + loop, invariant, next_iter) + + +def _encode_spec(pre: HeyExpr, variables: List[Var], + post: HeyExpr) -> HeyBlock: + global _encode_direction + return [ + HeyAssert(_encode_direction, pre), + HeyHavoc(_encode_direction, variables), + HeyValidate(_encode_direction), + HeyAssume(_encode_direction, post) + ] + + +def _encode_instrs(instrs: List[Instr]) -> HeyBlock: + + def generate(): + for instr in instrs: + res = _encode_instr(instr) + if isinstance(res, list): + yield from res + else: + yield res + + return list(generate()) + + +def _encode_instr(instr: Instr) -> Union[Instr, List[Instr]]: + if isinstance(instr, SkipInstr): + return HeySkip() + if isinstance(instr, WhileInstr): + (k, invariant) = _loop_annotation_stack.pop(0) + return _encode_loop(instr, invariant, k) + if isinstance(instr, IfInstr): + return HeyIte(_encode_expr(instr.cond), _encode_instrs(instr.true), + _encode_instrs(instr.false)) + if isinstance(instr, AsgnInstr): + assert not isinstance(instr.rhs, + (CUniformExpr, DUniformExpr, CategoricalExpr)) + return HeyAssign(instr.lhs, _encode_expr(instr.rhs)) + if isinstance(instr, ChoiceInstr): + return [ + HeyAssign("prob_choice", + HeyExpr(f"flip({_encode_expr(instr.prob)})")), + HeyIte(HeyExpr("prob_choice"), _encode_instrs(instr.lhs), + _encode_instrs(instr.rhs)) + ] + if isinstance(instr, TickInstr): + return HeyTick(_encode_expr(instr.expr)) + raise Exception("unsupported instruction") + + +def _collect_modified_vars(instrs: List[Instr]) -> List[Var]: + modified: Set[Var] = set() + for ref in walk_instrs(Walk.DOWN, instrs): + if isinstance(ref.val, AsgnInstr): + modified.add(ref.val.lhs) + return sorted(modified) + + +def _prob_to_odds(prob: Fraction) -> Tuple[int, int]: + return (prob.numerator, prob.denominator - prob.numerator) + + +def _has_prob_choices(program: Program) -> bool: + for instr_ref in walk_instrs(Walk.DOWN, program.instructions): + if isinstance(instr_ref.val, ChoiceInstr): + return True + return False + + +def _remove_tick_instrs(program: Program): + for instr_ref in walk_instrs(Walk.DOWN, program.instructions): + if isinstance(instr_ref.val, TickInstr): + instr_ref.val = SkipInstr() + + +def _iverson(expr: Expr) -> Expr: + return UnopExpr(Unop.IVERSON, expr) + + +def _times(lhs: Expr, rhs: Expr) -> Expr: + return BinopExpr(Binop.TIMES, lhs, rhs) + + +def _leq(lhs: Expr, rhs: Expr) -> Expr: + return BinopExpr(Binop.LEQ, lhs, rhs) + + +def _le(lhs: Expr, rhs: Expr) -> Expr: + return BinopExpr(Binop.LE, lhs, rhs) + + +def _minus(lhs: Expr, rhs: Expr) -> Expr: + return BinopExpr(Binop.MINUS, lhs, rhs) + + +def _neg(expr: Expr) -> Expr: + return UnopExpr(Unop.NEG, expr) + + +def _plus(lhs: Expr, rhs: Expr) -> Expr: + return BinopExpr(Binop.PLUS, lhs, rhs) + + +def _substitute_vars(expr: Expr, mapping: Dict[Var, Expr]) -> Expr: + # Substitute variables in an expression + expr = copy.deepcopy(expr) + expr_ref = Mut.alloc(SubstExpr(mapping, expr)) + substitute_expr(expr_ref) + return expr_ref.val + + +def _expr_vars(expr: Expr) -> List[str]: + # Find the vars in an expression + return [ + ref.val.var for ref in walk_expr(Walk.DOWN, Mut.alloc(expr)) + if isinstance(ref.val, VarExpr) + ] diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/encode.py b/pgcl/pgcl2heyvl/pgcl2heyvl/encode.py index 024b1056..469f893f 100644 --- a/pgcl/pgcl2heyvl/pgcl2heyvl/encode.py +++ b/pgcl/pgcl2heyvl/pgcl2heyvl/encode.py @@ -1,12 +1,15 @@ import copy from fractions import Fraction from textwrap import indent -from typing import Dict, List, Set, Tuple, Union +from typing import Any, Dict, List, Set, Tuple, Union # trunk-ignore(flake8/F401) from pgcl2heyvl.heyvl import ( + Encoding, Calculus, Direction, + HeyEncodingAnnotation, + HeyCalculusAnnotation, HeyAssert, HeyAssign, HeyAssume, @@ -30,6 +33,7 @@ HeyUIntType, HeyURealType, HeyValidate, + HeyWhile, ) from probably.pgcl.ast import ( AsgnInstr, @@ -64,9 +68,6 @@ from probably.util.ref import Mut _encode_direction: Direction = Direction.DOWN -_loop_annotation_stack: List[Tuple[int, Expr]] = [] -_bmc: bool = False - def encode_k_ind(program: Program, post: Expr, pre: Expr, calculus: Calculus, loop_annotations: List[Tuple[int, Expr]]) -> HeyObjects: @@ -107,10 +108,7 @@ def encode_k_ind(program: Program, post: Expr, pre: Expr, calculus: Calculus, else: raise Exception("unsupported calculus.") - global _loop_annotation_stack - assert len(_loop_annotation_stack) == 0 - _loop_annotation_stack = [(k, _encode_expr(inv)) - for (k, inv) in loop_annotations] + loop_annotation_stack = [(Encoding.K_INDUCTION, [k, _encode_expr(inv)]) for (k, inv) in loop_annotations] prob_choice_decl = [] if _has_prob_choices(program): @@ -119,6 +117,23 @@ def encode_k_ind(program: Program, post: Expr, pre: Expr, calculus: Calculus, if calculus != Calculus.ERT: _remove_tick_instrs(program) + + # Encode the program without any annotations + hey_instrs = _encode_instrs(program.instructions) + + annotated_block = _annotate_heyblock(hey_instrs, loop_annotation_stack) + + return_object = _encode_proc(name="main", + body= prob_choice_decl + _encode_init_assign(program) + annotated_block, + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + pre=hey_init_pre, + post=hey_post) + + if calculus is not None : + return_object = HeyCalculusAnnotation(calculus, return_object) + return [ HeyComment( "HeyVL file to show\n" + @@ -127,14 +142,7 @@ def encode_k_ind(program: Program, post: Expr, pre: Expr, calculus: Calculus, f"using k-induction with {', '.join([f'k = {k} and invariant = {_encode_expr(inv)}' for (k,inv) in loop_annotations])}\n" + "for the pGCL program C:\n\n" + f"{indent(str(program), ' ')}"), - _encode_proc(name="k_induction", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_instrs(program.instructions), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=_encode_direction, - pre=hey_init_pre, - post=hey_post) + return_object ] @@ -178,13 +186,7 @@ def encode_bounded_mc(program: Program, post: Expr, pre: Expr, else: raise Exception("unsupported calculus.") - # Set the bmc flag to true, the rest is the same as k-induction - global _bmc - _bmc = True - - global _loop_annotation_stack - assert len(_loop_annotation_stack) == 0 - _loop_annotation_stack = [(k, _encode_expr(inv)) + loop_annotation_stack = [(Encoding.UNROLL, [k, _encode_expr(inv)]) for (k, inv) in loop_annotations] prob_choice_decl = [] @@ -194,6 +196,19 @@ def encode_bounded_mc(program: Program, post: Expr, pre: Expr, if calculus != Calculus.ERT: _remove_tick_instrs(program) + # Encode the program without any annotations + hey_instrs = _encode_instrs(program.instructions) + + annotated_block = _annotate_heyblock(hey_instrs, loop_annotation_stack) + + return_object = _encode_proc(name="main", + body= prob_choice_decl + _encode_init_assign(program) + annotated_block, + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + pre=hey_init_pre, + post=hey_post) + return [ HeyComment( "HeyVL file to show that\n" + @@ -202,14 +217,7 @@ def encode_bounded_mc(program: Program, post: Expr, pre: Expr, f"using bounded model checking with {', '.join([f'k = {k} and invariant = {_encode_expr(inv)}' for (k,inv) in loop_annotations])}\n" + "for the pGCL program C:\n\n" + f"{indent(str(program), ' ')}"), - _encode_proc(name="bounded_model_checking", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_instrs(program.instructions), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=_encode_direction, - pre=hey_init_pre, - post=hey_post) + return_object ] @@ -246,45 +254,40 @@ def encode_ast_mciver(program: Program, invariant: Expr, variant: Expr, loop for loop in program.instructions if isinstance(loop, WhileInstr) ] assert len(loops_in_program) == 1 - loop = loops_in_program[0] prob_choice_decl = [] if _has_prob_choices(program): prob_choice_decl = [HeyDecl("prob_choice", BoolType())] - if "v" in program.variables or "l" in program.variables: - raise Exception("Program mustn't include a variable named 'v' and 'l'") + if "v" in program.variables: + raise Exception("Program mustn't include a variable named 'v'") # Encode expressions into HeyLo expressions hey_variant = _encode_expr(variant) - hey_loop_cond = _encode_expr(loop.cond) - - # Substitute variables with their init versions for the progress condition - init_variant = _to_init_expr(variant) + hey_prob = _encode_expr(prob) + hey_decrease = _encode_expr(decrease) + hey_invariant = _encode_expr(invariant) - # [I] * [phi] * (p o V) - progress_pre_expr = _times( - _iverson(invariant), - _times(_iverson(loop.cond), _substitute_vars(prob, {"v": variant}))) - # Replace all variables with their init versions for the preexpectation - progress_pre_expr = _to_init_expr(progress_pre_expr) + # Encode the program without any annotations + hey_instrs = _encode_instrs(program.instructions) - # V <= V(s) - d(V(s)) - progress_post_expr = _iverson( - _leq( - variant, - _minus(init_variant, _substitute_vars(decrease, - {"v": init_variant})))) + hey_arg_list = [hey_invariant,hey_variant,"v",hey_prob,hey_decrease] - free_var_name = "l" - hey_prob_free_var = _encode_expr( - _substitute_vars(prob, {"v": VarExpr(free_var_name)})) - hey_decrease_free_var = _encode_expr( - _substitute_vars(decrease, {"v": VarExpr(free_var_name)})) + # # Iterate over the instructions and replace the HeyWhile instructions with annotated versions + # for i, hey_instr in enumerate(hey_instrs): + # if isinstance(hey_instr, HeyWhile): + # hey_instrs[i] = HeyEncodingAnnotation(Encoding.AST, hey_arg_list, hey_instr) - hey_prob = _encode_expr(prob) - hey_decrease = _encode_expr(decrease) + annotated_block = _annotate_heyblock(hey_instrs, [(Encoding.AST, hey_arg_list)]) + + return_object = _encode_proc(name="main", + body= prob_choice_decl + _encode_init_assign(program) + annotated_block, + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + ) + return [ HeyComment( @@ -293,79 +296,7 @@ def encode_ast_mciver(program: Program, invariant: Expr, variant: Expr, f"invariant = {_encode_expr(invariant)}, variant = {hey_variant}, probability function p(v) = {_encode_expr(prob)}, decrease function d(v) = {_encode_expr(decrease)}\n" + "for the pGCL program C:\n\n" + f"{indent(str(program), ' ')}"), - # Check if prob is antitone - _encode_proc( - name="prob_antitone", - body=[ - HeyAssert( - Direction.DOWN, - HeyExpr( - f"forall {free_var_name}: UReal. (v <= {free_var_name}) ==> ({hey_prob_free_var} <= {hey_prob})" - ).embed()) - ], - input=_encode_var_dict(program.variables) | {"v": HeyURealType()}, - direction=Direction.DOWN, - comment= - f"forall {free_var_name}. (v <= {free_var_name}) ==> (prob({free_var_name}) <= prob(v))" - ), - # Check if decrease is antitone - _encode_proc( - name="decrease_antitone", - body=[ - HeyAssert( - Direction.DOWN, - HeyExpr( - f"forall {free_var_name}: UReal. (v <= {free_var_name}) ==> ({hey_decrease_free_var} <= {hey_decrease})" - ).embed()) - ], - input=_encode_var_dict(program.variables) | {"v": HeyURealType()}, - direction=Direction.DOWN, - comment= - f"forall {free_var_name}. (v <= {free_var_name}) ==> (decrease({free_var_name}) <= decrease(v))" - ), - # Check that [I] is a wp-subinvariant of the loop w.r.t. [I] - _encode_proc(name="I_wp_subinvariant", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_iter(loop, None, []), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.DOWN, - pre=_encode_expr(_to_init_expr(_iverson(invariant))), - post=_encode_expr(_iverson(invariant)), - comment="[I] <= \\Phi_{[I]}([I])"), - # Check that V = 0 indicates termination, i.e. !G iff V = 0 - _encode_proc( - name="termination_condition", - body=[ - HeyAssert( - Direction.DOWN, - HeyExpr(f"?(!({hey_loop_cond}) == ({hey_variant} == 0))")) - ], - input=_encode_var_dict(program.variables), - direction=Direction.DOWN, - comment="!G iff V = 0"), - # Check that V is a wp-superinvariant of the loop w.r.t V - _encode_proc(name="V_wp_superinvariant", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_iter(loop, None, []), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.UP, - pre=_encode_expr(init_variant), - post=_encode_expr(variant), - comment="\\Phi_{V}(V) <= V"), - # Check that V satisfies the progress condition - _encode_proc( - name="progress_condition", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_instrs(loop.body), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.DOWN, - pre=_encode_expr(progress_pre_expr), - post=_encode_expr(progress_post_expr), - comment="[I] * [G] * (p o V) <= \\s. wp[P]([V <= V(s) - d(V(s))])(s)" - ) + return_object ] @@ -408,19 +339,24 @@ def encode_past(program: Program, invariant: Expr, eps: Expr, if _has_prob_choices(program): prob_choice_decl = [HeyDecl("prob_choice", BoolType())] - # [!G] * I <= K - hey_cond1_expr = _encode_expr( - _leq(_times(_iverson(_neg(loop.cond)), invariant), k)).embed() + hey_k = _encode_expr(k) + hey_eps = _encode_expr(eps) + hey_invariant = _encode_expr(invariant) - # [G] * K <= [G] * I + [!G] - hey_cond2_expr = _encode_expr( - _leq( - _times(_iverson(loop.cond), k), - _plus(_times(_iverson(loop.cond), invariant), - _iverson(_neg(loop.cond))))).embed() - # [G] * (I - eps) - hey_cond3_pre = _encode_expr( - _to_init_expr(_times(_iverson(loop.cond), _minus(invariant, eps)))) + hey_arg_list = [hey_invariant,hey_eps,hey_k] + + # Encode the program without any annotations + hey_instrs = _encode_instrs(program.instructions) + + annotated_block = _annotate_heyblock(hey_instrs, [(Encoding.PAST, hey_arg_list)]) + + return_object = _encode_proc(name="main", + body= prob_choice_decl + _encode_init_assign(program) + annotated_block, + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + ) + return [ HeyComment( @@ -429,29 +365,7 @@ def encode_past(program: Program, invariant: Expr, eps: Expr, f"invariant = {_encode_expr(invariant)} eps = {_encode_expr(eps)} and k = {_encode_expr(k)}\n" + "for the pGCL program C:\n\n" + f"{indent(str(program), ' ')}"), - # Condition 1: [!G] * I <= K - _encode_proc(name="condition_1", - body=[HeyAssert(Direction.DOWN, hey_cond1_expr)], - input=_encode_var_dict(program.variables), - direction=Direction.DOWN, - comment="[!G] * I <= K"), - # Condition 2: [G] * K <= [G] * I + [!G] - _encode_proc(name="condition_2", - body=[HeyAssert(Direction.DOWN, hey_cond2_expr)], - input=_encode_var_dict(program.variables), - direction=Direction.DOWN, - comment="[G] * K <= [G] * I + [!G]"), - # Condition 3: \Phi_0(I) <= [G] * (I - eps) - _encode_proc(name="condition_3", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_iter(loop, _encode_expr(invariant), - _hey_const(_encode_expr(invariant))), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.UP, - pre=hey_cond3_pre, - post=HeyExpr("0"), - comment="\\Phi_0(I) <= [G] * (I - eps)") + return_object ] @@ -482,13 +396,29 @@ def encode_optional_stopping(program: Program, post: Expr, invariant: Expr, loop for loop in program.instructions if isinstance(loop, WhileInstr) ] assert len(loops_in_program) == 1 - loop = loops_in_program[0] prob_choice_decl = [] if _has_prob_choices(program): prob_choice_decl = [HeyDecl("prob_choice", BoolType())] - init_invariant = _to_init_expr(invariant) + hey_post = _encode_expr(post) + hey_invariant = _encode_expr(invariant) + hey_past_inv = _encode_expr(past_inv) + hey_c = _encode_expr(c) + + hey_arg_list = [hey_invariant,hey_past_inv,hey_c, hey_post] + + # Encode the program without any annotations + hey_instrs = _encode_instrs(program.instructions) + + annotated_block = _annotate_heyblock(hey_instrs, [(Encoding.OST, hey_arg_list)]) + + return_object = _encode_proc(name="main", + body= prob_choice_decl + _encode_init_assign(program) + annotated_block, + input=_encode_var_dict(_get_init_vars(program)), + output=_encode_var_dict(program.variables), + direction=_encode_direction, + ) return [ HeyComment( @@ -501,77 +431,7 @@ def encode_optional_stopping(program: Program, post: Expr, invariant: Expr, f"past-invariant = {_encode_expr(past_inv)} is used to show that C is PAST by showing\n " + f" {_encode_expr(past_inv)} >= ert[C](0)\n" + "for the pGCL program C:\n\n" + f"{indent(str(program), ' ')}"), - _encode_proc( - name="lt_infinity", - body=[ - HeyAssert( - Direction.DOWN, - HeyExpr(f"{_encode_expr(past_inv)} < ?(true)").embed()) - ], - input=_encode_var_dict(program.variables), - direction=Direction.DOWN, - comment="past_I < ∞"), - _encode_proc( - name="past", - body=prob_choice_decl + _encode_init_assign(program) + - # Inserted tick instruction to argue about ERT of the loop instead of WP/WLP - _encode_iter(loop, _encode_expr(past_inv), [HeyTick(HeyExpr("1"))] - + _hey_const(_encode_expr(past_inv))), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.UP, - pre=_encode_expr(_to_init_expr(past_inv)), - post=HeyExpr("0"), - comment="\\Phi_{0}(past_I) <= past_I, so ert[P](0) <= past_I"), - _encode_proc( - name="conditional_difference_bounded", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_instrs(loop.body), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.UP, - pre=_encode_expr(c), - post=HeyExpr( - f"ite({_encode_expr(_leq(init_invariant, invariant))}," + - f"{_encode_expr(_minus(invariant, init_invariant))}," + - f"{_encode_expr(_minus(init_invariant, invariant))})"), - comment="wp[P](|I(s)-I|)(s) <= c"), - _encode_proc(name="lower_bound", - body=prob_choice_decl + _encode_init_assign(program) + - _encode_iter(loop, _encode_expr(invariant), - _hey_const(_encode_expr(invariant))), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.DOWN, - pre=_encode_expr(_to_init_expr(invariant)), - post=_encode_expr(post), - comment="I <= \\Phi_{post}(I)"), - _encode_proc( - name="harmonize_I_f", - body=[ - HeyAssert( - Direction.DOWN, - HeyExpr( - f"!{_encode_expr(loop.cond)} ==> ({_encode_expr(invariant)} == {_encode_expr(post)})" - ).embed()) - ], - input=_encode_var_dict(program.variables), - direction=Direction.DOWN, - comment="!guard ==> (I = f)", - ), - # Check if \Phi_f(I) < ∞, - _encode_proc(name="loopiter_lt_infty", - body=[ - HeyValidate(Direction.DOWN), - HeyAssume(Direction.DOWN, HeyExpr("\\infty")) - ] + prob_choice_decl + _encode_init_assign(program) + - _encode_iter(loop, invariant, _hey_const(invariant)), - input=_encode_var_dict(_get_init_vars(program)), - output=_encode_var_dict(program.variables), - direction=Direction.UP, - pre=HeyExpr("0"), - post=_encode_expr(post), - comment="\\Phi_f(I) < ∞") + return_object ] @@ -579,6 +439,7 @@ def encode_omega_inv(program: Program, calculus: Calculus, invariant: Expr, post: Expr) -> HeyObjects: """ Encodes the proof for a lower/upper bound of an expectation of a pGCL loop using omega invariants. + Still uses the same direct encoding. Parameters ---------- @@ -743,28 +604,6 @@ def inner_encode(expr: Expr): raise Exception(f"unsupported expr : {expr}") -def _encode_loop(loop: WhileInstr, invariant: HeyExpr, k: int) -> HeyBlock: - global _bmc - global _encode_direction - - modified_vars = _collect_modified_vars(loop.body) - spec_or_empty = _encode_spec(invariant, modified_vars, - invariant) if not _bmc else [] - - if k <= 0: - return spec_or_empty - - if _bmc: - if _encode_direction == Direction.UP: - const_prog = _hey_const(HeyExpr("0")) - else: - const_prog = _hey_const(HeyExpr("1")) - next_iter = _encode_bmc(loop, invariant, k - 1, const_prog) - else: - const_prog = _hey_const(invariant) - next_iter = _encode_extend(loop, invariant, k - 1, const_prog) - - return spec_or_empty + _encode_iter(loop, invariant, next_iter) def _encode_iter(loop: WhileInstr, invariant: HeyExpr, @@ -858,8 +697,7 @@ def _encode_instr(instr: Instr) -> Union[Instr, List[Instr]]: if isinstance(instr, SkipInstr): return HeySkip() if isinstance(instr, WhileInstr): - (k, invariant) = _loop_annotation_stack.pop(0) - return _encode_loop(instr, invariant, k) + return HeyWhile(_encode_expr(instr.cond), _encode_instrs(instr.body)) if isinstance(instr, IfInstr): return HeyIte(_encode_expr(instr.cond), _encode_instrs(instr.true), _encode_instrs(instr.false)) @@ -878,6 +716,24 @@ def _encode_instr(instr: Instr) -> Union[Instr, List[Instr]]: return HeyTick(_encode_expr(instr.expr)) raise Exception("unsupported instruction") +def _annotate_heyblock(hey_block: HeyBlock, annotation_stack: List[Tuple[Encoding, List[HeyExpr]]]) -> HeyBlock: + + return_block = hey_block + # Iterate over the instructions and replace the HeyWhile instructions with annotated versions + for i, hey_instr in enumerate(hey_block): + if isinstance(hey_instr, HeyWhile): + if len(annotation_stack) != 0: + annotation = annotation_stack.pop(0) + encoding = annotation[0] + hey_arg_list = annotation[1] + + new_hey_instr = HeyWhile(hey_instr.cond, _annotate_heyblock(hey_instr.body, annotation_stack)) + + return_block[i] = HeyEncodingAnnotation(encoding, hey_arg_list , new_hey_instr) + else: + raise Exception("Missing loop annotations") + + return return_block def _collect_modified_vars(instrs: List[Instr]) -> List[Var]: modified: Set[Var] = set() diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/heyvl.py b/pgcl/pgcl2heyvl/pgcl2heyvl/heyvl.py index cfbc03f4..f7b16405 100644 --- a/pgcl/pgcl2heyvl/pgcl2heyvl/heyvl.py +++ b/pgcl/pgcl2heyvl/pgcl2heyvl/heyvl.py @@ -151,6 +151,32 @@ def __str__(self) -> str: return "wlp" +class Encoding(Enum): + INVARIANT = auto() + K_INDUCTION = auto() + UNROLL = auto() + PAST = auto() + AST = auto() + OMEGA = auto() + OST = auto() + + def __str__(self): + + if self == Encoding.INVARIANT: + return "invariant" + elif self == Encoding.K_INDUCTION: + return "k_induction" + elif self == Encoding.UNROLL: + return "unroll" + elif self == Encoding.PAST: + return "past" + elif self == Encoding.AST: + return "ast" + elif self == Encoding.OMEGA: + return "omega_invariant" + elif self == Encoding.OST: + return "ost" + @attr.s class HeyHavoc(HeyInstr): direction: Direction = attr.ib() @@ -292,3 +318,35 @@ def __str__(self) -> str: return indent( indent(self.comment, "// ", lambda line: not line.isspace()), "//", lambda line: line.isspace()) + + +@attr.s +class HeyEncodingAnnotation(HeyInstr): + encoding: Encoding = attr.ib() + args: List[HeyExpr] = attr.ib() + stmt: HeyInstr = attr.ib() + + + def __str__(self): + + arg_list = ", ".join( + [f"{arg}" for arg in self.args]) + + return f"@{self.encoding}({arg_list})\n{self.stmt}" + + +@attr.s +class HeyCalculusAnnotation(HeyObject): + calculus: Calculus = attr.ib() + proc: HeyObject = attr.ib() + + def __str__(self) -> str: + return f"@{self.calculus}\n{self.proc}" + +@attr.s +class HeyWhile(HeyInstr): + cond: HeyExpr = attr.ib() + body: HeyBlock = attr.ib() + + def __str__(self) -> str: + return f"while {self.cond} {_str_block(self.body)}" diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/tests/test_encodings.py b/pgcl/pgcl2heyvl/pgcl2heyvl/tests/test_encodings.py index bd7d2e4d..483a4393 100644 --- a/pgcl/pgcl2heyvl/pgcl2heyvl/tests/test_encodings.py +++ b/pgcl/pgcl2heyvl/pgcl2heyvl/tests/test_encodings.py @@ -4,12 +4,12 @@ import probably.pgcl.substitute as substitute import pytest -from pgcl2heyvl.encode import ( - encode_ast_mciver, - encode_k_ind, - encode_omega_inv, - encode_optional_stopping, - encode_past, +from pgcl2heyvl.direct_encode import ( + direct_encode_ast_mciver, + direct_encode_k_ind, + direct_encode_omega_inv, + direct_encode_optional_stopping, + direct_encode_past, ) from pgcl2heyvl.heyvl import Calculus, hey_objects_str from probably.pgcl.ast import Expr, Program @@ -63,7 +63,7 @@ def test_encode_ast_mciver(save): prob = _parse_expectation_with_constants(program, "1/(v+1)") decrease = _parse_expectation_with_constants(program, "1") return hey_objects_str( - encode_ast_mciver(program, invariant, variant, prob, decrease)) + direct_encode_ast_mciver(program, invariant, variant, prob, decrease)) @golden_test() @@ -78,7 +78,7 @@ def test_encode_k_ind(save): k = 5 loop_annotations = [(k, pre_expr)] return hey_objects_str( - encode_k_ind(program=program, + direct_encode_k_ind(program=program, post=post_expr, pre=pre_expr, calculus=Calculus.WP, @@ -93,7 +93,7 @@ def test_encode_omega_inv(save): invariant = _parse_expectation_with_constants(program, "[x <= n] * x") post = _parse_expectation_with_constants(program, "0") return hey_objects_str( - encode_omega_inv(program, Calculus.ERT, invariant, post)) + direct_encode_omega_inv(program, Calculus.ERT, invariant, post)) @golden_test() @@ -106,7 +106,7 @@ def test_encode_optional_stopping(save): past_inv = _parse_expectation_with_constants(program, "2 * [a]") post_expr = _parse_expectation_with_constants(program, "b") return hey_objects_str( - encode_optional_stopping(program, post_expr, invariant, past_inv, c)) + direct_encode_optional_stopping(program, post_expr, invariant, past_inv, c)) @golden_test() @@ -117,7 +117,7 @@ def test_encode_past(save): invariant = _parse_expectation_with_constants(program, "x+1") eps = _parse_expectation_with_constants(program, "0.5") k = _parse_expectation_with_constants(program, "1") - return hey_objects_str(encode_past(program, invariant, eps, k)) + return hey_objects_str(direct_encode_past(program, invariant, eps, k)) def _parse_expectation_with_constants(program: Program, diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/utils.py b/pgcl/pgcl2heyvl/pgcl2heyvl/utils.py index 0718d92d..5957f077 100644 --- a/pgcl/pgcl2heyvl/pgcl2heyvl/utils.py +++ b/pgcl/pgcl2heyvl/pgcl2heyvl/utils.py @@ -68,8 +68,6 @@ def _read_args_from_code(group: click.Group, ctx: click.Context, code: str): # Parse the command line args to overwrite file ARGS (if present) sysargs, _, _ = encoding_parser.parse_args( _list_after_first_match(sys.argv[2:], lambda x: x.startswith("--"))) - # Add "encoding" to the params to be able to invoke the corresponding function later im cmd.py - ctx.params["encoding"] = encoding_command.name used_defaults = dict() for param in opts_values: diff --git a/pgcl/pgcl2heyvl/pyproject.toml b/pgcl/pgcl2heyvl/pyproject.toml index 8194d25f..2e5afd5a 100644 --- a/pgcl/pgcl2heyvl/pyproject.toml +++ b/pgcl/pgcl2heyvl/pyproject.toml @@ -13,8 +13,6 @@ attrs = "^19.3.0" [tool.poetry.scripts] pgcl2heyvl = "pgcl2heyvl.cmd:main" -[tool.poetry.dev-dependencies] - [tool.poetry.group.dev.dependencies] pytest = "^7.2.2"