basic option + product instances for isValid

tools/hermes/src/Hermes.lean

@@ -45,6 +45,15 @@ class IsValid (α : Type) where
 instance (priority := low) defaultIsValid {α : Type} : IsValid α where
   isValid _ := True
 
+instance [IsValid α] [IsValid β] : IsValid (α × β) where
+  isValid
+    | (a, b) => IsValid.isValid a ∧ IsValid.isValid b
+
+instance [IsValid α] : IsValid (Option α) where
+  isValid
+    | none => True
+    | some a => IsValid.isValid a
+
 -- A tactic that queries the environment for the `Hermes.allow_sorry` axiom.
 -- If it exists, runs `sorry`. If not, fails with the provided error string.
 elab "eval_allow_sorry_or_fail" err:term : tactic => do

tools/hermes/tests/fixtures/option_is_valid/expected.stderr

@@ -0,0 +1,3 @@
+[External Error] generated/OptionIsValidOptionIsValid<HASH>/OptionIsValidOptionIsValid<HASH>.lean: could not synthesize default value for field 'h_ret_is_valid' of 'option_is_valid.invalid_option.Post' using tactics
+[External Error] generated/OptionIsValidOptionIsValid<HASH>/OptionIsValidOptionIsValid<HASH>.lean: This error comes from the implicit `simp_all` proof for `h_ret_is_valid`. Lean cannot automatically prove that this value satisfies the `isValid` type invariant. Consider providing a manual proof via `proof (h_ret_is_valid)`.
+Error: Lean verification failed

tools/hermes/tests/fixtures/option_is_valid/hermes.toml

@@ -0,0 +1,9 @@
+description = """
+Purpose: Verifies that `isValid` recurses through `Option`.
+Behavior: An invalid `Some Positive` return value should fail verification.
+"""
+
+[test]
+stderr_file = "expected.stderr"
+args = ["verify", "--unsound-allow-is-valid"]
+expected_status = "failure"

tools/hermes/tests/fixtures/option_is_valid/source/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "option_is_valid"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

tools/hermes/tests/fixtures/option_is_valid/source/src/lib.rs

@@ -0,0 +1,12 @@
+/// ```hermes
+/// isValid self := self.x > 0
+/// ```
+pub struct Positive {
+    pub x: u32,
+}
+
+/// ```hermes
+/// ```
+pub fn invalid_option() -> Option<Positive> {
+    Some(Positive { x: 0 })
+}

tools/hermes/tests/fixtures/option_is_valid_success/hermes.toml

@@ -0,0 +1,8 @@
+description = """
+Purpose: Verifies that `isValid` recurses through `Option`.
+Behavior: A valid `Some Positive` return value should verify successfully.
+"""
+
+[test]
+args = ["verify", "--unsound-allow-is-valid"]
+expected_status = "success"

tools/hermes/tests/fixtures/option_is_valid_success/source/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "option_is_valid_success"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

tools/hermes/tests/fixtures/option_is_valid_success/source/src/lib.rs

@@ -0,0 +1,18 @@
+/// ```hermes
+/// isValid self := self.x > 0
+/// ```
+pub struct Positive {
+    pub x: u32,
+}
+
+/// ```hermes
+/// proof (h_ret_is_valid):
+///   have h_ret : some { x := 1#u32 } = ret := by
+///     simpa [valid_option] using h_returns
+///   rw [← h_ret]
+///   simp [Hermes.IsValid.isValid]
+///   decide
+/// ```
+pub fn valid_option() -> Option<Positive> {
+    Some(Positive { x: 1 })
+}

tools/hermes/tests/fixtures/product_is_valid/expected.stderr

@@ -0,0 +1,3 @@
+[External Error] generated/ProductIsValidProductIsValid<HASH>/ProductIsValidProductIsValid<HASH>.lean: could not synthesize default value for field 'h_ret_is_valid' of 'product_is_valid.invalid_pair.Post' using tactics
+[External Error] generated/ProductIsValidProductIsValid<HASH>/ProductIsValidProductIsValid<HASH>.lean: This error comes from the implicit `simp_all` proof for `h_ret_is_valid`. Lean cannot automatically prove that this value satisfies the `isValid` type invariant. Consider providing a manual proof via `proof (h_ret_is_valid)`.
+Error: Lean verification failed

tools/hermes/tests/fixtures/product_is_valid/hermes.toml

@@ -0,0 +1,9 @@
+description = """
+Purpose: Verifies that `isValid` recurses through Lean product types.
+Behavior: An invalid `(Positive, u32)` return value should fail verification.
+"""
+
+[test]
+stderr_file = "expected.stderr"
+args = ["verify", "--unsound-allow-is-valid"]
+expected_status = "failure"

tools/hermes/tests/fixtures/product_is_valid/source/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "product_is_valid"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

tools/hermes/tests/fixtures/product_is_valid/source/src/lib.rs

@@ -0,0 +1,12 @@
+/// ```hermes
+/// isValid self := self.x > 0
+/// ```
+pub struct Positive {
+    pub x: u32,
+}
+
+/// ```hermes
+/// ```
+pub fn invalid_pair() -> (Positive, u32) {
+    (Positive { x: 0 }, 0)
+}

tools/hermes/tests/fixtures/product_is_valid_success/hermes.toml

@@ -0,0 +1,8 @@
+description = """
+Purpose: Verifies that `isValid` recurses through Lean product types.
+Behavior: A valid `(Positive, u32)` return value should verify successfully.
+"""
+
+[test]
+args = ["verify", "--unsound-allow-is-valid"]
+expected_status = "success"

tools/hermes/tests/fixtures/product_is_valid_success/source/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "product_is_valid_success"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]

tools/hermes/tests/fixtures/product_is_valid_success/source/src/lib.rs

@@ -0,0 +1,18 @@
+/// ```hermes
+/// isValid self := self.x > 0
+/// ```
+pub struct Positive {
+    pub x: u32,
+}
+
+/// ```hermes
+/// proof (h_ret_is_valid):
+///   have h_ret : ({ x := 1#u32 }, 0#u32) = ret := by
+///     simpa [valid_pair] using h_returns
+///   rw [← h_ret]
+///   simp [Hermes.IsValid.isValid]
+///   decide
+/// ```
+pub fn valid_pair() -> (Positive, u32) {
+    (Positive { x: 1 }, 0)
+}