verifier: provides conditioned on match (bytecodealliance#181)

Updates the semantics of partial term specs such that the provides are
conditioned on a match, when present.

Until taking priorities into account, this has not mattered since all
matches are assumed to happen and therefore the provides is assumed to
apply also. However, without this change the logic for negated
extractors is wrong, since the provides is assumed even when the
extractor match is negated.

Updates bytecodealliance#128

cranelift/isle/veri/veri/filetests/pass/provide_only_if_match.isle

@@ -0,0 +1,38 @@
+; Test case that the provides of a partial function are assumed only on match.
+;
+; Contrived regression test for incorrect extractor semantics.
+
+; 8-bit value type
+(type Value (primitive Value))
+(model Value (type (bv 8)))
+
+; Coin flip result.
+(type Coin (enum Heads Tails))
+
+; Top-level test term selects a result based on parity.
+(decl test (Value) Coin)
+(spec (test v) (provide
+        (= result
+            (if (= (extract 0 0 v) #b1)
+                (Coin.Heads)
+                (Coin.Tails)
+            )
+        )
+    )
+)
+
+; Contrived extractor matches on odd and provides it must be 73.
+(decl odd73 () Value)
+(extern extractor odd73 odd73)
+(spec (odd73)
+    (match (= (extract 0 0 result) #b1))
+    (provide (= result #x41))
+)
+
+; Lowering to heads when odd73 matches should still be correct.
+(rule test_odd73_heads 1 (test (odd73)) (Coin.Heads))
+
+; Accounting for priority should negate the matches of odd73, but not the
+; provides.
+(rule test_tails (test v) (Coin.Tails))
+(attr rule test_tails (veri priority))

cranelift/isle/veri/veri/src/veri.rs

@@ -1151,9 +1151,15 @@ impl<'a> ConditionsBuilder<'a> {
         // Partial function.
         // REVIEW(mbm): pin down semantics for partial function specifications.
         if let Domain::Partial(p) = domain {
+            // Matches describe when the function applies.
             let all_matches = self.all(matches);
             let eq = self.exprs_equal(p, all_matches);
             self.conditions.assumptions.push(eq);
+
+            // Provides are conditioned on the match.
+            let all_provides = self.all(provides);
+            let provide = self.dedup_expr(Expr::Imp(all_matches, all_provides));
+            provides = vec![provide];
         } else if !matches.is_empty() {
             bail!("spec matches on non-partial function");
         }