With `--allow-sorry`, warn on missing proofs, not synthesized `sorry` tactic

Currently, when running with `--allow-sorry`, Hermes will automatically replace any missing proof with the `sorry` tactic, e.g.:

```rust
/// ```hermes, spec
/// ensures ret.val > 0
/// ```
fn foo() -> u32 { 1 }
```

Combined with Lean's warnings about the `sorry` tactic, this results in confusing warnings:

```text
⚠ declaration uses `sorry`
╭─[[PROJECT_ROOT]/src/lib.rs:10:8]
9 │ /// ```
10 │ pub fn foo() -> u32 { 1 }
· ──┬─
· ╰── here
╰────
```

We should fix this. One approach would be, when we encounter a missing proof, to lower to our own tactic which is *equivalent* to `sorry` but not *literally* `sorry`. This will ensure that Lean doesn't generate a warning for it. We can then generate our *own* native warning directly from Hermes.