Makefile

# Verity: Formally verified smart contracts
#
# Prerequisites: curl, git, python3, bash
# Run `make setup` to install all tooling, then `make verify` to check all proofs.

.PHONY: help setup setup-elan setup-solc setup-foundry \
        verify verify-packages verify-targeted profile-lean test test-foundry test-python axiom-report \
        compile generate-yul check checks test-evmyullean-fork \
        refresh-status all clean

# Pinned versions (must match .github/workflows/verify.yml)
ELAN_VERSION     := v4.1.2
SOLC_VERSION     := 0.8.33
SOLC_URL         := https://binaries.soliditylang.org/linux-amd64/solc-linux-amd64-v$(SOLC_VERSION)+commit.64118f21
SOLC_SHA256      := 1274e5c4621ae478090c5a1f48466fd3c5f658ed9e14b15a0b213dc806215468
FOUNDRY_VERSION  := v1.5.0

help: ## Show this help
	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | \
		awk 'BEGIN {FS = ":.*?## "}; {printf "  \033[36m%-20s\033[0m %s\n", $$1, $$2}'

# ---------------------------------------------------------------------------
# Setup
# ---------------------------------------------------------------------------

setup: setup-elan setup-solc setup-foundry ## Install all tooling (elan, solc, foundry)
	@echo ""
	@echo "Setup complete. Run 'make verify' to check all proofs."

setup-elan: ## Install elan + Lean toolchain
	@if command -v elan >/dev/null 2>&1; then \
		echo "elan already installed: $$(elan --version)"; \
	else \
		echo "Installing elan $(ELAN_VERSION)..."; \
		curl -sSfL "https://raw.githubusercontent.com/leanprover/elan/$(ELAN_VERSION)/elan-init.sh" | \
			bash -s -- -y --default-toolchain none; \
		echo 'Add $$HOME/.elan/bin to your PATH if not already present.'; \
	fi

setup-solc: ## Install solc (SHA256-verified)
	@if command -v solc >/dev/null 2>&1 && solc --version 2>/dev/null | grep -q "$(SOLC_VERSION)"; then \
		echo "solc $(SOLC_VERSION) already installed"; \
	else \
		echo "Installing solc $(SOLC_VERSION)..."; \
		curl -sSfL "$(SOLC_URL)" -o /tmp/solc; \
		echo "$(SOLC_SHA256)  /tmp/solc" | sha256sum -c -; \
		sudo mv /tmp/solc /usr/local/bin/solc; \
		sudo chmod +x /usr/local/bin/solc; \
		echo "solc $(SOLC_VERSION) installed"; \
	fi

setup-foundry: ## Install Foundry (forge, cast, anvil)
	@if command -v forge >/dev/null 2>&1; then \
		echo "Foundry already installed: $$(forge --version)"; \
	else \
		echo "Installing Foundry $(FOUNDRY_VERSION)..."; \
		curl -L https://foundry.paradigm.xyz | bash; \
		$$HOME/.foundry/bin/foundryup --version $(FOUNDRY_VERSION); \
		echo 'Add $$HOME/.foundry/bin to your PATH if not already present.'; \
	fi

# ---------------------------------------------------------------------------
# Verification
# ---------------------------------------------------------------------------

verify: ## Verify all proofs (lake build)
	lake build

verify-packages: ## Verify split Lake packages build independently
	python3 scripts/check_split_package_builds.py

verify-targeted: ## Fast local iteration on hotspot modules before full verify
	lake build Compiler.Proofs.IRGeneration.SourceSemantics
	lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBuiltinSemantics
	lake build Compiler.Proofs.IRGeneration.FunctionBody
	lake build Compiler.Proofs.EndToEnd

profile-lean: ## Profile Lean module build time and update docs/LEAN_PERF_QUEUE.md
	python3 scripts/profile_lean_modules.py --output docs/LEAN_PERF_QUEUE.md

axiom-report: ## Generate axiom dependency report for all 550 theorems
	lake env lean PrintAxioms.lean 2>&1 | tee axiom-report-raw.log
	python3 scripts/check_axioms.py --log axiom-report-raw.log

# ---------------------------------------------------------------------------
# Compilation
# ---------------------------------------------------------------------------

compile: ## Build compiler + interpreter
	set -- $$(grep -vE '^[[:space:]]*($$|#)' packages/verity-examples/contracts.manifest); \
	lake build "$$@" verity-compiler difftest-interpreter

verify-storage-layout: ## Check committed storage layout artifacts against current Lean source (#1897)
	lake build verity-storage-layout-report
	python3 scripts/generate_storage_layout_report.py --check

generate-yul: compile ## Compile all contracts to Yul
	./.lake/build/bin/verity-compiler

# ---------------------------------------------------------------------------
# Testing
# ---------------------------------------------------------------------------

test: test-python ## Run fast tests (Python validators)

test-python: ## Run Python unit tests
	python3 -m unittest discover -s scripts -p 'test_*.py' -v

test-foundry: ## Run Foundry differential tests (requires solc + forge + generated Yul)
	FOUNDRY_PROFILE=difftest forge test

test-evmyullean-fork: ## Probe EVMYulLean fork conformance (audit + native lowering report + EndToEnd target)
	@echo "Checking EVMYulLean fork pin + drift audit..."
	python3 scripts/generate_evmyullean_fork_audit.py --check
	@echo "Checking EVMYulLean native lowering report..."
	python3 scripts/generate_evmyullean_native_lowering_report.py --check
	@echo "Building EVMYulLean bridge lemmas, native harness, and 0 concrete bridge tests..."
	lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
	lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeTest
	lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness
	@echo "Building public EVMYulLean EndToEnd target..."
	lake build Compiler.Proofs.EndToEnd
	@echo "EVMYulLean fork conformance probe passed."

check: ## Run local CI-equivalent checks job (no Lean build, no solc)
	@echo "Running CI-equivalent checks job..."
	python3 scripts/property_pipeline.py check
	python3 scripts/lean_lint.py --only contract_structure
	python3 scripts/lean_lint.py --only paths
	python3 scripts/lean_lint.py --only compilationmodel_split
	python3 scripts/lean_lint.py --only axioms
	python3 scripts/lean_lint.py --only trust_surface_registry
	python3 scripts/check_benchmark_cases.py
	python3 scripts/generate_verification_status.py --check
	python3 scripts/generate_layer2_boundary_catalog.py --check
	python3 scripts/check_verification_status_doc.py
	python3 scripts/docsync.py --check --only layer2_boundary
	python3 scripts/docsync.py --check --only layer2_boundary_catalog
	python3 scripts/generate_verify_sync_spec.py --check
	python3 scripts/check_verify_sync.py
	python3 scripts/check_bridge_coverage_sync.py
	python3 scripts/check_builtin_bridge_matrix_sync.py
	python3 scripts/docsync.py --check --only interpreter_feature_boundary_catalog
	python3 scripts/check_interpreter_feature_summary_sync.py
	python3 scripts/docsync.py --check --only low_level_call_boundary
	python3 scripts/docsync.py --check --only linear_memory_boundary
	python3 scripts/docsync.py --check --only axiomatized_primitive_boundary
	python3 scripts/docsync.py --check --only struct_mapping_surface
	python3 scripts/check_solc_pin.py
	python3 scripts/check_issue_templates.py
	python3 scripts/check_docs_workflow_sync.py
	python3 scripts/check_macro_health.py
	python3 scripts/lean_lint.py --only storage_layout
	python3 scripts/generate_storage_layout_report.py --check --no-lean
	python3 scripts/lean_lint.py --only lean_hygiene
	python3 scripts/check_gas.py coverage
	python3 scripts/check_compiler_boundaries.py
	python3 scripts/lean_lint.py --only split_compiler_test_artifacts
	python3 scripts/check_yul.py --builtin-boundary-only
	python3 scripts/lean_lint.py --only rewrite_proof_metadata
	python3 scripts/generate_evmyullean_capability_report.py --check
	python3 scripts/generate_evmyullean_native_lowering_report.py --check
	python3 scripts/generate_evmyullean_fork_audit.py --check
	python3 scripts/generate_print_axioms.py --check
	python3 scripts/lean_lint.py --only proof_length
	python3 scripts/check_issue_1060_integrity.py
	python3 scripts/update_doc_numbers.py --check
	python3 -m unittest discover -s scripts -p 'test_*.py' -v
	@echo "All checks passed."

checks: check ## Compatibility alias for the CI-equivalent checks job

refresh-status: ## Regenerate verification artifact
	scripts/refresh_verification_artifacts.sh

regen-storage-layout-report: ## Regenerate the storage layout audit artifacts (needs Lean)
	python3 scripts/generate_storage_layout_report.py

# ---------------------------------------------------------------------------
# Full pipeline
# ---------------------------------------------------------------------------

all: verify check axiom-report ## Full local verification pipeline
	@echo ""
	@echo "All proofs verified, all checks passed, axiom report generated."

clean: ## Remove build artifacts
	lake clean
	rm -f axiom-report-raw.log axiom-report.md