From c5017302127f2e467ca64eb1f9a6f7f00e49cb98 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 6 Jan 2022 16:05:02 +0100
Subject: [PATCH] [wp] test tactic modmask
---
src/plugins/wp/tests/wp_tip/modmask.i | 18 ++
.../tests/wp_tip/oracle/modmask.0.res.oracle | 79 +++++++++
.../script/check_lemma_and_modulo_u.json | 162 ++++++++++++++++++
.../script/check_lemma_and_modulo_us_255.json | 14 ++
.../tests/wp_tip/oracle/modmask.1.res.oracle | 79 +++++++++
.../script/check_lemma_and_modulo_u.json | 162 ++++++++++++++++++
.../script/check_lemma_and_modulo_us_255.json | 14 ++
7 files changed, 528 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_tip/modmask.i
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
diff --git a/src/plugins/wp/tests/wp_tip/modmask.i b/src/plugins/wp/tests/wp_tip/modmask.i
new file mode 100644
index 00000000000..1970a5e6202
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/modmask.i
@@ -0,0 +1,18 @@
+/* run.config
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+/*@
+ check lemma and_modulo_us_255:
+ \forall unsigned short us ; (us & 0xFF) == us % 0x100 ;
+*/
+
+/*@
+ check lemma and_modulo_u:
+ \forall unsigned us, integer shift;
+ 0 <= shift < (sizeof(us) * 8) ==> (us & ((1 << shift) - 1)) == us % (1 << shift);
+*/
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
new file mode 100644
index 00000000000..dd1cd3edf7d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -0,0 +1,79 @@
+# frama-c -wp [...]
+[kernel] Parsing modmask.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp:script:allgoals]
+ Lemma and_modulo_u:
+ Prove: let x_0 = (lsl 1 shift_0) in
+ (0<=shift_0) -> (shift_0<=31) -> (is_uint32 us_0)
+ -> ((us_0 mod x_0)=(land us_0 (x_0-1)))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Lemma and_modulo_us_255:
+ Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-0 (generated):
+ Let x = lsl(1, shift_0).
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: (0 <= us_0) /\ (0 < x) /\ (exists i : Z. (lsl(1, i) = x) /\ (0 <= i)).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
+ Assume { Have: is_uint16(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-3 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 < lsl(1, shift_0).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-4 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_u : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 0
+ Script: 2
+[wp] Updated session with 2 new valid scripts.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
new file mode 100644
index 00000000000..e40e8863e3c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
@@ -0,0 +1,162 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "us_0 mod (lsl 1 shift_0)",
+ "pattern": "%$uslsl1$shift" },
+ "children": { "Mask Guard": [ { "header": "Split", "tactic": "Wp.split",
+ "params": {},
+ "select": { "select": "clause-goal",
+ "target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
+ "pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
+ "children": { "Goal 1/3": [ { "header": "Definition",
+ "tactic": "Wp.unfold",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 2,
+ "kind": "have",
+ "target": "(is_uint32 us_0)",
+ "pattern": "is_uint32$us" },
+ "children":
+ { "Unfold 'is_uint32'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/3": [ { "header": "Range",
+ "tactic": "Wp.range",
+ "params":
+ { "inf": 0,
+ "sup": 31 },
+ "select":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "children":
+ { "Lower 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 1":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 2":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 3":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 4":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 5":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 6":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 7":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 8":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 9":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 10":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 11":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 12":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 13":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 14":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 15":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 16":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 17":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 20":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 21":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 22":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 23":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 24":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 25":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 26":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 27":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 28":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 29":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 30":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 3/3": [ { "header": "Instance",
+ "tactic": "Wp.instance",
+ "params":
+ { "P1":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "P2": null,
+ "P3": null,
+ "P4": null,
+ "P5": null,
+ "P6": null,
+ "P7": null,
+ "P8": null,
+ "P9": null,
+ "P10": null },
+ "select":
+ { "select": "clause-goal",
+ "target": "exists i_0:int. ((lsl 1 i_0)=(lsl 1 shift_0)) /\\ (0<=i_0)",
+ "pattern": "\\Elsl011$shift" },
+ "children":
+ { "Witness":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ],
+ "Mask": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
new file mode 100644
index 00000000000..0232433c576
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
@@ -0,0 +1,14 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "us_0 mod 256", "pattern": "%$us256" },
+ "children": { "Mask Guard": [ { "header": "Definition",
+ "tactic": "Wp.unfold", "params": {},
+ "select": { "select": "clause-step",
+ "at": 0, "kind": "have",
+ "target": "(is_uint16 us_0)",
+ "pattern": "is_uint16$us" },
+ "children": { "Unfold 'is_uint16'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Mask": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
new file mode 100644
index 00000000000..dd1cd3edf7d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -0,0 +1,79 @@
+# frama-c -wp [...]
+[kernel] Parsing modmask.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp:script:allgoals]
+ Lemma and_modulo_u:
+ Prove: let x_0 = (lsl 1 shift_0) in
+ (0<=shift_0) -> (shift_0<=31) -> (is_uint32 us_0)
+ -> ((us_0 mod x_0)=(land us_0 (x_0-1)))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Lemma and_modulo_us_255:
+ Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-0 (generated):
+ Let x = lsl(1, shift_0).
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: (0 <= us_0) /\ (0 < x) /\ (exists i : Z. (lsl(1, i) = x) /\ (0 <= i)).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
+ Assume { Have: is_uint16(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_us_255 subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 <= us_0.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-3 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: 0 < lsl(1, shift_0).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_check_lemma_and_modulo_u subgoal:
+
+ Goal Wp.Tactical.typed_check_lemma_and_modulo_u-4 (generated):
+ Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
+ Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_u : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 0
+ Script: 2
+[wp] Updated session with 2 new valid scripts.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
new file mode 100644
index 00000000000..7d2e4b041e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
@@ -0,0 +1,162 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(land us_0 ((lsl 1 shift_0)-1))",
+ "pattern": "land$us+-1lsl1$shift" },
+ "children": { "Mod Guard": [ { "header": "Split", "tactic": "Wp.split",
+ "params": {},
+ "select": { "select": "clause-goal",
+ "target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
+ "pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
+ "children": { "Goal 1/3": [ { "header": "Definition",
+ "tactic": "Wp.unfold",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 2,
+ "kind": "have",
+ "target": "(is_uint32 us_0)",
+ "pattern": "is_uint32$us" },
+ "children":
+ { "Unfold 'is_uint32'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/3": [ { "header": "Range",
+ "tactic": "Wp.range",
+ "params":
+ { "inf": 0,
+ "sup": 31 },
+ "select":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "children":
+ { "Lower 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 0":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 1":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 2":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 3":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 4":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 5":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 6":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 7":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 8":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 9":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 10":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 11":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 12":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 13":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 14":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 15":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 16":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 17":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 20":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 21":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 22":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 23":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 24":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 25":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 26":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 27":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 28":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 29":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 30":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 31":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 3/3": [ { "header": "Instance",
+ "tactic": "Wp.instance",
+ "params":
+ { "P1":
+ { "select": "inside-goal",
+ "occur": 0,
+ "target": "shift_0",
+ "pattern": "$shift" },
+ "P2": null,
+ "P3": null,
+ "P4": null,
+ "P5": null,
+ "P6": null,
+ "P7": null,
+ "P8": null,
+ "P9": null,
+ "P10": null },
+ "select":
+ { "select": "clause-goal",
+ "target": "exists i_0:int. ((lsl 1 i_0)=(lsl 1 shift_0)) /\\ (0<=i_0)",
+ "pattern": "\\Elsl011$shift" },
+ "children":
+ { "Witness":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ],
+ "Mod": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
new file mode 100644
index 00000000000..a56490bac7a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
@@ -0,0 +1,14 @@
+[ { "header": "Mod-Mask", "tactic": "Wp.modmask",
+ "params": { "Wp.modmask.revert": false },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(land 255 us_0)", "pattern": "land255$us" },
+ "children": { "Mod Guard": [ { "header": "Definition",
+ "tactic": "Wp.unfold", "params": {},
+ "select": { "select": "clause-step",
+ "at": 0, "kind": "have",
+ "target": "(is_uint16 us_0)",
+ "pattern": "is_uint16$us" },
+ "children": { "Unfold 'is_uint16'":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Mod": [ { "prover": "qed", "verdict": "valid" } ] } } ]
--
GitLab