From 850802bde814935e64afb5b748b08a1cf56c73a8 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 12 Jan 2024 12:04:14 -0800 Subject: [PATCH] fix: Typos and truncated code snippet in standard libraries blog (#31) The truncated code snippet was due to the `inline-dafny` implementation only understanding source files where the code is contained in an explicit module, since it assumes any line that is literally "}\n" is the end of a module and hence the terminator for the snippet. I indented all of the manual snippets to align with the corrected one at the end. Also corrected a couple of typos and included the sample input (thanks @stefan-aws!) --- _includes/standard-libraries.html | 240 +++++++++++---------- assets/mdk/standard-libraries.mdk | 146 +++++++------ assets/src/standard-libraries/solution.dfy | 54 +++-- 3 files changed, 234 insertions(+), 206 deletions(-) diff --git a/_includes/standard-libraries.html b/_includes/standard-libraries.html index 5b5095a..7b453a2 100644 --- a/_includes/standard-libraries.html +++ b/_includes/standard-libraries.html @@ -391,9 +391,9 @@

Now for the actual code. Let's start from the bottom-up: we're clearly going to need a function to extract the calibration value as a number from a single line of text.

-
function CalibrationValue(line: string): nat {
-  // ...
-}
+
  function CalibrationValue(line: string): nat {
+    // ...
+  }

How do we find the first and last digits?

Sequences and Wrappers

Having a look at the top-level index of Dafny standard libraries, @@ -460,50 +460,50 @@ For this exercise I'm just using import statements so it's more obvious when we're using things from the standard libraries.

-
import Std.Collections.Seq
+
  import Std.Collections.Seq
 
-function CalibrationValue(line: string): nat {
-  var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
-  var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
+  function CalibrationValue(line: string): nat {
+    var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
+    var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
 
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  // Still need to parse the result as a number...
-}

+    // Still need to parse the result as a number...
+  }

Progress! We'll figure out what to pass for the second arguments on the first two lines in a moment. First, how do we convert our resultAsString to a number, more specifically a nat? This is more specifically an operation on strings rather than generic sequences. That means now we can open our Std.Strings present, and see that it contains a shiny new ToNat function!

-
import Std.Collections.Seq
-import Std.Strings
+
  import Std.Collections.Seq
+  import Std.Strings
 
-function CalibrationValue(line: string): nat {
-  var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
-  var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
+  function CalibrationValue(line: string): nat {
+    var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
+    var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
 
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Strings.ToNat(resultStr)
-}

+    Strings.ToNat(resultAsString)
+  }

Even better, digging into the implementation of ToNat leads us to what we need to plug the holes we skipped over: the Strings.DecimalConversion.IsDigitChar predicate tells us if a character is a digit.

-
import Std.Collections.Seq
-import Std.Strings
-import Std.Strings.DecimalConversion
+
  import Std.Collections.Seq
+  import Std.Strings
+  import Std.Strings.DecimalConversion
 
-function CalibrationValue(line: string): nat {
-  var firstDigitIndex := Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
-  var lastDigitIndex := Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
+  function CalibrationValue(line: string): nat {
+    var firstDigitIndex := Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
+    var lastDigitIndex := Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
 
-  // Error: incorrect type for selection into string (got Option<nat>)
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    // Error: incorrect type for selection into string (got Option<nat>)
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Strings.ToNat(resultAsString)
-}

+    Strings.ToNat(resultAsString)
+  }

Before we pat ourselves on the back too hard, though, we notice this program doesn't typecheck yet: firstDigitIndex and lastDigitIndex are not plain nat values but Option<nat> values. @@ -518,19 +518,19 @@ Let's change our return type, change the two regular := assignment operators to elephants instead, and wrap up our result as an Option<nat> so it matches our new return type:

-
import Std.Collections.Seq
-import Std.Strings
-import Std.Strings.DecimalConversion
-import Std.Wrappers
+
  import Std.Collections.Seq
+  import Std.Strings
+  import Std.Strings.DecimalConversion
+  import Std.Wrappers
 
-function CalibrationValue(line: string): Wrappers.Option<nat> {
-  var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
-  var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
+  function CalibrationValue(line: string): Wrappers.Option<nat> {
+    var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
+    var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
 
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Wrappers.Some(Strings.ToNat(resultAsString))
-}

+    Wrappers.Some(Strings.ToNat(resultAsString))
+  }

Now if either attempt to find a digit fails, the execution of the function body will immediately stop, and that failure will become the result of the whole function. @@ -545,7 +545,7 @@ and not something like a Wrappers.Option<nat> or a Wrappers.Result<nat, string>, because it always succeeds in parsing the string.

-

How does Dafny know that resultStr is always parsable as a non-negative integer? +

How does Dafny know that resultAsString is always parsable as a non-negative integer? Because of the post-conditions of Seq.IndexByOption and Seq.LastIndexByOption, Dafny actually knows that they return the indexes of elements that satisfy the “by” predicate, and therefore deduces that [line[firstDigitIndex], line[lastDigitIndex]] @@ -563,14 +563,14 @@ Here's our first attempt at a reusable utility for reading Advent of Code puzzle input (because after all we have another month's worth of puzzles to solve!)

-
// Just the imports we need for this snippet.
-import Std.FileIO
-import Std.Wrappers
+
  // Just the imports we need for this snippet.
+  import Std.FileIO
+  import Std.Wrappers
 
-method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
-  // Error: incorrect return type for method out-parameter 'res'
-  input := FileIO.ReadBytesFromFile("input.txt");
-}

+  method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
+    // Error: incorrect return type for method out-parameter 'res'
+    input := FileIO.ReadBytesFromFile("input.txt");
+  }

Note that FileIO.ReadBytesFromFile is a method rather than a function, and so ReadPuzzleInput has to be as well. A function has to behave like a pure mathematical function @@ -589,17 +589,17 @@ But let's pretend we're writing Real Code for the moment so I can show off the Std.Unicode library; hey you never know, later puzzles might have proper UTF8 content!

-
import Std.BoundedInts
-import Std.FileIO
-import Std.Unicode.UnicodeStringsWithUnicodeChar
-import Std.Wrappers
+
  import Std.BoundedInts
+  import Std.FileIO
+  import Std.Unicode.UnicodeStringsWithUnicodeChar
+  import Std.Wrappers
 
-method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
-  var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
-  
-  var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
-  input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
-}

+  method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
+    var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
+    
+    var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
+    input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
+  }

A few notes:

Sprinting to the finish

Now let's put it all together and write our main method:

-
method Main() {
-  var input :- expect ReadPuzzleInput();
+
  method Main() {
+    var input :- expect ReadPuzzleInput();
 
-  var lines := Seq.Split(s, '\n');
+    var lines := Seq.Split(s, '\n');
 
-  var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
+    var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
 
-  var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
-  print total, "\n";
-}

+    var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
+    print total, "\n";
+  }

We've used one more trick with failure-compatible types in this method: :- expect, a variation on the elephant operator to make “assign or halt” statements. ReadPuzzleInput returns a Result, but if it fails there's nothing more we can do @@ -650,87 +650,109 @@

MapWithResult is a short-circuiting variation of Map where the mapped function can fail.

-

If we put the sample input from the puzzle description into input.txt +

Let's put the sample input from the puzzle description into input.txt so we can try it out (not the actual puzzle input - I draw the line at publishing the answer in this blog post, -you're just going to have to run the solution yourself to get that!), -we can run our project and get… +you're just going to have to run the solution yourself to get that!) +

+
1abc2
+pqr3stu8vwx
+a1b2c3d4e5f
+treb7uchet
+

Now we can run our project and get…

-
% dafny run dfyconfig.toml
+
% dafny run dfyconfig.toml
 
 Dafny program verifier finished with 3 verified, 0 errors
 142

-
Huzzah! We have a working solution to the first puzzle in less than 40 lines of Dafny code
+
Huzzah! We have a working solution to the first puzzle in less than 40 lines of Dafny code
 (see below for the complete program),
 all thanks to the Dafny standard libraries.
 

 
 
 
-
import Std.BoundedInts
-import Std.Collections.Seq
-import Std.FileIO
-import Std.Strings
-import Std.Strings.DecimalConversion
-import Std.Unicode.UnicodeStringsWithUnicodeChar
-import Std.Wrappers
+
  import Std.BoundedInts
+  import Std.Collections.Seq
+  import Std.FileIO
+  import Std.Strings
+  import Std.Strings.DecimalConversion
+  import Std.Unicode.UnicodeStringsWithUnicodeChar
+  import Std.Wrappers
+
+  method Main() {
+    var input :- expect ReadPuzzleInput();
+
+    var lines := Seq.Split(input, '\n');
 
-method Main() {
-  var input :- expect ReadPuzzleInput();
+    var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
+
+    var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
+    print total, "\n";
+  }
+
+  method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
+    var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
+    var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
+    
+    input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
+  }
 
-  var lines := Seq.Split(input, '\n');
+  function CalibrationValue(line: string): Wrappers.Result<nat, string> {
+    var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
+    var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
 
-  var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
+    var resultStr := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
-  print total, "\n";
Looking back and looking ahead

-
The standard libraries are made possible by the recent support for
-Dafny build artifacts: 
+    Wrappers.Success(Strings.ToNat(resultStr))
+  }
Looking back and looking ahead

+
The standard libraries are made possible by the recent support for
+Dafny build artifacts: 
 compressed files containing the contents of an entire Dafny library along with metadata about how it was verified.
-These files use the extension .doo for Dafny Output Object1.
-They play much the same role as .jar files do for Java packages.
-Internally, the standard libraries are packaged up as multiple .doo files
+These files use the extension .doo for Dafny Output Object1.
+They play much the same role as .jar files do for Java packages.
+Internally, the standard libraries are packaged up as multiple .doo files
 and embedded as resources in the Dafny tool.
-When --standard-libraries is switched on,
-the appropriate set of .doo files are added as additional program source.
+When --standard-libraries is switched on,
+the appropriate set of .doo files are added as additional program source.
 

-
This means the standard library source isn't re-verified every time your verify your Dafny project,
+
This means the standard library source isn't re-verified every time your verify your Dafny project,
 but the tool checks to make sure the options they were previously verified with
 are compatible with the objects in your project.
-In particular, this means if you try to use them with the older unicode-char = false option,
-you'll get an explicit error right away,
+In particular, this means if you try to use them with the older unicode-char = false option,
+you'll get an explicit error right away,
 rather than potentially misusing code not meant for this mode.
 

-
As excited as I am about having standard libraries in Dafny,
-I've also been nervous about having them for a long time:
-I'd be sad in the future if anyone gave Dafny a pass
+
As excited as I am about having standard libraries in Dafny,
+I've also been nervous about having them for a long time:
+I'd be sad in the future if anyone gave Dafny a pass
 because its footprint had grown too bloated for their environment.
-Part of the reason the code is labelled as “standard libraries”, plural,
+Part of the reason the code is labelled as “standard libraries”, plural,
 is to hint at the fact that they may be split up into different packages in the future.
 Now that we have standard libraries in Dafny,
-we're also setting our sights on helping Dafny users create their own shared libraries
-and distributing them as pre-verified .doo files in the future,
+we're also setting our sights on helping Dafny users create their own shared libraries
+and distributing them as pre-verified .doo files in the future,
 so such libraries also get this layer of protection against misuse.
 

-
Another great improvement over the old dafny-lang/libraries repository
+
Another great improvement over the old dafny-lang/libraries repository
 is that the Dafny standard libraries are well-tested for all of the programming languages
-that Dafny currently compiles to: C#, Go, Python, Java and JavaScript.
+that Dafny currently compiles to: C#, Go, Python, Java and JavaScript.
 That means even libraries that depend on target language details
-such as Std.FileIO and Std.Concurrent
+such as Std.FileIO and Std.Concurrent
 are safe to use in multi-target Dafny projects.
-
Until next year

-
I'll leave this post at that, as I've got some catching up to do in the Advent of Code challenge before time runs out!
+
Until next year

+
I'll leave this post at that, as I've got some catching up to do in the Advent of Code challenge before time runs out!
 In the meantime, install Dafny 4.4, take the standard libraries for a test drive, 
-and feel free to cut an issue if you run into speed bumps.
+and feel free to cut an issue if you run into speed bumps.
 Even better, if you have your own spiffy reusable Dafny code you keep in your back pocket,
-create a pull request and get it into the standard libraries!
+create a pull request and get it into the standard libraries!
 

 

 

 
-

-
1.This is true, but the real reason for the name is a nod to the other Daphne from Scooby Doo.
-↩

+

+
1.This is true, but the real reason for the name is a nod to the other Daphne from Scooby Doo.
+↩

 
 
 
diff --git a/assets/mdk/standard-libraries.mdk b/assets/mdk/standard-libraries.mdk
index 0e519c9..1c1a16d 100644
--- a/assets/mdk/standard-libraries.mdk
+++ b/assets/mdk/standard-libraries.mdk
@@ -101,9 +101,9 @@ Now for the actual code. Let's start from the bottom-up:
 we're clearly going to need a function to extract the calibration value as a number from a single line of text.
 
 ```dafny
-function CalibrationValue(line: string): nat {
-  // ...
-}
+  function CalibrationValue(line: string): nat {
+    // ...
+  }
 ```
 
 How do we find the first and last digits?
@@ -177,16 +177,16 @@ For this exercise I'm just using `import` statements
 so it's more obvious when we're using things from the standard libraries.
 
 ```dafny
-import Std.Collections.Seq
+  import Std.Collections.Seq
 
-function CalibrationValue(line: string): nat {
-  var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
-  var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
+  function CalibrationValue(line: string): nat {
+    var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
+    var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
 
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  // Still need to parse the result as a number...
-}
+    // Still need to parse the result as a number...
+  }
 ```
 
 Progress! We'll figure out what to pass for the second arguments on the first two lines in a moment.
@@ -196,17 +196,17 @@ That means **now** we can open our `Std.Strings` present,
 and see that it contains a shiny new `ToNat` function!
 
 ```dafny
-import Std.Collections.Seq
-import Std.Strings
+  import Std.Collections.Seq
+  import Std.Strings
 
-function CalibrationValue(line: string): nat {
-  var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
-  var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
+  function CalibrationValue(line: string): nat {
+    var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
+    var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);
 
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Strings.ToNat(resultStr)
-}
+    Strings.ToNat(resultAsString)
+  }
 ```
 
 Even better, digging into the implementation of `ToNat` leads us to what we need
@@ -214,19 +214,19 @@ to plug the holes we skipped over:
 the `Strings.DecimalConversion.IsDigitChar` predicate tells us if a character is a digit.
 
 ```dafny
-import Std.Collections.Seq
-import Std.Strings
-import Std.Strings.DecimalConversion
+  import Std.Collections.Seq
+  import Std.Strings
+  import Std.Strings.DecimalConversion
 
-function CalibrationValue(line: string): nat {
-  var firstDigitIndex := Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
-  var lastDigitIndex := Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
+  function CalibrationValue(line: string): nat {
+    var firstDigitIndex := Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
+    var lastDigitIndex := Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
 
-  // Error: incorrect type for selection into string (got Option)
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    // Error: incorrect type for selection into string (got Option)
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Strings.ToNat(resultAsString)
-}
+    Strings.ToNat(resultAsString)
+  }
 ```
 
 Before we pat ourselves on the back too hard, though,
@@ -244,19 +244,19 @@ Let's change our return type, change the two regular `:=` assignment operators t
 and wrap up our result as an `Option` so it matches our new return type:
 
 ```dafny
-import Std.Collections.Seq
-import Std.Strings
-import Std.Strings.DecimalConversion
-import Std.Wrappers
+  import Std.Collections.Seq
+  import Std.Strings
+  import Std.Strings.DecimalConversion
+  import Std.Wrappers
 
-function CalibrationValue(line: string): Wrappers.Option {
-  var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
-  var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
+  function CalibrationValue(line: string): Wrappers.Option {
+    var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
+    var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);
 
-  var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Wrappers.Some(Strings.ToNat(resultAsString))
-}
+    Wrappers.Some(Strings.ToNat(resultAsString))
+  }
 ```
 
 Now if either attempt to find a digit fails,
@@ -273,7 +273,7 @@ That's why the return type of `ToNat` is just `nat`
 and not something like a `Wrappers.Option` or a `Wrappers.Result`,
 because it always succeeds in parsing the string.
 
-How does Dafny know that `resultStr` is always parsable as a non-negative integer?
+How does Dafny know that `resultAsString` is always parsable as a non-negative integer?
 Because of the post-conditions of `Seq.IndexByOption` and `Seq.LastIndexByOption`,
 Dafny actually **knows** that they return the indexes of elements that satisfy the "by" predicate,
 and therefore deduces that `[line[firstDigitIndex], line[lastDigitIndex]]`
@@ -294,14 +294,14 @@ Here's our first attempt at a reusable utility for reading Advent of Code puzzle
 (because after all we have another month's worth of puzzles to solve!)
 
 ```dafny
-// Just the imports we need for this snippet.
-import Std.FileIO
-import Std.Wrappers
-
-method ReadPuzzleInput() returns (input: Wrappers.Result) {
-  // Error: incorrect return type for method out-parameter 'res'
-  input := FileIO.ReadBytesFromFile("input.txt");
-}
+  // Just the imports we need for this snippet.
+  import Std.FileIO
+  import Std.Wrappers
+
+  method ReadPuzzleInput() returns (input: Wrappers.Result) {
+    // Error: incorrect return type for method out-parameter 'res'
+    input := FileIO.ReadBytesFromFile("input.txt");
+  }
 ```
 
 Note that `FileIO.ReadBytesFromFile` is a `method` rather than a `function`,
@@ -323,17 +323,17 @@ But let's pretend we're writing Real Code for the moment so I can show off the `
 hey you never know, later puzzles might have proper UTF8 content!
 
 ```dafny
-import Std.BoundedInts
-import Std.FileIO
-import Std.Unicode.UnicodeStringsWithUnicodeChar
-import Std.Wrappers
-
-method ReadPuzzleInput() returns (input: Wrappers.Result) {
-  var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
-  
-  var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
-  input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
-}
+  import Std.BoundedInts
+  import Std.FileIO
+  import Std.Unicode.UnicodeStringsWithUnicodeChar
+  import Std.Wrappers
+
+  method ReadPuzzleInput() returns (input: Wrappers.Result) {
+    var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
+    
+    var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
+    input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
+  }
 ```
 
 A few notes:
@@ -347,7 +347,7 @@ A few notes:
   This is a side effect of the Dafny standard libraries having multiple independent contributions from various
   projects, and you can expect future versions of Dafny to provide more versions of common utilities
   to make combining things a bit smoother.
-* `FromUTF8Checked` returns an `Option`, but `FileIO.ReadBytesFrom` returns a `Result, string>`.
+* `FromUTF8Checked` returns an `Option`, but `FileIO.File` returns a `Result, string>`.
   To unify with a common result type, we use `Option.ToResult` to convert the former value to a `Result`,
   which is a handy and common trick. See [the documentation for `Std.Wrappers`](https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std/Wrappers.md) for more details.
 
@@ -356,16 +356,16 @@ A few notes:
 Now let's put it all together and write our main method:
 
 ```dafny
-method Main() {
-  var input :- expect ReadPuzzleInput();
+  method Main() {
+    var input :- expect ReadPuzzleInput();
 
-  var lines := Seq.Split(s, '\n');
+    var lines := Seq.Split(s, '\n');
 
-  var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
+    var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
 
-  var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
-  print total, "\n";
-}
+    var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
+    print total, "\n";
+  }
 ```
 
 We've used one more trick with failure-compatible types in this method:
@@ -386,10 +386,18 @@ mapping our `CalibrationValue` function over the sequence of lines,
 and summing the results into the final answer.
 `MapWithResult` is a short-circuiting variation of `Map` where the mapped function can fail.
 
-If we put the sample input from the puzzle description into `input.txt`
+Let's put the sample input from the puzzle description into `input.txt` so we can try it out
 (not the actual puzzle input - I draw the line at publishing the answer in this blog post,
-you're just going to have to run the solution yourself to get that!),
-we can run our project and get...
+you're just going to have to run the solution yourself to get that!)
+
+```
+1abc2
+pqr3stu8vwx
+a1b2c3d4e5f
+treb7uchet
+```
+
+Now we can run our project and get...
 
 ```dafny
 % dafny run dfyconfig.toml
diff --git a/assets/src/standard-libraries/solution.dfy b/assets/src/standard-libraries/solution.dfy
index 6a6126b..db27b2d 100644
--- a/assets/src/standard-libraries/solution.dfy
+++ b/assets/src/standard-libraries/solution.dfy
@@ -1,41 +1,39 @@
 
-// Module contents not indented so they match the indentation
-// of the rest of the snippets when included by inline-dafny
 module M1 {
 
-import Std.BoundedInts
-import Std.Collections.Seq
-import Std.FileIO
-import Std.Strings
-import Std.Strings.DecimalConversion
-import Std.Unicode.UnicodeStringsWithUnicodeChar
-import Std.Wrappers
+  import Std.BoundedInts
+  import Std.Collections.Seq
+  import Std.FileIO
+  import Std.Strings
+  import Std.Strings.DecimalConversion
+  import Std.Unicode.UnicodeStringsWithUnicodeChar
+  import Std.Wrappers
 
-method Main() {
-  var input :- expect ReadPuzzleInput();
+  method Main() {
+    var input :- expect ReadPuzzleInput();
 
-  var lines := Seq.Split(input, '\n');
+    var lines := Seq.Split(input, '\n');
 
-  var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
+    var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);
 
-  var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
-  print total, "\n";
-}
+    var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
+    print total, "\n";
+  }
 
-method ReadPuzzleInput() returns (input: Wrappers.Result) {
-  var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
-  var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
-  
-  input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
-}
+  method ReadPuzzleInput() returns (input: Wrappers.Result) {
+    var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
+    var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
+    
+    input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
+  }
 
-function CalibrationValue(line: string): Wrappers.Result {
-  var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
-  var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
+  function CalibrationValue(line: string): Wrappers.Result {
+    var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
+    var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
 
-  var resultStr := [line[firstDigitIndex], line[lastDigitIndex]];
+    var resultStr := [line[firstDigitIndex], line[lastDigitIndex]];
 
-  Wrappers.Success(Strings.ToNat(resultStr))
-}
+    Wrappers.Success(Strings.ToNat(resultStr))
+  }
 
 }