Initial commit: Lean 4 math and crypto toolchain with SHA-256, HMAC, … #1

	name: CI

	on:
	push:
	branches: [main, master]
	pull_request:
	branches: [main, master]
	workflow_dispatch:

	jobs:
	test:
	strategy:
	matrix:
	os: [ubuntu-22.04, macos-14]
	lean-version: [leanprover/lean4:v4.21.0]

	runs-on: ${{ matrix.os }}

	steps:
	- name: Checkout
	uses: actions/checkout@v4

	- name: Setup Lean
	uses: leanprover/lean-action@v1

	- name: Install Rust
	uses: actions-rs/toolchain@v1
	with:
	toolchain: stable
	override: true

	- name: Build
	run: lake build

	- name: Test
	run: lake test

	- name: Extract smoke test
	run: \|
	# Placeholder for extraction smoke test
	echo "Extraction smoke test - TODO: implement lake exe extract"
	# lake exe extract smoke

	- name: Check for sorry
	run: \|
	if grep -r "sorry" LeanToolchain/; then
	echo "Found 'sorry' statements - these should be replaced with proofs"
	exit 1
	fi

Provide feedback