From ddbcfaf36bd5a36b7257e28e5818dadfcd53ee8a Mon Sep 17 00:00:00 2001 From: urikirsh Date: Wed, 24 Jul 2024 21:18:41 +0300 Subject: [PATCH] reworked implication structure cases, added --- docs/prover/checking/sanity.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/docs/prover/checking/sanity.md b/docs/prover/checking/sanity.md index 4933d601..b91ea6ee 100644 --- a/docs/prover/checking/sanity.md +++ b/docs/prover/checking/sanity.md @@ -112,7 +112,7 @@ rule tautology { Since every `uint` satisfies the assertion, the assertion is tautological, which may indicate an error in the specification. -The tautology check will add a node per `assert` or `satisfy` statement to each rule. The nodes are named with the prefix `assert_not_tautological_` followed by a numerical ID. For example, the rule report for the above `tautology` rule will look like this: +The tautology check will add a node per `assert` or `satisfy` statement to each rule. The nodes are named with the prefix `assert_not_tautological_`. For example, the rule report for the above `tautology` rule will look like this: ![Screenshot of assert tautology subrule](tautology_subrule.png) @@ -189,9 +189,13 @@ The assertion structure check tries to prove some complex logical statements by breaking them into simpler parts. The following situations are reported by the assertion structure check: -1. `assert p => q;` is reported as a sanity violation if `p` is false whenever the - assertion is reached (in which case the simpler assertion `assert !p;` more - clearly describes the situation). In that case the node named `assertion_left_operand_check_` followed by a numerical ID will have a yellow icon. Sanity will also be violated if `q` is always true (in which case `assert q;` is a clearer alternative). In that case the node named `assertion_left_operand_check_` followed by a numerical ID will have a yellow icon. +1. `assert p => q;` is reported as a sanity violation if whenever the assertion is reached: + + 1. `p` is always false. In this case, `q` is never checked. A simpler way to write this assertion is `assert !p;`. The node named `assertion_left_operand_check_` will have a yellow icon. + + 2. `p` is always true. A simpler way to write this assertion is `assert q;`. The node named `assertion_left_operand_check_` will have a yellow icon. + + 3. `q` is always true. A simpler way to write this assertion is `assert q;`. The node named `assertion_right_operand_check_`. ![Screenshot of sanity structure for implication](implication_sanity_structure.png) @@ -227,7 +231,7 @@ rule require_redundant { In this example, the second requirement is redundant, since any `x` greater than 3 will also be greater than 2. -The redundant require check will add a node per `require` statement to each rule. The nodes are named with the prefix `require_not_redundant_` followed by a numerical ID. +The redundant require check will add a node per `require` statement to each rule. The nodes are named with the prefix `require_not_redundant_`. ![Screenshot of rule report showing a redundant require check](sanity-icons.png)