Aside
Note: Some clever among you may try
```dafny
assert Split("a:b", ':') == ["a", "b"];
```
Dafny will not unwind every possible fact.
This is why I say that Dafny does not believe us.
These kinds of verification errors are not saying "This is false",
they are saying "I can't prove that *is* true".
In fact we can convince Dafny by adding
```dafny
assert Split("a:b", ':')[0] == "a";
```
before the above `assert`.
## Step 8
Ok, so what do we do if there are not enough `:` in `identifier`?
Dafny does not have the ability to `throw` an exception.
The return type in Dafny is a contract or postcondition.
That means that with the current function signature,
we MUST return an `AwsKmsArn` no matter what.
What we need is a way to express failure.
Dafny has a way to do this.
You can read about [failure compatible types here](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-update-failure)
if you like.
But we will go over everything you need.
First we need a type that can express
the difference between `Success` and `Failure`.
In the `Wrappers` module defined in the `Wrappers.dfy` file,
the `Result` type does exactly this.
It takes 2 type parameters.
One for the `Success` and the other for `Failure`[^monad]
[^monad]: If this sounds to you like a monad,
then congratulations it is pretty close.
If you have no idea what a monad is,
then [congratulations](https://en.wikipedia.org/wiki/Monad_(functional_programming)) you are one of the [lucky 10,000](https://xkcd.com/1053/)!
Update the existing function.
The difference is the return value `: (result: Result