Proof-only solidity_contract import for Vault

[fricoben]

What this adds

A self-contained proof-only example under Contracts/VaultFromSolidity that imports an existing Solidity Vault directly into Lean and proves specifications against the imported transparent definitions. The handwritten Contracts/Vault example is unchanged.

Pipeline

Vault.sol
  → pinned solc 0.8.33 --standard-json --no-import-callback
  → typed Solidity AST + storageLayout
  → Lean-only Importer.lean validation and translation
  → safe transparent Verity definitions
  → Spec.lean + Lean proofs

There is no production Python frontend, custom serialized instruction IR, generated model .lean, CompilationModel, or bytecode. Python remains only as the disposable acceptance/mutation test orchestrator.

Self-contained file guide

File	Purpose
Contracts/VaultFromSolidity/Vault.sol	Solidity implementation.
Contracts/VaultFromSolidity/Importer/Importer.lean	Invokes pinned solc, validates its standard JSON output, translates supported constructs, and registers checked definitions.
Contracts/VaultFromSolidity/VaultFromSolidity.lean	Declares solidity_contract VaultFromSolidity from "Vault.sol".
Contracts/VaultFromSolidity/Spec.lean	Human-written requirements for the imported contract.
Contracts/VaultFromSolidity/Proofs/Execution.lean	Fifteen proofs directly about imported definitions.
Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py	Disposable mutation, rejection, freshness, rollback, transparency, and axiom suite.

Determinism and fail-closed validation

• Pins the official Linux-amd64 solc 0.8.33 binary by exact version output and SHA-256 checksum, with checksum checks before and after compiler execution.
• Uses --standard-json and --no-import-callback.
• Recursively validates a closed AST schema, required fields, primitive/record/list types, source IDs/spans, declaration IDs/references, type descriptions, exported symbols, and storage layout.
• Rejects unsupported nodes, metadata, operators, storage forms, source paths, and declaration collisions with source-position diagnostics.
• Registers safe transparent declarations transactionally and kernel-checks each declaration synchronously.
• Includes Solidity source, compiler output/pin, importer implementation, and compiler version in sourceDigest.
• Changes to accepted deposit/getter behavior refresh artifacts and fail their corresponding existing proofs.

Developer UX

solidity_contract VaultFromSolidity from "Vault.sol"
#print Contracts.VaultFromSolidity.deposit

lake build VaultFromSolidity
python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py
make check

After Solidity edits, rebuild and reload Lean. The POC accepts only the registered Vault and a deliberately small Solidity subset.

Trust boundary

The proof-only importer remains trusted. Lean checks the generated definitions and every theorem about their execution; this is not yet a theorem that the Lean translation preserves all Solidity meaning. Exact revert bytes, deployment, calldata/dispatch, gas, bytecode, and full Solidity/EVM equivalence remain outside the claim. See TRUST_ASSUMPTIONS.md for the precise host/compiler/importer assumptions.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
verity	Ready	Preview	Sep 10, 2026 11:30am UTC

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```