[//]: # "Copyright Amazon.com Inc. or its affiliates. All Rights Reserved."
[//]: # "SPDX-License-Identifier: CC-BY-SA-4.0"
Welcome!
We're going to take you through the process of implementing a simple function
to parse an Amazon Resource Name (ARN) string
in the verification-aware programming language Dafny.
We're also going to use the Duvet code quality tool
to ensure we comply with a human-readable specification of correctness.
## Step 0
First let's spin up a development environment with all the dependencies we'll need.
Click the button below to open this repository in a GitPod workspace.
You'll want to open it in a new tab
so you can come back to the next step once it finishes starting up.
If you are not already signed in as a GitHub user,
you will be prompted to authenticate through GitHub.
[](https://gitpod.io/#https://github.com/aws-samples/how-to-write-more-correct-software-workshop)
If you are prompted to choose your IDE, select "Visual Studio Code for the Web".
If GitPod doesn't work for whatever reason,
alternatives are documented [here](./environment-alternatives.md).
This workshop is not a race,
and there is no test at the end.
We will walk you through everything
so take take time to read through everything.
## Step 1
The `exercises/start` directory contains our initial state,
with a few files to get you started.
In VS Code, open the file `exercises/start/src/AwsKmsArnParsing.dfy`.
You should see:
```dafny
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: MIT-0
include "../../../dafny-helpers/include.dfy"
module {:options "-functionSyntax:4"} AwsKmsArnParsing {
import opened Wrappers
import opened Util
}
```
You will also see the Dafny extension automatically download Dafny for you,
if this is the first time you've opened a Dafny source file.
There's no need to understand the details of what's already in the file,
but if you are keen you can read more [here](#notes-on-the-initial-state).
## Step 2
Since we are dealing with correct software,
we need a definition of correctness!
We have given you a specification.
This has been lightly edited from the [AWS Encryption SDK](https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/aws-kms/aws-kms-key-arn.md)
for this workshop. This is no made-up problem we're solving!
Currently `duvet` is optimized to handle RFC style (ITEF) files.
We have converted the markdown specification into this format for you.
Soon, `duvet` will support markdown directly.
`duvet` can read text documents
and extract MUST/SHOULD ([RFC-2119](https://datatracker.ietf.org/doc/html/rfc2119) normative language) statements as requirements.
`duvet` will keep track of these requirements for us.
It will help us account for every requirement,
and ask us to provide some evidence that our implementation of the requirements are correct.
You will see how this works in more detail later.
In VS Code [open a terminal](https://code.visualstudio.com/docs/terminal/basics) and enter:
```bash
cd exercises/start
````
You can also right-click the `exercises/start` folder and click "Open in Integrated Terminal".
Now let's extract the requirements and run a report.
We have made nice `make` targets for you.
The `make duvet_report` will fail.
This is expected because we have not implemented anything.
```bash
make duvet_extract
make duvet_report
```
The second command fails because we have not even started.
There will now be a `compliance_report.html` report in the `start` folder.
Right-click it and select "Open with Live Server",
which should open the page in your browser
(in a separate tab if you are using the web version of VS Code).
If you don't see a new tab, check to see if you have blocked pop-ups.
If you click on the `aws-kms-key-arn` link,
you will see that we have a total of 20 requirements
for our `aws-kms-key-arn` specification.
This report came from `aws-kms-key-arn.txt`.
Click on the "aws-kms-key-arn" link and you can see details on these requirements.
We will start on section `2.5` so go ahead
and click on one of the `2.5` links in the left-most column
and take a minute to look at this part of the specification
and how it breaks down into a checklist.
## Step 3
Since we are going to be parsing strings,
we need some containers to put the parts of the strings in.
Paste the following code into the `AwsKmsArnParsing` module
and then we will go over what it means.
Assuming you are reading these steps on GitHub,
there should be a handy hidden copy button
in the top-right corner of each code snippet for your convenience and delight.
Unless we say otherwise, each time we give you a snippet like this,
go ahead and paste it under the imports.
You shouldn't see any errors,
again unless we say otherwise.
If you run into problems please
[cut us an issue](https://github.com/aws-samples/how-to-write-more-correct-software-workshop/issues/new)!
```dafny
datatype AwsArn = AwsArn(
nameonly arnLiteral: string,
nameonly partition: string,
nameonly service: string,
nameonly region: string,
nameonly account: string,
nameonly resource: AwsResource
)
datatype AwsResource = AwsResource(
nameonly resourceType: string,
nameonly value: string
)
predicate ValidAwsArn?(arn:AwsArn)
predicate ValidAwsResource?(resource:AwsResource)
predicate AwsKmsArn?(arn:AwsArn)
predicate AwsKmsResource?(resource:AwsResource)
```
A `datatype` is an immutable container.
They are used to organize data.
We will add properties to them to hold our strings.
To the left of the `=` is the name of the `datatype`, which can be used as a type.
To the right of the `=` are the `datatype`'s constructors.
In this case, we have only one.
Later we will have more.
Much like other languages,
every argument given to a `datatype` constructor
is a property.
This means that if the variable `obj` is an `AwsArn`
then `obj.service` is a `string`.
`nameonly` forces callers to use named parameters
as opposed to positional parameters.
This makes the call more verbose,
but also makes it much more readable.
You are not required to use it
in your code,
but we highly recommend it.
What is a `predicate` and what's the deal with that `?` at the end?
A `predicate` is a function that returns a `boolean`.
It is syntactic sugar for `function ValidAwsArn?(arn: AwsArn): bool`.
Generally such functions ask a question.
For example "Is this AwsArn `arn` a valid AwsArn?".
Since `?` is a perfectly good character for a name in Dafny,
it is often added to a `predicate`.
Dafny is perfectly happy with constructs that have no body.
We will use this later.
## Step 4
Now we have some containers.
Let's talk about the correct values for these containers.
Replace the current definitions of the bodiless `predicate`s
with the following code.
```dafny
predicate ValidAwsArn?(arn:AwsArn)
{
&& arn.arnLiteral == "arn"
&& 0 < |arn.partition|
&& 0 < |arn.service|
&& 0 < |arn.region|
&& 0 < |arn.account|
&& ValidAwsResource?(arn.resource)
}
predicate ValidAwsResource?(resource:AwsResource)
{
&& 0 < |resource.value|
}
predicate AwsKmsArn?(arn:AwsArn)
{
&& ValidAwsArn?(arn)
&& arn.service == "kms"
&& AwsKmsResource?(arn.resource)
}
predicate AwsKmsResource?(resource:AwsResource)
{
&& ValidAwsResource?(resource)
&& (
|| resource.resourceType == "key"
|| resource.resourceType == "alias"
)
}
```
We are checking the `AwsArn` container
to see if it is correct.
We can read `ValidAwsArn?` as:
The arnLiteral MUST be the string "arn";
the partition, service, region, and account
MUST NOT be empty strings;
and finally the resource MUST be a correct AwsResource.
A `predicate` is a kind of function.
You will note that there is no `;`.
The return value for any `predicate` or `function`
is just the value of the function's body.
The leading token, `&&`, is just sugar.
Leading boolean operators like this
lets you reorder things easily.
It may look strange at first,
but leading tokens like this grow on you.
`string`s in Dafny are sequences of characters.
Surrounding a sequence with `|` will return the length (cardinality) of a sequence.
So `|arn.partition|` is simply the length of the string.
Go back and take a look at our report.
Does this seem to capture most of what the specification says makes a valid AWS KMS ARN?
## Step 5
Many languages have types similar to Dafny's `datatype`,
albeit not always immutable.
These types already contribute some progress towards correctness.
After all, you can't put a number into a string.
A subset type in Dafny lets us encapsulate the correctness we defined
in a `predicate` into a new, more precise type.
We can then reason about this new type statically.
If most types represent the basic shape of your data,
then Dafny's subset types are paintings
full of light, shadow, and color.
As we will see,
to return a subset type we will need to prove
that the `datatype` has been constructed correctly.
But after that the correctness is baked into the subset type.
Let's create one!
```dafny
type AwsKmsArn = arn: AwsArn | AwsKmsArn?(arn) witness *
```
1. `type AwsKmsArn`
tells Dafny we want to define a type named `AwsKmsArn`.
1. `arn: AwsArn` means that base type is `AwsArn`.
To define the constraints of this subset type,
we need a symbol of the base type to use when defining these constraints.
1. `| AwsKmsArn?(arn)` means that if we pass the instance `arn`
to `AwsKmsArn?`, it MUST return `true`.
The `|` can be read as "such that".
This type can be read
"An `AwsKmsArn` is an `AwsArn` `arn` such that `AwsKmsArn?(arn)` is true".
1. `witness`:
In Dafny, some contexts only allow you to use a type
if you can prove at least one value of that type exists.
The `witness` clause is there to prove to Dafny
this is true, by providing a sample value.
In our case we don't need this.
`witness *` tells Dafny,
"Don't worry,
it doesn't matter whether a value
of this type actually exists."
Feel free to check out [witness clauses](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-witness)
in the reference manual for more details.
In the meantime,
let's create a subset type for `AwsKmsResource` as well:
```dafny
type AwsKmsResource = resource: AwsResource | AwsKmsResource?(resource) witness *
```
## Step 6
Ok! Let's get started.
Copy over these naive signatures.
```dafny
function ParseAwsKmsArn(identifier: string)
: (result: AwsKmsArn)
function ParseAwsKmsResource(identifier: string)
: (result: AwsKmsResource)
```
`function` is mostly what you expect.
However, `function`s in Dafny are more restrictive
than you are probably used to.
They are more like mathematical functions: 100% deterministic.
The can't mutate, use loops, or create objects.
These restrictions are important
because `function`s are the building blocks for proof.
They provide a good introduction to Dafny
and we won't run into these restrictions today.
`: (result: AwsKmsResource)`?
The first `:` tells Dafny "This is the return value".
By putting it in `()` we can give our return value a name
(i.e. `result`) and a type for this return value.
This lets us reference it in a postcondition or `ensures` clause.
Postconditions are things that MUST be true
about the result of the function.
## Step 7
Here is a naive implementation
to copy over.
Note that it is `':'` not `":"`:
the first is a character, the second is a string.
We have introduced the dreaded semicolon `;`,
but never fear, we are still just defining a pure expression!
This syntax is just a way of introducing names for sub-expressions.
You can read `var x := e; y` as "let `x` be `e` within `y`".
If you do this multiple times,
you end up with something that looks suspiciously like
a sequence of statements.
Ultimately the result of the function
is the expression following the last `;`.
Replace the `ParseAwsKmsArn` function with this code.
This code will give you errors, which we will go over.
```dafny
function ParseAwsKmsArn(identifier: string)
: (result: AwsKmsArn)
{
var components := Split(identifier, ':');
var resource := ParseAwsKmsResource(components[5]);
var arn := AwsArn(
arnLiteral := components[0],
partition := components[1],
service := components[2],
region := components[3],
account := components[4],
resource := resource
);
arn
}
```
Now we see two errors!
`index out of range` on `components[5]`, and
`value does not satisfy the subset constraints of 'AwsKmsArn'`
on the final `arn`.
Dafny does not believe us that `6 == |components|`.
That is, that there are at least 5 `:` in `identifier`.
This makes sense to us.
We know nothing about `identifier`.
What do we know?
How can we ask Dafny about such things?
`assert` statements are how we declare what we believe is true
at a particular point in the code.
But Dafny will also tell you whether it agrees.
Most languages have a way for you to do "console log debugging"
where you make changes, run the code, and check the output.
`assert` is a way to do something similar in Dafny.
However, instead of checking a specific value at runtime,
Dafny will check them all before you ever execute your code.
An `assert` is an error unless Dafny can deduce
that it is impossible for the expression to be false.
The `Split` function splits a string into multiple strings
according to a delimiter character,
so `Split("a:b:c") == ["a", "b", "c"]` for example.
In particular, `Split` will return a single element
if the character does not appear in the string.
So `Split("no colon", ':') == ["no colon"]`.
After the `Split` try adding
```dafny
assert Split("no colon", ':') == ["no colon"];
```
You should **not** see an error on this assert,
which is Dafny telling us that this is indeed true!
This means we can
```dafny
assert 1 <= |components|;
```
and sure enough Dafny will believe us.
But any larger number, say `assert 2 <= |components|;`,
Dafny will disagree.
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`.