Formal Methods for Critical Systems Project 2 - Verified File Reverse and Grep Utilities

Curricular Unit: Formal Methods for Critical Systems - 2025/26 2S
Faculty: FEUP
Professor: João Ferreira
Authors: Bruno Oliveira, Dário Guimarães, José Sousa
Final Grade: 19.25/20

This project consists of two challenges, each requiring the implementation of a verified utility in Dafny. The first challenge involves creating a file reverse utility, while the second challenge focuses on developing an executable that mimics the grep command. Both utilities are designed to be verified, using deductive verification, ensuring correctness and reliability in their operations.

Group Elements

• up202208700 Bruno Oliveira
• up202502543 Dário Guimarães
• up202208817 José Sousa

Accomplished Work

Challenge 1: Verified File Reverse Utility

As part of the first challenge, we implemented a reverse line utility that takes two file paths as input (source and destination) and reverses the lines of the source file, writing them to the destination file if it does not already exist.

The program works in three stages. First, ReadLines reads the source file as an array of bytes and transforms it into a seq<Line> (where type Line = seq<byte>), an easier representation to work with and reason about for this context. Then Reverse reverses the sequence of lines. Finally, WriteLines transforms the reversed seq<Line> back into bytes and writes them to the destination file.

Reverse is specified by the ghost function Rev<T>, which defines reversal inductively: the empty sequence stays empty, and a non-empty sequence becomes its tail reversed followed by its head. The implementation places each element at its mirrored position using a sequence comprehension, achieving O(n) complexity. This is preferred over a loop with repeated appends, which would be O(n²) since Dafny sequences are immutable:

ghost function Rev<T>(s: seq<T>): seq<T>
{
  if |s| == 0 then [] else Rev(s[1..]) + [s[0]]
}

method Reverse<T>(s: seq<T>) returns (rev: seq<T>)
  ensures rev == Rev(s)
{
  rev := seq(|s|, i requires 0 <= i < |s| => s[|s| - 1 - i]);
}

Note: If the source file ends with \n, it is treated as an empty last line; when reversed, this becomes an empty first line.

Preserving the total byte count

One of the hardest challenges we faced was that FileStream.Write requires the number of bytes written to fit in a 32-bit integer. To solve this, we defined TotalSize, a function that computes how many bytes a seq<Line> corresponds to, and proved it is preserved by reversal so the output always has the same size as the input.

Challenge 2: Verified Grep Utility

For the second challenge, we implemented a verified grep utility that searches for pattern occurrences in a file and displays matching lines with highlighted matches. The challenge was divided into two implementations - a naive approach and a KMP-based approach - however, all code outside the search algorithm is shared between both implementations. This shared code resides in the grep-utils/ folder, which contains helper modules for reading command-line arguments, reading files, splitting content into lines, and highlighting matches. Both implementations have identical Main methods that orchestrate these utilities, diverging only in the Search function implementation.

Shared Utilities (grep-utils)

The grep-utils/ folder contains five Dafny modules and one C# file that together provide a verified I/O pipeline:

Args.dfy - Parses command-line arguments. The GetArgs method validates that exactly 3 arguments are provided (program name + pattern + file path) and that neither pattern nor file path is empty. Its postconditions guarantee that, on success, the returned values exactly match CommandLineArgs()[1] and CommandLineArgs()[2].

FileIO.dfy - Handles file reading. The ReadFile method checks if the file exists, opens it, reads its full content into a buffer, and closes it. Postconditions ensure that, on success, the returned content exactly matches env.files.state()[filePath].

LineSplitter.dfy - Splits file content into lines. The SplitIntoLines method iterates over the content, splitting at each \n character. The ghost function ReconstructLines defines how lines should recombine (joining with \n). Postconditions guarantee that no resulting line contains \n and that reconstruction matches the original content, ensuring no splits were missed or added incorrectly.

HighlightMatches.dfy - Highlights matches using ANSI color codes. The HighlightMatches method wraps each match in red (\[31m...\[0m).

Naive Implementation

The naive Search method slides over every valid start position j from 0 to n - m, comparing text[j..j+m] against pattern. Matches are recorded in a bool[] array (avoiding expensive set operations) and converted to a set<int> at the end.

method Search(pattern: string, text: string) returns (matches: set<int>)
  requires 0 < |pattern|
  ensures forall idx :: idx in matches <==> IsMatch(text, pattern, idx)

Naive Correctness

The postcondition is proven by two loop invariants capturing soundness and completeness:

invariant forall idx :: 0 <= idx <= n - m && isMatch[idx] ==> IsMatch(text, pattern, idx)
invariant forall idx :: 0 <= idx < j && IsMatch(text, pattern, idx) ==> isMatch[idx]

When j == n - m + 1, the invariants imply that isMatch records exactly all valid matches, as defined by:

ghost predicate IsMatch(text: string, pattern: string, idx: int)
{
  0 <= idx <= |text| - |pattern| && text[idx .. idx + |pattern|] == pattern
}

KMP Implementation

As part of the challenge, we also implemented a fully verified version of the Knuth-Morris-Pratt (KMP) string searching algorithm. The implementation is almost identical to the one presented in the book "Introduction to Algorithms", where we compute the prefix function using the method ComputePrefix, and use it for our search in Search to find all occurrences of a pattern in a given text.

The postconditions of both ComputePrefix and Search are translated into simple expressions that directly reflect the mathematical definitions of the prefix function and a substring matching algorithm.

method ComputePrefix(pattern: string) returns (prefix: array<int>)
  requires 0 < |pattern|
  ensures prefix.Length == |pattern|
  ensures forall i :: 0 <= i < |pattern| ==> IsMaxPrefix(pattern, i + 1, prefix[i])

method Search(text: string, pattern: string) returns (matches: set<int>)
  requires 0 < |pattern|
  ensures forall idx :: idx in matches <==> IsMatch(text, pattern, idx)

KMP Correctness

To prove the correctness of our KMP implementation, we defined a total of three auxiliar predicates (IsValidPrefix, IsMaxPrefix, and IsMatch) and four auxiliar lemmas (ComputePrefix_MaxPrefixGrowsByAtMostOne, ComputePrefix_FallbackSkipsNoValidPrefix, ComputePrefix_PrefixExtension, and Search_NoMatchAfterFallback). All the predicates and lemmas are properly documented, with clarifying comments throughout the proofs.

Both methods are proven based on ensuring the main invariants in each step, which are directly adapted from the postconditions. For ComputePrefix, the main invariant is:

invariant forall i :: 0 <= i < q ==> IsMaxPrefix(pattern, i + 1, prefix[i])

The proof then, for each iteration, asserts that IsMaxPrefix(pattern, q, k), which involves not only proving that IsValidPrefix(pattern, q, k) holds, but also that there is no valid prefix of length greater than k relative to q. The main challenge is in the proof of the second part, specially on the updates of the value of k and at the start of the iteration, which are taken care of by the lemmas ComputePrefix_FallbackSkipsNoValidPrefix and ComputePrefix_MaxPrefixGrowsByAtMostOne, respectively.

For Search, the main invariants are:

invariant forall idx :: 0 <= idx <= n - m && isMatch[idx] ==> IsMatch(text, pattern, idx)
invariant forall idx :: 0 <= idx < i - q && IsMatch(text, pattern, idx) ==> isMatch[idx]

Both invariants translate the soundness and completeness of the matches found so far, i.e. all the matches found are valid, and all the valid matches in the text up to the current index are found. The proof of the first invariant is straightforward, as it only requires to assert that IsMatch(text, pattern, i - m) holds whenever a match is found. The second invariant is more tricky, for a similar reason to what was encountered with the ComputePrefix invariant, when we fallback the value of k. Thus, the lemma Search_NoMatchAfterFallback is used to help prove the fallback steps, based on the prefix function maximality.

References

1. Cormen, Thomas H., et al. Introduction to Algorithms. Fourth edition, The MIT Press, 2022.
2. Donald E Knuth, James H Morris, Jr, and Vaughan R Pratt. Fast pattern matching in strings. SIAM journal on computing, 6(2):323–350, 1977.