A File Archiver

• A content-addressable store identifies files by their hash rather than their name
  • Two files with the same content get the same address
  • Like Git's .git/objects directory
• We'll build it in layers: types first, then pure logic, then I/O
• See the JavaScript and Python versions for comparison

Type Aliases

-- A content address is just a hex string of the hash
abbrev Hash := String

• abbrev creates a type alias (a shorter name for an existing type)
  • Hash and String are interchangeable
• A content address is just a hex string of the file's hash

-- A manifest maps each original file path to its content hash
abbrev Manifest := List (String × Hash)

• A manifest maps original file paths to their content hashes
• List (String × Hash) is a list of (path, hash) pairs
• abbrev makes the intent clearer than writing List (String × Hash) everywhere

abbrev vs. def for Type Aliases

• Lean has two ways to create a type alias: abbrev and def
• abbrev is transparent: the type checker sees through it and treats Hash exactly as String
  • Type class instances for String (like ToString or BEq) automatically apply to Hash
  • You can pass a Hash anywhere a String is expected without any conversion
• def is opaque: the type checker treats the alias as a distinct type
  • Instances do not transfer automatically; you must re-derive or re-declare them
  • Passing a def-aliased type where the original is expected is a type error
• Use abbrev when the alias is purely for readability and you want full interchangeability
• Use def when you want the type system to enforce that the aliased type is not accidentally mixed with the original

Hashing Bytes

-- Hash a ByteArray to a 16-character hex string
def hashBytes (ba : ByteArray) : Hash :=
  let h : UInt64 := hash ba
  let hex := "0123456789abcdef".toList
  let digits := (List.range 16).map fun i =>
    let nibble := (h >>> (60 - i * 4).toUInt64) &&& 0xF
    hex[nibble.toNat]!
  String.ofList digits

• hashBytes takes a ByteArray and returns a 16-character hex Hash
• hash is Lean's built-in structural hash function
  • Returns a UInt64 (unsigned 64-bit integer)
  • A real archiver would use SHA-256, but this is good enough for teaching
• The body formats the UInt64 into hex by extracting each 4-bit nibble
  • h >>> n shifts the hash right by n bits
  • &&& 0xF masks off the lowest 4 bits to get one hex digit
• String.ofList digits converts the list of Char to a String
  • String.mk would also work, but Lean now prefers String.ofList

Building the Manifest

-- Pure: deduplicate a list of (path, bytes) pairs into (Manifest, blob store)
def buildManifest (files : List (String × ByteArray)) :
    Manifest × List (Hash × ByteArray) :=
  let entries := files.map fun (path, bytes) => (path, hashBytes bytes, bytes)
  let manifest := entries.map fun (path, h, _) => (path, h)
  let blobs := entries.foldl (init := []) fun acc (_, h, bytes) =>
    if acc.any (·.1 == h) then acc else acc ++ [(h, bytes)]
  (manifest, blobs)

• buildManifest is the pure core of the archiver
  • No I/O: takes data in, returns data out
  • Hence the name "pure"
• Step 1: hash every file's bytes and create (path, hash, bytes) triples
• Step 2: extract just the (path, hash) pairs into the manifest
• Step 3: deduplicate blobs by checking if a hash already exists in the accumulator
  • acc.any (·.1 == h): "does any entry in acc have .1 equal to h?"
  • (·.1 == h) uses the · placeholder for the tuple's first field
• Returns a pair (manifest, blobs)
  • manifest maps every path to its hash (even duplicates)
  • blobs stores each unique (hash, bytes) pair only once

Snapshot: Writing Files

-- IO: write each unique blob to a file named <hash>.bck
def snapshot (files : List (String × ByteArray)) (archiveDir : String) :
    IO Manifest := do
  let (manifest, blobs) := buildManifest files
  for (h, bytes) in blobs do
    IO.FS.writeBinFile s!"{archiveDir}/{h}.bck" bytes
  return manifest

• snapshot is an I/O function: note the IO Manifest return type
• Calls the pure buildManifest, then writes each unique blob to disk
• for (h, bytes) in blobs do iterates over the blob list (instead of recursing)
  • Destructures each (hash, bytes) pair in the loop header
• IO.FS.writeBinFile writes raw bytes to a file
  • Like Python's open(path, "wb").write(data)
• Each blob is saved as archiveDir/<hash>.bck
  • The .bck extension is just a convention — like Git's loose object format
• Returns the manifest so the caller can save or transmit it

Restore: Reading Files Back

-- IO: read blobs from the archive and write them back to their original paths
def restore (manifest : Manifest) (archiveDir : String) : IO Unit := do
  for (path, h) in manifest do
    let bytes ← IO.FS.readBinFile s!"{archiveDir}/{h}.bck"
    IO.FS.writeBinFile path bytes

• restore reverses the process
  • Read blobs from the archive
  • Write them to original paths
• IO Unit means "does I/O but returns nothing useful"
  • Like a Python function that returns None
• ← captures the result of IO.FS.readBinFile
  • Reading from disk is I/O, so we need the left arrow
• s!"{archiveDir}/{h}.bck" constructs the blob path using string interpolation
• Then IO.FS.writeBinFile writes the bytes back to the original file path

Listing a Directory

-- Collect all regular files in a directory as (path, bytes) pairs
def listFiles (dir : String) : IO (List (String × ByteArray)) := do
  let entries ← (dir : System.FilePath).readDir
  let mut files : List (String × ByteArray) := []
  for entry in entries do
    let info ← entry.path.metadata
    if info.type == IO.FS.FileType.file then
      let bytes ← IO.FS.readBinFile entry.path
      files := files ++ [(entry.path.toString, bytes)]
  return files

• dir.readDir lists all entries in a directory and returns an Array IO.FS.DirEntry
  • dir must be a System.FilePath; a String is coerced automatically
  • Like Python's os.scandir(dir) — returns both files and subdirectories
• entry.path.metadata inspects the filesystem entry
  • Returns an IO.FS.Metadata record with a .type field
  • IO.FS.FileType.file means a regular file; .dir is a subdirectory
• let mut files := [] accumulates results using a mutable variable in the do block (see io)
• The result is a list of (path, bytes) pairs — exactly what snapshot already expects

Archiving a Directory

-- Archive every regular file in srcDir to archiveDir
def snapshotDir (srcDir archiveDir : String) : IO Manifest := do
  IO.FS.createDirAll archiveDir
  let files ← listFiles srcDir
  snapshot files archiveDir

• snapshotDir is four lines: create the archive directory, list files, call snapshot
• snapshot (from archive.lean) is unchanged — it accepts any List (String × ByteArray)
• This is the payoff of pure-core design: the I/O boundary is thin and swappable
  • Swapping hand-written sample files for real disk files required only listFiles

-- Entry point: archive a directory and report results
-- Run with: lean --run archive/archive_dir.lean
def main : IO Unit := do
  let archiveDir := "archive-dir"
  IO.println s!"Scanning current directory..."
  let manifest ← snapshotDir "." archiveDir
  IO.println s!"Archived {manifest.length} file(s) to {archiveDir}/"
  let blobs := (buildManifest (← listFiles ".")).2.length
  IO.println s!"Unique content blobs: {blobs}"
  IO.println "Done."

• To compile and type-check:
  • lake env lean archive/archive_dir.lean
• To run and create a real archive:
  • lean --run archive/archive_dir.lean
• The distinction between these two commands is important; see build for a full explanation

Testing the Pure Core

-- Tests (pure core) ---------------------------------------------------

def sampleFiles : List (String × ByteArray) := [
  ("a.txt", "hello".toUTF8),
  ("b.txt", "hello".toUTF8),   -- same content as a.txt
  ("c.txt", "world".toUTF8)
]

-- Two files with identical content should produce only two blobs
#guard (buildManifest sampleFiles).2.length == 2

-- Both a.txt and b.txt map to the same hash
#guard
  let (manifest, _) := buildManifest sampleFiles
  (manifest.find? (·.1 == "a.txt")).map (·.2) ==
  (manifest.find? (·.1 == "b.txt")).map (·.2)

• We can test the pure logic without touching the filesystem
  • Because buildManifest is pure, tests are fast and deterministic
• sampleFiles creates three files: a.txt and b.txt have identical content
• "hello".toUTF8 converts a string to a ByteArray
  • Like Python's "hello".encode("utf-8")
• First #guard: two identical files should produce only two blobs, not three
  • .2.length accesses the blob list (second element of the pair) and counts it
• Second #guard: a.txt and b.txt should map to the same hash
  • manifest.find? (·.1 == "a.txt") finds the entry for a.txt
  • .map (·.2) extracts the hash from the found entry
• Both #guard expressions evaluate to true, so compilation succeeds silently

The Full Picture

• Forty lines of code implement a content-addressable archive
• The design separates pure computation from I/O
  • buildManifest can be tested without touching disk
  • snapshot and restore do the actual reading and writing
• This is the functional style in practice:
  • Types describe the data (Hash, Manifest)
  • Pure functions transform it (buildManifest)
  • A thin I/O layer connects to the outside world

Running the Program

-- Entry point: snapshot sample files to ./archive-dir, then restore them
-- Run with: lean --run archive/archive.lean
def main : IO Unit := do
  let archiveDir := "archive-dir"
  -- create the archive directory (ok if it already exists)
  IO.FS.createDirAll archiveDir
  IO.println s!"Snapshotting to {archiveDir}/"
  let manifest ← snapshot sampleFiles archiveDir
  IO.println s!"Created {manifest.length} manifest entries"
  IO.println "Restoring files..."
  restore manifest archiveDir
  IO.println "Done."

• main is the entry point when you run a Lean file as a program
  • Like Python's if __name__ == "__main__": block
• IO.FS.createDirAll archiveDir creates the archive directory
  • Won't fail if the directory already exists
• The steps match our earlier sections exactly: snapshot, then restore
• IO.println outputs a line of text to stdout
• manifest.length is the number of entries in the manifest

Compiling and Running

• To compile (check types, run #eval and #guard):
  • lake env lean archive/archive.lean
  • This is what we've been doing all along
  • The #guard tests run at compile time
  • main is not executed: it's just type-checked
• To run the program (execute main):
  • lean --run archive/archive.lean
  • This compiles the file and calls the main function
• After running, check the results:
  • ls archive-dir/ shows the .bck blob files
  • Two files, because a.txt and b.txt are deduplicated
  • cat a.txt, cat b.txt, cat c.txt show the restored content in the current directory
• The two commands serve different purposes:
  • lake env lean for development: type-check and test
  • lean --run for execution: actually do the I/O

-- hashBytes should produce correct hex digits, but the loop extracts
-- nibbles in the wrong order. The result is reversed. Fix it.
def hashBytes (ba : ByteArray) : String :=
  let h : UInt64 := hash ba
  let hex := "0123456789abcdef".toList
  let digits := (List.range 16).map fun i =>
    let nibble := (h >>> (i * 4).toUInt64) &&& 0xF
    hex[nibble.toNat]!
  String.ofList digits

#guard hashBytes "hello".toUTF8 == hashBytes "hello".toUTF8
#guard hashBytes "hello".toUTF8 != hashBytes "world".toUTF8

-- buildManifest should deduplicate blobs by hash, but it keeps every
-- blob entry instead. The blob store has duplicates. Fix the dedup check.
abbrev Hash := String

def hashBytes (ba : ByteArray) : Hash :=
  toString (hash ba)

def buildManifest (files : List (String × ByteArray)) :
    List (String × Hash) × List (Hash × ByteArray) :=
  let entries := files.map fun (path, bytes) => (path, hashBytes bytes, bytes)
  let manifest := entries.map fun (path, h, _) => (path, h)
  let blobs := entries.map fun (_, h, bytes) => (h, bytes)
  (manifest, blobs)

def sample : List (String × ByteArray) := [
  ("a.txt", "hello".toUTF8),
  ("b.txt", "hello".toUTF8),   -- same content as a.txt
  ("c.txt", "world".toUTF8)
]

#guard (buildManifest sample).2.length == 2

-- snapshot should create the archive directory before writing blobs,
-- but it doesn't. The first file write will fail. Add the missing directory
-- creation step.
abbrev Hash := String

def snapshot (files : List (String × ByteArray)) (archiveDir : String) :
    IO Unit := do
  for (path, bytes) in files do
    let h : Hash := toString (hash bytes)
    IO.FS.writeBinFile s!"{archiveDir}/{h}.bck" bytes

#eval snapshot [("a.txt", "hello".toUTF8)] "test-archive"

-- restore constructs the blob path wrong: it uses the file path instead
-- of the hash to read the blob. Fix the file path construction.
abbrev Hash := String
abbrev Manifest := List (String × Hash)

def restore (manifest : Manifest) (archiveDir : String) : IO Unit := do
  for (path, _h) in manifest do
    let bytes ← IO.FS.readBinFile s!"{archiveDir}/{path}.bck"
    IO.FS.writeBinFile path bytes

-- To test: first run snapshot on sample data, then restore with this.
-- The bug path uses the file name instead of the hash for the blob file.

-- Look up a file path in the manifest and return its hash (if present).
-- You may use the existing definitions from archive.lean.
abbrev Hash := String
abbrev Manifest := List (String × Hash)

def findFile (manifest : Manifest) (path : String) : Option Hash :=
  none

#guard findFile [("a.txt", "abc123"), ("b.txt", "def456")] "a.txt" == some "abc123"
#guard findFile [("a.txt", "abc123")] "c.txt" == none
#guard findFile [] "x.txt" == none

-- Count how many unique blobs are in the blob store.
-- A blob store is a list of (hash, bytes) pairs.
abbrev Hash := String

def countUniqueBlobs (blobs : List (Hash × ByteArray)) : Nat :=
  0

def sampleBlobs : List (Hash × ByteArray) := [
  ("abc", "hello".toUTF8),
  ("def", "world".toUTF8),
  ("abc", "hello".toUTF8)   -- duplicate hash, same content
]

#guard countUniqueBlobs sampleBlobs == 2
#guard countUniqueBlobs [] == 0
#guard countUniqueBlobs [("x", "a".toUTF8)] == 1

-- Find all file paths in the manifest that have the given hash.
abbrev Hash := String
abbrev Manifest := List (String × Hash)

def findByHash (manifest : Manifest) (target : Hash) : List String :=
  []

def m : Manifest := [("a.txt", "abc"), ("b.txt", "def"), ("c.txt", "abc")]

#guard findByHash m "abc" == ["a.txt", "c.txt"]
#guard findByHash m "xyz" == []
#guard findByHash [] "abc" == []

-- Compare two manifests. Return the paths that appear in the first
-- manifest but not the second (new or renamed files).
abbrev Hash := String
abbrev Manifest := List (String × Hash)

def diffManifests (old new : Manifest) : List String :=
  []

def oldManifest : Manifest := [("a.txt", "abc"), ("b.txt", "def")]
def newManifest : Manifest := [("a.txt", "abc"), ("c.txt", "xyz")]

#guard diffManifests oldManifest newManifest == ["b.txt"]
#guard diffManifests newManifest oldManifest == ["c.txt"]
#guard diffManifests [] [] == []

-- buildManifest constructs the manifest, but the path and hash are mispaired.
-- The entry for each file should contain (path, hash). Fix the pairing.
abbrev Hash := String
abbrev Manifest := List (String × Hash)

def hashBytes (ba : ByteArray) : Hash :=
  let h : UInt64 := hash ba
  let hex := "0123456789abcdef".toList
  let digits := (List.range 16).map fun i =>
    let nibble := (h >>> (60 - i * 4).toUInt64) &&& 0xF
    hex[nibble.toNat]!
  String.ofList digits

def buildManifest (files : List (String × ByteArray)) :
    Manifest × List (Hash × ByteArray) :=
  let entries := files.map fun (path, bytes) => (path, hashBytes bytes, bytes)
  -- BUG: manifest pairs each path with the wrong file's hash
  -- The manifest is built by zipping paths with the *reversed* hash list
  let hashes := entries.map fun (_, h, _) => h
  let manifest := List.zip
    (entries.map fun (p, _, _) => p)
    hashes.reverse
  let blobs := entries.foldl (init := []) fun acc (_, h, bytes) =>
    if acc.any (·.1 == h) then acc else acc ++ [(h, bytes)]
  (manifest, blobs)

#guard
  let files := [("a.txt", "hello".toUTF8), ("b.txt", "world".toUTF8)]
  let (manifest, _) := buildManifest files
  (manifest.find? (·.1 == "a.txt")).map (·.2) == some (hashBytes "hello".toUTF8)

#guard
  let files := [("a.txt", "hello".toUTF8), ("b.txt", "hello".toUTF8)]
  let (manifest, _) := buildManifest files
  (manifest.find? (·.1 == "a.txt")).map (·.2) ==
  (manifest.find? (·.1 == "b.txt")).map (·.2)