sha2-fv 0.1.0

Formally verified Pure Rust implementation of the SHA-2 hash function family (SHA-224, SHA-256, SHA-384, SHA-512, SHA-512/224, SHA-512/256), with Lean 4 proofs of correctness against FIPS 180-4.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

# Makefile for verifying SHA-2 with Aeneas + Lean.
#
# Targets:
#   make extract - Run Charon (Rust → LLBC) and Aeneas (LLBC → Lean)
#   make prove   - Build the Lean proofs (lake build)
#   make clean   - Remove generated LLBC and Lean files
#
# The Rust source is left untouched: Aeneas reads it as-is.

LEAN_DIR        := proofs/lean
EXTRACT_SUBDIR  := Extraction
LEAN_PKG        := $(LEAN_DIR)/$(EXTRACT_SUBDIR)
LLBC            := $(LEAN_DIR)/sha2.llbc

CHARON_OPTIONS  := --preset=aeneas \
	--rustc-arg=--allow=unused
AENEAS_OPTIONS  := -backend lean -split-files -abort-on-error \
	-subdir $(EXTRACT_SUBDIR) -namespace $(EXTRACT_SUBDIR)

# Translate the full SHA-256 path: the public `sha256` and `sha224` entry
# points in lib.rs, plus everything they call.
START_FROM      := \
	--start-from sha2::sha256 \
	--start-from sha2::sha224 \
	--start-from sha2::sha512 \
	--start-from sha2::sha384 \
	--start-from sha2::sha512_256 \
	--start-from sha2::sha512_224

CARGO_FEATURES  := --no-default-features \
	--features "sha256,sha256_224,sha512,sha512_224,sha512_256,sha512_384"

# Colors for output
BLUE   := \033[34m
BBLUE  := \033[1;34m
RESET  := \033[0m
GREEN  := \033[32m

.PHONY: all extract prove clean help

all: extract prove

help:
	@echo "SHA-2 Aeneas+Lean verification Makefile"
	@echo ""
	@echo "Available targets:"
	@printf "  $(BLUE)extract$(RESET)  - Run Charon then Aeneas to regenerate Lean files\n"
	@printf "  $(BLUE)prove$(RESET)    - lake build the Lean proofs\n"
	@printf "  $(BLUE)clean$(RESET)    - Remove generated files\n"
	@printf "  $(BLUE)help$(RESET)     - Show this help message\n"

# Step 1: Charon translates Rust → LLBC
# Step 2: Aeneas translates LLBC → Lean
extract:
	@printf "$(BBLUE)[CHARON]$(RESET) Translating Rust → LLBC...\n"
	@mkdir -p $(LEAN_DIR)
	charon cargo $(CHARON_OPTIONS) --dest-file $(abspath $(LLBC)) $(START_FROM) -- $(CARGO_FEATURES)
	@printf "$(BBLUE)[AENEAS]$(RESET) Translating LLBC → Lean...\n"
	@mkdir -p $(LEAN_PKG)
	aeneas $(LLBC) $(AENEAS_OPTIONS) -dest $(LEAN_DIR)
	@printf "$(GREEN)✓$(RESET) Extraction complete. Generated files in $(LEAN_PKG)\n"

prove:
	@printf "$(BBLUE)[LAKE]$(RESET) Building Lean proofs...\n"
	cd $(LEAN_DIR) && lake build
	@printf "$(GREEN)✓$(RESET) All proofs check.\n"

clean:
	rm -f $(LLBC)
	rm -rf $(LEAN_PKG)
	rm -rf $(LEAN_DIR)/.lake/build