diff --git a/.github/actions/setup-solc/action.yml b/.github/actions/setup-solc/action.yml index e29fe6fcc1..81dfc668ce 100644 --- a/.github/actions/setup-solc/action.yml +++ b/.github/actions/setup-solc/action.yml @@ -1,6 +1,12 @@ name: Setup solc description: Cache and install the Solidity compiler +inputs: + destination: + description: Optional repository-local path at which to copy the verified binary + required: false + default: '' + runs: using: composite steps: @@ -46,4 +52,12 @@ runs: - name: Verify solc shell: bash - run: solc --version + run: | + solc --version + destination='${{ inputs.destination }}' + if [ -n "$destination" ]; then + mkdir -p "$(dirname "$destination")" + cp "$(command -v solc)" "$destination" + chmod +x "$destination" + echo "${SOLC_SHA256} ${destination}" | sha256sum -c - + fi diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 1cd8b104b8..b7c50a54d9 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -391,6 +391,11 @@ jobs: disable-lake-cache-restore: ${{ env.VERIFY_DISABLE_LAKE_CACHE_RESTORE }} cache-primary-key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lakefile.lean') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.run_id }} + - name: Setup pinned solc for Lean Solidity importer + uses: ./.github/actions/setup-solc + with: + destination: .lake/solidity-import/solc + - name: Rebuild cached local Lean modules run: | rm -rf .lake/build/lib/lean/Verity .lake/build/ir/Verity diff --git a/AUDIT.md b/AUDIT.md index 426b5c1210..da36459b12 100644 --- a/AUDIT.md +++ b/AUDIT.md @@ -5,6 +5,34 @@ reviewable. Keep it synchronized with `TRUST_ASSUMPTIONS.md` and `AXIOMS.md` whenever semantics, trusted components, generated audit artifacts, or CI boundary checks change. +## Proof-only Solidity Vault POC + +The focused suite probes unknown, wrong-typed, and missing AST fields (including +documentation metadata), invalid source spans, and malformed storage layout +through synthetic compiler-output mutations, plus unsupported source constructs, +contract `layout at`, +registered-source symlink escape, and Lean importer digest sensitivity. It also +checks safe transparent declarations, duplicate aliases, a deliberately +malformed late declaration and complete registration rollback, plus the pinned +compiler's checksum. The digest scope is documented in `TRUST_ASSUMPTIONS.md`; it is not a transitive build identity. + +Evidence command: +`python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py` +(after `lake build VaultFromSolidity` and installation of the pinned compiler). +The focused runner builds and audits the imported execution proofs, changes +accepted deposit/getter behavior while preserving source mtime and requires old +proofs to fail, rejects unsupported source, checks unchanged artifacts, and +exercises Lean-importer and compiler content invalidation. Mutations occur only +in disposable copies. This is local acceptance evidence, not a new CI job, +bytecode/runtime test, or proof of translation correctness. + +The complete example surface lives under `Contracts/VaultFromSolidity`: Solidity +source, Lean importer, specification, execution proofs and focused acceptance +tests. It is independent of the handwritten `Contracts/Vault` example. No +Python frontend, custom serialized IR, generated Lean source, or bytecode is in +the translation path. Trust and axiom scope are recorded in +`TRUST_ASSUMPTIONS.md` and `AXIOMS.md`. + ## Current Audit State - Lean proof placeholders: 0 `sorry` in compiler/proof modules. diff --git a/AXIOMS.md b/AXIOMS.md index 0ad5bb9859..b5a1e2e296 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -2,6 +2,19 @@ This file is the authoritative registry of axioms used by Verity proof code. +## Proof-only Solidity Vault audit + +`PrintAxioms.lean` includes the imported Vault execution theorems. The focused +`solidity_importer_test.py` runs `#print axioms` in a disposable audit module for +every theorem in `Contracts/VaultFromSolidity/Proofs/Execution.lean` and requires +coverage of all declared theorems, rejecting `sorryAx` and project axioms. +Its malformed-declaration probe also checks that kernel error recovery does not +leave any partial declarations or fallback axioms in the import namespace. +The imported Vault proofs report only the standard Lean foundations `propext`, +`Classical.choice`, and `Quot.sound`; they do not depend on `solidityMappingSlot_injective`. +This does not remove the trusted Solidity frontend/translation boundary described +in `TRUST_ASSUMPTIONS.md`, or change the compiler axiom registry below. + ## Policy Axioms are exceptional. When an axiom exists, it must have: diff --git a/Contracts/VaultFromSolidity/Importer/Importer.lean b/Contracts/VaultFromSolidity/Importer/Importer.lean new file mode 100644 index 0000000000..121bfc808f --- /dev/null +++ b/Contracts/VaultFromSolidity/Importer/Importer.lean @@ -0,0 +1,849 @@ +import Lean +import Verity.Stdlib.Math +import Compiler.Sha256.Engine + +/-! +A proof-only Solidity frontend. This module invokes pinned `solc --standard-json`, +validates a closed typed-AST/storage-layout subset, and directly registers safe, +transparent Verity definitions. It emits neither an intermediate IR nor Lean source. +-/ + +open Lean Meta Elab Command + +namespace SolidityImporter + +private def solcVersionOutput := + "solc, the solidity compiler commandline interface\nVersion: 0.8.33+commit.64118f21.Linux.g++" +private def solcSha256 := "1274e5c4621ae478090c5a1f48466fd3c5f658ed9e14b15a0b213dc806215468" +private def registeredSource := "Contracts/VaultFromSolidity/Vault.sol" + +private def field (j : Json) (key : String) : MetaM Json := + match j.getObjVal? key with + | .ok v => pure v + | .error e => throwError "{e}" + +private def field? (j : Json) (key : String) : Option Json := + (j.getObjVal? key).toOption + +private def str (j : Json) : MetaM String := + match j.getStr? with + | .ok v => pure v + | .error e => throwError "{e}" + +private def nat (j : Json) : MetaM Nat := + match j.getNat? with + | .ok v => pure v + | .error e => throwError "{e}" + +private def int (j : Json) : MetaM Int := + match j.getInt? with + | .ok v => pure v + | .error e => throwError "{e}" + +private def bool (j : Json) : MetaM Bool := + match j.getBool? with + | .ok v => pure v + | .error e => throwError "{e}" + +private def arr (j : Json) : MetaM (Array Json) := + match j.getArr? with + | .ok v => pure v + | .error e => throwError "{e}" + +private def objKeys (j : Json) : MetaM (List String) := + match j with + | .obj o => pure <| o.foldl (fun keys key _ => key :: keys) [] + | _ => throwError "object expected" + +private def requireKeys (j : Json) (allowed : List String) (what : String) : MetaM Unit := do + for key in ← objKeys j do + unless key ∈ allowed do throwError "unknown {what} field {key}" + +private def nodeKind (j : Json) : MetaM String := field j "nodeType" >>= str +private def nodeId (j : Json) : MetaM Nat := field j "id" >>= nat + +private partial def collectAstIds (j : Json) : MetaM (List Nat) := do + match j with + | .obj o => + let self ← if (field? j "nodeType").isSome then do pure [← nodeId j] else pure [] + let mut ids := self + for (_, value) in o.toList do ids := ids ++ (← collectAstIds value) + pure ids + | .arr xs => + let mut ids := [] + for value in xs do ids := ids ++ (← collectAstIds value) + pure ids + | _ => pure [] + +private def expect (ok : Bool) (message : String) : MetaM Unit := + unless ok do throwError message + +private def hexDigit (n : Nat) : Char := + if n < 10 then Char.ofNat ('0'.toNat + n) else Char.ofNat ('a'.toNat + n - 10) + +private def sha256Hex (bytes : ByteArray) : String := + (Sha256Engine.sha256 bytes).data.foldl (init := "") fun acc byte => + acc.push (hexDigit (byte.toNat / 16)) |>.push (hexDigit (byte.toNat % 16)) + +private def verifyCompiler (compiler : System.FilePath) : MetaM Unit := do + let output ← IO.Process.output { cmd := "/usr/bin/sha256sum", args := #[compiler.toString] } + unless output.exitCode == 0 && (output.stdout.take 64).toString == solcSha256 do + throwError "compiler checksum mismatch" + +private structure SourceContext where + path : System.FilePath + logicalPath : String + bytes : ByteArray + sourceId : Nat + +private def parseSpan (j : Json) : MetaM (Nat × Nat × Nat) := do + let pieces := (← str (← field j "src")).splitOn ":" + match pieces with + | [a, b, c] => + let some start := a.toNat? | throwError "invalid source span" + let some size := b.toNat? | throwError "invalid source span" + let some sourceId := c.toNat? | throwError "invalid source span" + pure (start, size, sourceId) + | _ => throwError "invalid source span" + +private def failAt (ctx : SourceContext) (j : Json) (why : String) : MetaM α := do + let (start, size, _sourceId) ← parseSpan j + let before := ctx.bytes.data.extract 0 (min start ctx.bytes.size) + let (line, column) := before.foldl + (fun (p : Nat × Nat) b => if b == 10 then (p.1 + 1, 1) else (p.1, p.2 + 1)) (1, 1) + let excerptBytes : ByteArray := ⟨ctx.bytes.data.extract start (min (start + size) (min ctx.bytes.size (start + 100)))⟩ + let excerpt := String.fromUTF8? excerptBytes |>.getD "" + let kind := (← nodeKind j) + throwError "{ctx.logicalPath}:{line}:{column}: {kind}: {why}\n{excerpt}" + +private def needAt (ctx : SourceContext) (j : Json) (ok : Bool) (why : String) : MetaM Unit := + unless ok do failAt ctx j why + +private def commonFields := ["id", "src", "nodeType"] +private def expressionFields := ["isConstant", "isLValue", "isPure", "lValueRequested", "typeDescriptions"] + +private def allowedNodeFields : String → Option (List String) + | "SourceUnit" => some ["absolutePath", "exportedSymbols", "license", "nodes"] + | "PragmaDirective" => some ["literals"] + | "ContractDefinition" => some ["abstract", "baseContracts", "canonicalName", "contractDependencies", + "contractKind", "documentation", "fullyImplemented", "linearizedBaseContracts", "name", "nameLocation", + "nodes", "scope", "usedErrors", "usedEvents", "storageLayout"] + | "StructuredDocumentation" => some ["text"] + | "VariableDeclaration" => some ["constant", "functionSelector", "mutability", "name", "nameLocation", "scope", + "stateVariable", "storageLocation", "typeDescriptions", "typeName", "visibility", "value"] + | "ElementaryTypeName" => some ["name", "stateMutability", "typeDescriptions"] + | "Mapping" => some ["keyName", "keyNameLocation", "keyType", "typeDescriptions", "valueName", + "valueNameLocation", "valueType"] + | "ErrorDefinition" => some ["errorSelector", "name", "nameLocation", "parameters"] + | "FunctionDefinition" => some ["body", "functionSelector", "implemented", "kind", "modifiers", "name", + "nameLocation", "parameters", "returnParameters", "scope", "stateMutability", "virtual", "visibility", + "documentation"] + | "ParameterList" => some ["parameters"] + | "Block" => some ["statements"] + | "ExpressionStatement" => some ["expression"] + | "Assignment" => some (expressionFields ++ ["leftHandSide", "operator", "rightHandSide"]) + | "BinaryOperation" => some (expressionFields ++ ["commonType", "leftExpression", "operator", "rightExpression", "function"]) + | "Identifier" => some ["argumentTypes", "name", "overloadedDeclarations", "referencedDeclaration", "typeDescriptions"] + | "MemberAccess" => some (expressionFields ++ ["expression", "memberLocation", "memberName"]) + | "IndexAccess" => some (expressionFields ++ ["baseExpression", "indexExpression"]) + | "Literal" => some (expressionFields ++ ["hexValue", "kind", "subdenomination", "value"]) + | "FunctionCall" => some (expressionFields ++ ["arguments", "expression", "kind", "nameLocations", "names", "tryCall"]) + | "VariableDeclarationStatement" => some ["assignments", "declarations", "initialValue"] + | "IfStatement" => some ["condition", "trueBody", "falseBody"] + | "RevertStatement" => some ["errorCall"] + | "Return" => some ["expression", "functionReturnParameters"] + | _ => none + +private def requiredNodeFields : String → List String + | "SourceUnit" => ["absolutePath", "exportedSymbols", "license", "nodes"] + | "PragmaDirective" => ["literals"] + | "ContractDefinition" => ["abstract", "baseContracts", "canonicalName", "contractDependencies", + "contractKind", "fullyImplemented", "linearizedBaseContracts", "name", "nameLocation", "nodes", + "scope", "usedErrors", "usedEvents"] + | "StructuredDocumentation" => ["text"] + | "VariableDeclaration" => ["constant", "mutability", "name", "nameLocation", "scope", "stateVariable", + "storageLocation", "typeDescriptions", "typeName", "visibility"] + | "ElementaryTypeName" => ["name", "typeDescriptions"] + | "Mapping" => ["keyName", "keyNameLocation", "keyType", "typeDescriptions", "valueName", + "valueNameLocation", "valueType"] + | "ErrorDefinition" => ["errorSelector", "name", "nameLocation", "parameters"] + | "FunctionDefinition" => ["body", "functionSelector", "implemented", "kind", "modifiers", "name", + "nameLocation", "parameters", "returnParameters", "scope", "stateMutability", "virtual", "visibility"] + | "ParameterList" => ["parameters"] + | "Block" => ["statements"] + | "ExpressionStatement" => ["expression"] + | "Assignment" => expressionFields ++ ["leftHandSide", "operator", "rightHandSide"] + | "BinaryOperation" => expressionFields ++ ["commonType", "leftExpression", "operator", "rightExpression"] + | "Identifier" => ["name", "overloadedDeclarations", "referencedDeclaration", "typeDescriptions"] + | "MemberAccess" => expressionFields ++ ["expression", "memberLocation", "memberName", "typeDescriptions"] + | "IndexAccess" => expressionFields ++ ["baseExpression", "indexExpression", "typeDescriptions"] + | "Literal" => expressionFields ++ ["hexValue", "kind", "value", "typeDescriptions"] + | "FunctionCall" => expressionFields ++ ["arguments", "expression", "kind", "nameLocations", "names", + "tryCall", "typeDescriptions"] + | "VariableDeclarationStatement" => ["assignments", "declarations", "initialValue"] + | "IfStatement" => ["condition", "trueBody"] + | "RevertStatement" => ["errorCall"] + | "Return" => ["expression", "functionReturnParameters"] + | _ => [] + +private def childFields : List String := ["nodes", "baseContracts", "parameters", "returnParameters", "body", + "statements", "typeName", "keyType", "valueType", "modifiers", "overrides", "storageLayout", "leftHandSide", + "rightHandSide", "leftExpression", "rightExpression", "expression", "baseExpression", "indexExpression", + "arguments", "declarations", "initialValue", "condition", "trueBody", "falseBody", "errorCall"] + +private def validateTypeDescription (j : Json) : MetaM Unit := do + requireKeys j ["typeIdentifier", "typeString"] "type description" + let _ ← str (← field j "typeIdentifier") + let _ ← str (← field j "typeString") + +private def validateStringArray (j : Json) : MetaM Unit := do + for value in ← arr j do let _ ← str value + +private def validateNatArray (j : Json) : MetaM Unit := do + for value in ← arr j do let _ ← nat value + +private def validateAssignments (j : Json) : MetaM Unit := do + for value in ← arr j do unless value.isNull do let _ ← nat value + +private def validateExportedSymbols (j : Json) : MetaM Unit := do + match j with + | .obj entries => for (_, ids) in entries.toList do validateNatArray ids + | _ => throwError "expected exported-symbol object" + +private def validateMetadataField (ctx : SourceContext) (node : Json) (kind key : String) (value : Json) : MetaM Unit := do + if ["absolutePath", "canonicalName", "contractKind", "text", "mutability", "name", + "nameLocation", "scope", "storageLocation", "visibility", "stateMutability", "keyName", + "keyNameLocation", "valueName", "valueNameLocation", "errorSelector", "kind", "operator", + "memberLocation", "memberName", "hexValue", "value"].contains key then + if key == "scope" then let _ ← nat value + else let _ ← str value + else if ["abstract", "fullyImplemented", "constant", "stateVariable", "indexed", "implemented", + "virtual", "isConstant", "isLValue", "isPure", "lValueRequested", "tryCall"].contains key then + let _ ← bool value + else if key == "referencedDeclaration" then + let _ ← int value + else if key == "functionReturnParameters" then + let _ ← nat value + else if ["contractDependencies", "linearizedBaseContracts", "usedErrors", "usedEvents", + "baseFunctions", "overloadedDeclarations"].contains key then + validateNatArray value + else if ["literals", "nameLocations", "names"].contains key then + validateStringArray value + else if key == "assignments" then validateAssignments value + else if key == "exportedSymbols" then validateExportedSymbols value + else if ["license", "functionSelector", "subdenomination"].contains key then + unless value.isNull do let _ ← str value + else + failAt ctx node ("unvalidated AST metadata field " ++ kind ++ "." ++ key) + +private partial def validateNode (ctx : SourceContext) (j : Json) : MetaM Unit := do + let kind ← nodeKind j + let some allowed := allowedNodeFields kind | failAt ctx j "unsupported AST node" + let keys ← objKeys j + needAt ctx j (keys.all fun key => commonFields.contains key || allowed.contains key) + ("unexpected AST fields: " ++ String.intercalate ", " (keys.filter fun k => !(commonFields.contains k || allowed.contains k))) + let missing := (requiredNodeFields kind).filter fun key => !(keys.contains key) + needAt ctx j missing.isEmpty ("missing AST fields: " ++ String.intercalate ", " missing) + let _ ← nodeId j + let (start, size, sourceId) ← parseSpan j + needAt ctx j (sourceId == ctx.sourceId && start <= ctx.bytes.size && size <= ctx.bytes.size - start) + "source span outside registered source" + if let some description := field? j "typeDescriptions" then + validateTypeDescription description + if let some common := field? j "commonType" then + unless common.isNull do validateTypeDescription common + if let some arguments := field? j "argumentTypes" then + unless arguments.isNull do + for description in ← arr arguments do validateTypeDescription description + if let some documentation := field? j "documentation" then + if documentation.isNull then pure () + else match documentation with + | .str _ => pure () + | .obj _ => + needAt ctx j ((← nodeKind documentation) == "StructuredDocumentation") "invalid documentation" + validateNode ctx documentation + | _ => failAt ctx j "invalid documentation" + for key in keys do + unless commonFields.contains key || childFields.contains key || + ["typeDescriptions", "commonType", "argumentTypes", "documentation"].contains key || + (kind == "VariableDeclaration" && key == "value") do + try validateMetadataField ctx j kind key (← field j key) + catch _ => failAt ctx j ("invalid AST metadata field " ++ kind ++ "." ++ key) + if kind == "ContractDefinition" then + needAt ctx j ((field? j "storageLayout").all Json.isNull) "contract layout at specifier unsupported" + if kind == "VariableDeclaration" then + needAt ctx j ((field? j "value").all Json.isNull && (field? j "overrides").all Json.isNull) + "initializer/override unsupported" + if kind == "BinaryOperation" then + needAt ctx j ((field? j "function").all Json.isNull) "user-defined operator unsupported" + if kind == "FunctionCall" then + needAt ctx j ((← str (← field j "kind")) == "functionCall" && !(← bool (← field j "tryCall")) && + (← arr (← field j "names")).isEmpty) "unsupported call surface" + for key in childFields do + if let some value := field? j key then + if key == "storageLayout" && kind == "ContractDefinition" then pure () + else if value.isNull then pure () + else match value with + | .arr values => for child in values do validateNode ctx child + | .obj _ => validateNode ctx value + | _ => failAt ctx j ("invalid AST child: " ++ key) + let requireKind (key : String) (kinds : List String) : MetaM Unit := do + let child ← field j key + needAt ctx j (kinds.contains (← nodeKind child)) ("unexpected child kind: " ++ key) + match kind with + | "SourceUnit" => + let _ ← arr (← field j "nodes") + | "ContractDefinition" => + let _ ← arr (← field j "nodes"); let _ ← arr (← field j "baseContracts") + | "FunctionDefinition" => + requireKind "body" ["Block"] + requireKind "parameters" ["ParameterList"] + requireKind "returnParameters" ["ParameterList"] + let _ ← arr (← field j "modifiers") + | "ParameterList" => + for p in (← arr (← field j "parameters")) do + needAt ctx j ((← nodeKind p) == "VariableDeclaration") "invalid parameter declaration" + | "Block" => let _ ← arr (← field j "statements") + | "VariableDeclaration" => requireKind "typeName" ["ElementaryTypeName", "Mapping"] + | "Mapping" => requireKind "keyType" ["ElementaryTypeName"]; requireKind "valueType" ["ElementaryTypeName"] + | "ExpressionStatement" => let _ ← field j "expression" + | "Assignment" => let _ ← field j "leftHandSide"; let _ ← field j "rightHandSide" + | "BinaryOperation" => let _ ← field j "leftExpression"; let _ ← field j "rightExpression" + | "MemberAccess" => let _ ← field j "expression" + | "IndexAccess" => let _ ← field j "baseExpression"; let _ ← field j "indexExpression" + | "FunctionCall" => let _ ← field j "expression"; let _ ← arr (← field j "arguments") + | "VariableDeclarationStatement" => + for d in (← arr (← field j "declarations")) do + needAt ctx j ((← nodeKind d) == "VariableDeclaration") "invalid local declaration" + let _ ← field j "initialValue" + | "IfStatement" => requireKind "trueBody" ["Block"] + | "RevertStatement" => requireKind "errorCall" ["FunctionCall"] + | "Return" => let _ ← field j "expression" + | "ErrorDefinition" => requireKind "parameters" ["ParameterList"] + | _ => pure () + +private structure FieldInfo where + id : Nat + name : String + getter : Option String + slot : Nat + mapping : Bool + +private structure Frontend where + source : SourceContext + ast : Json + fields : List FieldInfo + errors : List (Nat × String) + functions : List Json + digest : String + +private def validName (name : String) : Bool := + match name.toList with + | [] => false + | c :: cs => c.isAlpha && cs.all (fun c => c.isAlphanum || c == '_') && name != "sourceDigest" + +private def identifier (ctx : SourceContext) (j : Json) : MetaM String := do + let name ← str (← field j "name") + needAt ctx j (validName name) "unsupported/reserved name" + pure name + +private def typeString (j : Json) : MetaM String := + field j "typeDescriptions" >>= (field · "typeString") >>= str + +set_option maxRecDepth 2048 in +private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : String) + (raw : ByteArray) (outputText version importerText : String) : MetaM Frontend := do + let output ← match Json.parse outputText with + | .ok j => pure j + | .error e => throwError "invalid solc standard JSON: {e}" + requireKeys output ["contracts", "sources", "errors"] "solc output" + if let some errors := field? output "errors" then + for e in (← arr errors) do + requireKeys e ["component", "errorCode", "formattedMessage", "message", "severity", + "sourceLocation", "type"] "compiler diagnostic" + if (← str (← field e "severity")) == "error" then + throwError "{← str (← field e "formattedMessage")}" + let sources ← field output "sources" + let sourceKeys ← objKeys sources + expect (sourceKeys == [logicalPath]) "unexpected compiler sources" + let sourceOut ← field sources logicalPath + requireKeys sourceOut ["ast", "id"] "source output" + let sourceId ← nat (← field sourceOut "id") + let ast ← field sourceOut "ast" + let ctx := { path := sourcePath, logicalPath, bytes := raw, sourceId } + needAt ctx ast ((← nodeKind ast) == "SourceUnit") "root must be SourceUnit" + validateNode ctx ast + needAt ctx ast ((← str (← field ast "absolutePath")) == logicalPath) + "source-unit path mismatch" + let ids ← collectAstIds ast + needAt ctx ast (ids.length == ids.eraseDups.length) "duplicate Solidity AST node ID" + let mut contracts : List Json := [] + for node in (← arr (← field ast "nodes")) do + match ← nodeKind node with + | "PragmaDirective" => + let literals ← arr (← field node "literals") + needAt ctx node (literals.size == 4 && (← str literals[0]!) == "solidity" && + (← str literals[1]!) == "^" && (← str literals[2]!) == "0.8" && + (← str literals[3]!) == ".33") "unsupported pragma" + | "ContractDefinition" => contracts := node :: contracts + | _ => failAt ctx node "unsupported source declaration" + needAt ctx ast (contracts.length == 1) "exactly one concrete contract required" + let contract := contracts.head! + let contractId ← nodeId contract + needAt ctx contract ((← str (← field contract "contractKind")) == "contract" && + !(← bool (← field contract "abstract")) && (← bool (← field contract "fullyImplemented")) && + (← arr (← field contract "baseContracts")).isEmpty && + (← arr (← field contract "contractDependencies")).isEmpty && + (← arr (← field contract "usedEvents")).isEmpty) + "inheritance/abstract contract unsupported" + let linearized ← arr (← field contract "linearizedBaseContracts") + needAt ctx contract (linearized.size == 1 && (← nat linearized[0]!) == contractId) + "invalid contract linearization" + let contractName ← str (← field contract "name") + needAt ctx contract ((← str (← field contract "canonicalName")) == contractName && + (← nat (← field contract "scope")) == (← nodeId ast)) "contract identity mismatch" + let exports ← field ast "exportedSymbols" + needAt ctx ast ((← objKeys exports) == [contractName]) "exported symbol mismatch" + let exportedIds ← arr (← field exports contractName) + needAt ctx ast (exportedIds.size == 1 && (← nat exportedIds[0]!) == contractId) + "exported symbol mismatch" + let compilerContracts ← field output "contracts" + expect ((← objKeys compilerContracts) == [logicalPath]) "unexpected compiler contract sources" + let sourceContracts ← field compilerContracts logicalPath + expect ((← objKeys sourceContracts) == [contractName]) "unexpected compiler contracts" + let contractOut ← field sourceContracts contractName + requireKeys contractOut ["storageLayout"] "contract output" + let layout ← field contractOut "storageLayout" + requireKeys layout ["storage", "types"] "storage layout" + let storage ← arr (← field layout "storage") + let layoutTypes ← field layout "types" + let layoutTypeKeys ← objKeys layoutTypes + expect (layoutTypeKeys.length == 3 && layoutTypeKeys.all fun key => + ["t_address", "t_uint256", "t_mapping(t_address,t_uint256)"].contains key) + "unexpected storage type table" + let mut fields : List FieldInfo := [] + let mut errors : List (Nat × String) := [] + let mut functions : List Json := [] + for node in (← arr (← field contract "nodes")) do + match ← nodeKind node with + | "VariableDeclaration" => + let name ← identifier ctx node + needAt ctx node ((← bool (← field node "stateVariable")) && !(← bool (← field node "constant")) && + (← str (← field node "mutability")) == "mutable" && (field? node "value").all Json.isNull && + (← str (← field node "storageLocation")) == "default" && + (← nat (← field node "scope")) == contractId) "initializer/constant/transient field unsupported" + let typ ← typeString node + needAt ctx node (typ == "uint256" || typ == "mapping(address => uint256)") "unsupported storage type" + let id ← nodeId node + let some entry := storage.find? fun e => (field? e "astId").bind (·.getNat?.toOption) == some id + | failAt ctx node "missing storage layout" + requireKeys entry ["astId", "contract", "label", "offset", "slot", "type"] "storage entry" + needAt ctx node ((← str (← field entry "contract")) == s!"{logicalPath}:{contractName}" && + (← str (← field entry "label")) == name) "storage declaration mismatch" + needAt ctx node ((← nat (← field entry "offset")) == 0) "missing/packed layout" + let typeId ← str (← field entry "type") + let layoutType ← field layoutTypes typeId + let expectedTypeKeys := if typ == "uint256" then + ["encoding", "label", "numberOfBytes"] + else ["encoding", "key", "label", "numberOfBytes", "value"] + requireKeys layoutType expectedTypeKeys "storage type" + needAt ctx node ((← str (← field layoutType "numberOfBytes")) == "32") "nonword layout" + if typ == "uint256" then + needAt ctx node ((← str (← field layoutType "encoding")) == "inplace" && + (← str (← field layoutType "label")) == typ) "bad scalar layout" + else + let keyType ← field layoutTypes (← str (← field layoutType "key")) + let valueType ← field layoutTypes (← str (← field layoutType "value")) + requireKeys keyType ["encoding", "label", "numberOfBytes"] "mapping key type" + requireKeys valueType ["encoding", "label", "numberOfBytes"] "mapping value type" + let layoutEncoding ← str (← field layoutType "encoding") + let keyEncoding ← str (← field keyType "encoding") + let keyLabel ← str (← field keyType "label") + let keyBytes ← str (← field keyType "numberOfBytes") + let valueEncoding ← str (← field valueType "encoding") + let valueLabel ← str (← field valueType "label") + let valueBytes ← str (← field valueType "numberOfBytes") + needAt ctx node (layoutEncoding == "mapping" && keyEncoding == "inplace" && + keyLabel == "address" && keyBytes == "20" && valueEncoding == "inplace" && + valueLabel == "uint256" && valueBytes == "32") "bad mapping layout" + let getter := if (← str (← field node "visibility")) == "public" then some name else none + let slotText ← str (← field entry "slot") + let some slot := slotText.toNat? | failAt ctx node "invalid storage slot" + fields := FieldInfo.mk id (name ++ "Slot") getter slot (typ.startsWith "mapping") :: fields + | "ErrorDefinition" => + let ps ← arr (← field (← field node "parameters") "parameters") + needAt ctx node ps.isEmpty "only zero-argument custom errors" + errors := ((← nodeId node), (← identifier ctx node)) :: errors + | "FunctionDefinition" => + needAt ctx node ((← nat (← field node "scope")) == contractId) "function scope mismatch" + functions := node :: functions + | _ => failAt ctx node "unsupported contract declaration" + needAt ctx contract (storage.size == fields.length && storage.all fun e => + (field? e "astId").bind (·.getNat?.toOption) |>.any fun id => fields.any (·.id == id)) "unaccounted layout field" + let names := fields.flatMap fun f => f.name :: f.getter.toList + needAt ctx contract (names.length == names.eraseDups.length) "storage/generated name collision" + let slots := fields.map (·.slot) + needAt ctx contract (slots.length == slots.eraseDups.length) "storage slot collision" + let usedErrors ← arr (← field contract "usedErrors") + let mut usedErrorIds : List Nat := [] + for errorId in usedErrors do usedErrorIds := (← nat errorId) :: usedErrorIds + let errorIds := errors.map (·.1) + needAt ctx contract (usedErrorIds.length == errorIds.length && + usedErrorIds.all fun id => errorIds.contains id) "custom error reference mismatch" + let sourceText := String.fromUTF8? raw |>.getD "" + let digest := sha256Hex (sourceText ++ outputText ++ importerText ++ solcSha256 ++ version).toUTF8 + pure <| Frontend.mk ctx ast fields.reverse errors functions.reverse digest + +private def uint := mkConst ``Verity.Core.Uint256 +private def address := mkConst ``Verity.Core.Address +private def unit := mkConst ``Unit +private def valueType (s : String) : MetaM Expr := + match s with + | "uint256" => pure uint + | "address" => pure address + | "unit" => pure unit + | _ => throwError "unsupported type {s}" + +private def ret (x : Expr) : MetaM Expr := mkAppM ``Verity.pure #[x] +private def seq (m t : Expr) (k : Expr → MetaM Expr) : MetaM Expr := + withLocalDeclD `value t fun x => do + let next ← k x + mkAppM ``Verity.bind #[m, ← mkLambdaFVars #[x] next] + +private def register (name : Name) (value : Expr) : MetaM Unit := do + if (← getEnv).contains name then throwError "declaration collision: {name}" + let value ← instantiateMVars value + let type ← instantiateMVars (← inferType value) + if value.hasMVar || value.hasFVar || type.hasMVar || type.hasFVar then + throwError "unclosed imported declaration {name}" + addDecl (.defnDecl { name, levelParams := [], type, value, hints := .regular 0, safety := .safe }) + (forceExpose := true) + compileDecls #[name] (logErrors := false) + +private abbrev Locals := List (Nat × String × Expr) +private abbrev Slots := List (Nat × Expr) + +private def lookupLocal (locals : Locals) (id : Nat) : Option (String × Expr) := + (locals.find? fun x => x.1 == id).map fun x => (x.2.1, x.2.2) + +private def lookupSlot (slots : Slots) (id : Nat) : MetaM Expr := + match slots.lookup id with + | some e => pure e + | none => throwError "unresolved declaration id {id}" + +private def checked (op : String) (a b : Expr) : MetaM Expr := do + let fn ← match op with + | "+" | "+=" => pure ``Verity.Stdlib.Math.safeAdd + | "-" | "-=" => pure ``Verity.Stdlib.Math.safeSub + | _ => throwError "unsupported arithmetic {op}" + mkAppM ``Verity.Stdlib.Math.requireSomeUint #[← mkAppM fn #[a, b], mkStrLit "Panic(0x11)"] + +private def requireType (frontend : Frontend) (j : Json) (expected : String) : MetaM Unit := do + let actual ← typeString j + let identifier ← str (← field (← field j "typeDescriptions") "typeIdentifier") + let expectedIdentifier := match expected with + | "uint256" => "t_uint256" + | "address" => "t_address" + | "mapping(address => uint256)" => "t_mapping$_t_address_$_t_uint256_$" + | "msg" => "t_magic_message" + | "bool" => "t_bool" + | _ => "" + needAt frontend.source j (actual == expected && identifier == expectedIdentifier) ("expected " ++ expected) + +private partial def translateExpr (frontend : Frontend) (slots : Slots) (locals : Locals) (j : Json) + (k : Expr → MetaM Expr) : MetaM Expr := do + match ← nodeKind j with + | "Identifier" => + let rid ← int (← field j "referencedDeclaration") + if rid < 0 then failAt frontend.source j "unresolved builtin identifier" + let id := rid.toNat + if let some (typ, value) := lookupLocal locals id then + requireType frontend j typ + k value + else + let some info := frontend.fields.find? (·.id == id) + | failAt frontend.source j "unresolved declaration reference" + needAt frontend.source j (!info.mapping) "mapping requires index access" + requireType frontend j "uint256" + seq (← mkAppM ``Verity.getStorage #[← lookupSlot slots id]) uint k + | "MemberAccess" => + let base ← field j "expression" + needAt frontend.source j ((← str (← field j "memberName")) == "sender" && + (← nodeKind base) == "Identifier" && (← str (← field base "name")) == "msg" && + (← int (← field base "referencedDeclaration")) == -15 && + (field? j "referencedDeclaration").all Json.isNull) "only builtin msg.sender supported" + requireType frontend base "msg" + requireType frontend j "address" + seq (mkConst ``Verity.msgSender) address k + | "IndexAccess" => + let base ← field j "baseExpression" + needAt frontend.source j ((← nodeKind base) == "Identifier") "unsupported index base" + let rid ← int (← field base "referencedDeclaration") + let some info := if rid < 0 then none else frontend.fields.find? (·.id == rid.toNat) + | failAt frontend.source j "unsupported index base" + needAt frontend.source j info.mapping "unsupported index base" + requireType frontend base "mapping(address => uint256)" + let index ← field j "indexExpression" + requireType frontend index "address" + requireType frontend j "uint256" + translateExpr frontend slots locals index fun key => do + let slot ← lookupSlot slots info.id + seq (← mkAppM ``Verity.getMapping #[slot, key]) uint k + | "Literal" => + let value ← str (← field j "value") + let some n := value.toNat? | failAt frontend.source j "unsupported literal" + needAt frontend.source j ((← str (← field j "kind")) == "number" && + (field? j "subdenomination").all Json.isNull && n < 2^256) "unsupported literal" + needAt frontend.source j ((← typeString j).startsWith "int_const ") "unsupported literal type" + k (← mkAppM ``Verity.Core.Uint256.ofNat #[mkNatLit n]) + | "BinaryOperation" => + let op ← str (← field j "operator") + needAt frontend.source j (op == "+" || op == "-") "unsupported binary operation/types" + requireType frontend j "uint256" + let left ← field j "leftExpression" + let right ← field j "rightExpression" + requireType frontend left "uint256"; requireType frontend right "uint256" + translateExpr frontend slots locals left fun a => do + translateExpr frontend slots locals right fun b => do + seq (← checked op a b) uint k + | _ => failAt frontend.source j "unsupported expression" + +private def translateLValue (frontend : Frontend) (slots : Slots) (locals : Locals) (j : Json) + (k : Expr → Option Expr → MetaM Expr) : MetaM Expr := do + match ← nodeKind j with + | "Identifier" => + let rid ← int (← field j "referencedDeclaration") + let some info := if rid < 0 then none else frontend.fields.find? (·.id == rid.toNat) + | failAt frontend.source j "unsupported storage lvalue" + needAt frontend.source j (!info.mapping) "mapping requires index access" + requireType frontend j "uint256" + k (← lookupSlot slots info.id) none + | "IndexAccess" => + let base ← field j "baseExpression" + needAt frontend.source j ((← nodeKind base) == "Identifier") "unsupported index base" + let rid ← int (← field base "referencedDeclaration") + let some info := if rid < 0 then none else frontend.fields.find? (·.id == rid.toNat) + | failAt frontend.source j "unsupported index base" + needAt frontend.source j info.mapping "unsupported index base" + requireType frontend base "mapping(address => uint256)" + let index ← field j "indexExpression" + requireType frontend index "address" + requireType frontend j "uint256" + translateExpr frontend slots locals index fun key => do + k (← lookupSlot slots info.id) (some key) + | _ => failAt frontend.source j "only storage assignment supported" + +private partial def translateStmts (frontend : Frontend) (slots : Slots) (locals : Locals) + (returns : String) (nodes : List Json) : MetaM Expr := do + match nodes with + | [] => + if returns == "unit" then ret (mkConst ``Unit.unit) + else throwError "missing terminal return" + | node :: rest => + match ← nodeKind node with + | "ExpressionStatement" => + let assignment ← field node "expression" + needAt frontend.source node ((← nodeKind assignment) == "Assignment") "unsupported expression statement" + requireType frontend assignment "uint256" + let op ← str (← field assignment "operator") + needAt frontend.source assignment (op == "=" || op == "+=" || op == "-=") "unsupported assignment" + translateLValue frontend slots locals (← field assignment "leftHandSide") fun slot key => do + let write (value : Expr) : MetaM Expr := do + let action ← match key with + | none => mkAppM ``Verity.setStorage #[slot, value] + | some index => mkAppM ``Verity.setMapping #[slot, index, value] + seq action unit fun _ => translateStmts frontend slots locals returns rest + let rhsNode ← field assignment "rightHandSide" + if op == "=" then translateExpr frontend slots locals rhsNode write + else + let read ← match key with + | none => mkAppM ``Verity.getStorage #[slot] + | some index => mkAppM ``Verity.getMapping #[slot, index] + seq read uint fun old => do + translateExpr frontend slots locals rhsNode fun rhs => do + seq (← checked op old rhs) uint write + | "VariableDeclarationStatement" => + let declarations ← arr (← field node "declarations") + needAt frontend.source node (declarations.size == 1) "unsupported locals" + let declaration := declarations[0]! + needAt frontend.source declaration (!(← bool (← field declaration "stateVariable")) && + !(← bool (← field declaration "constant")) && + (← str (← field declaration "mutability")) == "mutable" && + (← str (← field declaration "storageLocation")) == "default" && + (← str (← field declaration "visibility")) == "internal") "unsupported local declaration" + requireType frontend declaration "uint256" + let id ← nodeId declaration + let _ ← identifier frontend.source declaration + let initialValue ← field node "initialValue" + translateExpr frontend slots locals initialValue fun value => + translateStmts frontend slots ((id, "uint256", value) :: locals) returns rest + | "IfStatement" => + let falseBody := field? node "falseBody" + let trueBody ← field node "trueBody" + let statements ← arr (← field trueBody "statements") + needAt frontend.source node (falseBody.all Json.isNull && statements.size == 1 && + (← nodeKind statements[0]!) == "RevertStatement") "only if/revert guard supported" + let call ← field statements[0]! "errorCall" + let callee ← field call "expression" + let rid ← int (← field callee "referencedDeclaration") + let some errorName := if rid < 0 then none else frontend.errors.lookup rid.toNat + | failAt frontend.source node "unsupported revert" + needAt frontend.source node ((← nodeKind callee) == "Identifier" && + (← arr (← field call "arguments")).isEmpty) "unsupported revert" + let condition ← field node "condition" + needAt frontend.source condition ((← nodeKind condition) == "BinaryOperation" && + (← str (← field condition "operator")) == "<") "only uint256 comparison guard supported" + requireType frontend condition "bool" + let commonType ← field condition "commonType" + needAt frontend.source condition ((← str (← field commonType "typeString")) == "uint256" && + (← str (← field commonType "typeIdentifier")) == "t_uint256") "unsupported comparison type" + let left ← field condition "leftExpression" + let right ← field condition "rightExpression" + requireType frontend left "uint256"; requireType frontend right "uint256" + translateExpr frontend slots locals left fun a => + translateExpr frontend slots locals right fun b => do + let av ← mkAppM ``Verity.Core.Uint256.val #[a] + let bv ← mkAppM ``Verity.Core.Uint256.val #[b] + let allowed ← mkAppM ``Nat.ble #[bv, av] + let guard ← mkAppM ``Verity.require #[allowed, mkStrLit (errorName ++ "()")] + seq guard unit fun _ => translateStmts frontend slots locals returns rest + | "Return" => + needAt frontend.source node (rest.isEmpty && returns == "uint256") "only terminal scalar return" + translateExpr frontend slots locals (← field node "expression") ret + | _ => failAt frontend.source node "unsupported statement" + +private def nonpayable (m : Expr) : MetaM Expr := + seq (mkConst ``Verity.msgValue) uint fun value => do + let n ← mkAppM ``Verity.Core.Uint256.val #[value] + let zero ← mkAppM ``Nat.beq #[n, mkNatLit 0] + let guard ← mkAppM ``Verity.require #[zero, mkStrLit "Nonpayable"] + seq guard unit fun _ => pure m + +private def validateValueDecl (frontend : Frontend) (p : Json) : MetaM Unit := do + needAt frontend.source p (!(← bool (← field p "stateVariable")) && + !(← bool (← field p "constant")) && + (← str (← field p "mutability")) == "mutable" && + (← str (← field p "storageLocation")) == "default" && + (← str (← field p "visibility")) == "internal" && + (field? p "value").all Json.isNull) "unsupported parameter declaration" + +private partial def translateParams (frontend : Frontend) (params : List Json) (locals : Locals) + (k : Locals → MetaM Expr) : MetaM Expr := do + match params with + | [] => k locals + | p :: ps => + validateValueDecl frontend p + let typ ← typeString p + needAt frontend.source p (typ == "uint256" || typ == "address") "unsupported value type" + let name ← identifier frontend.source p + let id ← nodeId p + withLocalDeclD (Name.mkSimple name) (← valueType typ) fun x => do + mkLambdaFVars #[x] (← translateParams frontend ps ((id, typ, x) :: locals) k) + +private def importFrontend (ns : Name) (frontend : Frontend) : MetaM Unit := do + if debug.skipKernelTC.get (← getOptions) then throwError "kernel checking must be enabled" + let mut names := #[ns ++ `sourceDigest] + for f in frontend.fields do + names := names.push (ns ++ Name.mkSimple f.name) + if let some getter := f.getter then names := names.push (ns ++ Name.mkSimple getter) + for fn in frontend.functions do + let name ← identifier frontend.source fn + names := names.push (ns ++ Name.mkSimple name) + for i in [:names.size] do + if (← getEnv).contains names[i]! || (names.extract 0 i).contains names[i]! then + throwError "declaration collision: {names[i]!}" + let mut slots : Slots := [] + for f in frontend.fields do + let ty ← if f.mapping then mkArrow address uint else pure uint + let slot ← mkAppOptM ``Verity.StorageSlot.mk #[some ty, some (mkNatLit f.slot)] + let name := ns ++ Name.mkSimple f.name + register name slot + slots := (f.id, mkConst name) :: slots + for f in frontend.fields do + if let some getter := f.getter then + let slot ← lookupSlot slots f.id + let value ← if f.mapping then + withLocalDeclD `account address fun account => do + let getter ← mkAppM ``Verity.getMapping #[slot, account] + mkLambdaFVars #[account] (← nonpayable getter) + else nonpayable (← mkAppM ``Verity.getStorage #[slot]) + register (ns ++ Name.mkSimple getter) value + for fn in frontend.functions do + let name ← identifier frontend.source fn + needAt frontend.source fn ((← str (← field fn "kind")) == "function" && + (← bool (← field fn "implemented")) && (← arr (← field fn "modifiers")).isEmpty && + !(← bool (← field fn "virtual")) && (field? fn "overrides").all Json.isNull && + ["external", "public"].contains (← str (← field fn "visibility")) && + ["nonpayable", "view"].contains (← str (← field fn "stateMutability"))) "unsupported function surface" + let ps ← arr (← field (← field fn "parameters") "parameters") + let rs ← arr (← field (← field fn "returnParameters") "parameters") + needAt frontend.source fn (ps.size <= 1 && rs.size <= 1) "unsupported signature" + for r in rs do + validateValueDecl frontend r + needAt frontend.source r ((← str (← field r "name")).isEmpty && (← typeString r) == "uint256") + "unsupported return type" + let returns := if rs.isEmpty then "unit" else "uint256" + let value ← translateParams frontend ps.toList [] fun locals => do + let code ← translateStmts frontend slots locals returns + (← arr (← field (← field fn "body") "statements")).toList + let expected ← mkAppM ``Verity.Contract #[← valueType returns] + unless ← isDefEq (← inferType code) expected do + throwError "imported body does not match typed AST return signature" + nonpayable code + register (ns ++ Name.mkSimple name) value + register (ns ++ `sourceDigest) (mkStrLit frontend.digest) + +private def compileFrontend (root source : System.FilePath) : MetaM Frontend := do + let canonicalRoot ← IO.FS.realPath root + let canonicalSource ← IO.FS.realPath source + unless canonicalSource.toString.startsWith (canonicalRoot.toString ++ "/") do + throwError "source outside package" + let expected ← IO.FS.realPath (canonicalRoot / registeredSource) + unless canonicalSource == expected do throwError "unregistered source or source outside package" + let compiler := canonicalRoot / ".lake/solidity-import/solc" + verifyCompiler compiler + let versionOut ← IO.Process.output { cmd := compiler.toString, args := #["--version"] } + unless versionOut.exitCode == 0 && versionOut.stdout.trimAscii.toString == solcVersionOutput do + throwError "compiler version mismatch" + verifyCompiler compiler + let sourceBytes ← IO.FS.readBinFile canonicalSource + let sourceText ← match String.fromUTF8? sourceBytes with + | some text => pure text + | none => throwError "Solidity source is not UTF-8" + let settings := Json.mkObj [ + ("optimizer", Json.mkObj [("enabled", false)]), + ("viaIR", false), ("evmVersion", "cancun"), ("remappings", Json.arr #[]), + ("outputSelection", Json.mkObj [("*", Json.mkObj [ + ("", Json.arr #["ast"]), ("*", Json.arr #["storageLayout"])])])] + let input := Json.mkObj [("language", "Solidity"), + ("sources", Json.mkObj [(registeredSource, Json.mkObj [("content", sourceText)])]), + ("settings", settings)] + let output ← IO.Process.output + { cmd := compiler.toString, args := #["--standard-json", "--no-import-callback"] } + (some input.compress) + unless output.exitCode == 0 do throwError "solc failed: {output.stderr}" + verifyCompiler compiler + let importerText ← IO.FS.readFile + (canonicalRoot / "Contracts/VaultFromSolidity/Importer/Importer.lean") + parseCompilerOutput canonicalSource registeredSource sourceBytes output.stdout versionOut.stdout importerText + +syntax (name := solidityContract) "solidity_contract " ident " from " str : command + +@[command_elab solidityContract] def elabSolidityContract : CommandElab := fun stx => do + let saved ← getEnv + try + let authored ← IO.FS.realPath (← getFileName) + let source := authored.parent.getD "." / stx[3].isStrLit?.get! + let mut root := authored.parent.getD "." + while !(← (root / "lakefile.lean").pathExists) do + let some parent := root.parent | throwError "package root not found" + if parent == root then throwError "package root not found" + root := parent + let frontend ← liftTermElabM <| compileFrontend root source + let ns := (← getCurrNamespace) ++ stx[1].getId + liftTermElabM <| withOptions (Elab.async.set · false) (importFrontend ns frontend) + catch e => + setEnv saved + throw e + +end SolidityImporter diff --git a/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py b/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py new file mode 100644 index 0000000000..4da220b795 --- /dev/null +++ b/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py @@ -0,0 +1,419 @@ +#!/usr/bin/env python3 +"""Acceptance checks for the Lean-only Solidity frontend. + +Python only orchestrates disposable builds and mutations. The production import +path is `Contracts/VaultFromSolidity/Importer/Importer.lean` -> pinned solc -> checked Lean declarations. +""" + +import hashlib +import os +from pathlib import Path +import re +import shutil +import subprocess +import tempfile + +ROOT = Path(__file__).resolve().parents[4] + + +def lake_binary() -> str: + found = shutil.which("lake") + if found: + return found + version = (ROOT / "lean-toolchain").read_text().strip().split(":")[-1] + candidates = [ + Path.home() / ".elan/toolchains" / f"leanprover--lean4---{version}" / "bin/lake", + Path("/home/claudine/.hermes/profiles/claudine/home/.elan/toolchains") + / f"leanprover--lean4---{version}" / "bin/lake", + ] + for candidate in candidates: + if candidate.is_file(): + return str(candidate) + raise RuntimeError("lake executable not found") + + +LAKE = lake_binary() +ENV = dict(os.environ) + + +def check(ok: bool, message: str) -> None: + if not ok: + raise AssertionError(message) + print("PASS " + message, flush=True) + + +def run(root: Path, args: list[str], success: bool = True, contains: str | None = None) -> str: + process = subprocess.run( + args, cwd=root, env=ENV, text=True, capture_output=True, timeout=300 + ) + output = process.stdout + process.stderr + if (process.returncode == 0) != success or (contains and contains not in output) or "PANIC" in output: + raise AssertionError(f"{args}: exit {process.returncode}\n{output}") + return output + + +def main() -> None: + importer_path = ROOT / "Contracts/VaultFromSolidity/Importer/Importer.lean" + importer_text = importer_path.read_text() + python_frontend = ROOT / "Contracts/VaultFromSolidity/Importer/scripts/solidity_importer.py" + check(not python_frontend.exists(), "no Python importer/frontend exists") + check("--standard-json" in importer_text and "--no-import-callback" in importer_text, + "Lean importer invokes pinned solc standard JSON with import callback disabled") + check("solcSha256" in importer_text and "compiler checksum mismatch" in importer_text, + "Lean importer enforces compiler checksum and version pin") + check('cmd := "/usr/bin/sha256sum"' in importer_text and 'cmd := "sha256sum"' not in importer_text, + "compiler checksum utility uses a fixed path, not PATH lookup") + check("translateExpr" in importer_text and "translateStmts" in importer_text, + "Solidity constructs have explicit Lean translation functions") + check(all(tag not in importer_text for tag in ('[\"read\"', '[\"write\"', '[\"guard\"')), + "no custom serialized JSON IR tags") + + with tempfile.TemporaryDirectory(prefix="verity-vault-check-", dir=ROOT.parent) as directory: + root = Path(directory) + for name in ("Verity", "Compiler", "Contracts", "scripts"): + shutil.copytree(ROOT / name, root / name) + for name in ("lakefile.lean", "lake-manifest.json", "lean-toolchain"): + shutil.copy2(ROOT / name, root / name) + shutil.copytree(ROOT / ".lake/build", root / ".lake/build") + (root / ".lake/solidity-import").mkdir(parents=True) + shutil.copy2(ROOT / ".lake/solidity-import/solc", root / ".lake/solidity-import/solc") + (root / ".lake/packages").symlink_to(ROOT / ".lake/packages", target_is_directory=True) + + source = root / "Contracts/VaultFromSolidity/Vault.sol" + original = source.read_bytes() + source_stamp = source.stat() + importer = root / "Contracts/VaultFromSolidity/Importer/Importer.lean" + importer_original = importer.read_bytes() + importer_stamp = importer.stat() + compiler = root / ".lake/solidity-import/solc" + compiler_original = compiler.read_bytes() + lean_sources = set(root.rglob("*.lean")) + + def edit_source(data: bytes) -> None: + source.write_bytes(data) + os.utime(source, ns=(source_stamp.st_atime_ns, source_stamp.st_mtime_ns)) + + def build(success: bool = True, contains: str | None = None) -> str: + return run(root, [LAKE, "build", "VaultFromSolidity"], success, contains) + + def artifacts() -> dict[str, tuple[int, str]]: + paths = list((root / ".lake/build/lib/lean/Contracts/VaultFromSolidity").rglob("*.olean")) + return { + str(path.relative_to(root)): ( + path.stat().st_mtime_ns, + hashlib.sha256(path.read_bytes()).hexdigest(), + ) + for path in paths + } + + def source_digest() -> str: + digest_probe = root / ".lake/solidity-import/SourceDigestProbe.lean" + try: + digest_probe.write_text( + "import Contracts.VaultFromSolidity.VaultFromSolidity\n" + "#eval Contracts.VaultFromSolidity.sourceDigest\n" + ) + output = run(root, [LAKE, "env", "lean", str(digest_probe)]) + match = re.search(r'"([0-9a-f]{64})"', output) + if match is None: + raise AssertionError("sourceDigest is not an auditable SHA-256 value") + check(True, "sourceDigest is an auditable SHA-256 value") + return match.group(1) + finally: + digest_probe.unlink(missing_ok=True) + + build() + check(True, "baseline lake build VaultFromSolidity") + + ux_probe = root / "Contracts/VaultFromSolidity/FrontendProbe.lean" + try: + ux_probe.write_text('''import Contracts.VaultFromSolidity.Importer.Importer +solidity_contract Vault from "Vault.sol" +#print Vault.deposit +''') + ux_output = run(root, [LAKE, "env", "lean", str(ux_probe)]) + check("def Vault.deposit" in ux_output and "Verity.setStorage" in ux_output, + "documented solidity_contract Vault UX exposes #print Vault.deposit") + finally: + ux_probe.unlink(missing_ok=True) + + proof = root / "Contracts/VaultFromSolidity/Proofs/Execution.lean" + proof_text = proof.read_text() + theorem_names = re.findall(r"^theorem\s+(\w+)", proof_text, re.M) + audit_file = root / ".lake/solidity-import/AxiomAudit.lean" + try: + audit_file.write_text( + "import Contracts.VaultFromSolidity.Proofs.Execution\n" + + "\n".join( + "#print axioms Contracts.VaultFromSolidity.Proofs.Execution." + name + for name in theorem_names + ) + + "\n" + ) + audit = run(root, [LAKE, "env", "lean", str(audit_file)]) + finally: + audit_file.unlink(missing_ok=True) + entries = re.findall( + r"'Contracts.VaultFromSolidity.Proofs.Execution.(\w+)' depends on axioms: \[([^\]]*)\]", audit + ) + check(set(theorem_names) == {name for name, _ in entries}, + "every theorem appears in actual #print axioms output") + axioms = {a.strip() for _, values in entries for a in values.split(",") if a.strip()} + check(axioms <= {"propext", "Quot.sound", "Classical.choice"}, + "no project axioms or sorryAx: " + ", ".join(sorted(axioms))) + + probe = root / ".lake/solidity-import/RegistrationProbe.lean" + try: + probe.write_text('''import Contracts.VaultFromSolidity.VaultFromSolidity +open Lean Elab Command +#print Contracts.VaultFromSolidity.deposit +run_cmd do + for suffix in ["totalAssetsSlot", "totalSupplySlot", "shareBalancesSlot", + "deposit", "withdraw", "balanceOf", "totalAssets", "totalSupply", + "shareBalances", "sourceDigest"] do + let name := `Contracts.VaultFromSolidity ++ Name.mkSimple suffix + let some (.defnInfo info) := (← getEnv).find? name + | throwError "not a transparent definition: {name}" + unless info.safety == .safe && !info.value.hasMVar && !info.value.hasFVar do + throwError "unsafe or unclosed definition: {name}" + for dep in info.value.getUsedConstants do + if dep.toString.startsWith "Contracts." && + !dep.toString.startsWith "Contracts.VaultFromSolidity." then + throwError "imported declaration depends on handwritten contract: {dep}" + let some (.defnInfo deposit) := (← getEnv).find? `Contracts.VaultFromSolidity.deposit + | throwError "missing imported deposit" + for dep in [``Verity.setMapping, ``Verity.setStorage, ``Verity.Stdlib.Math.safeAdd] do + unless deposit.value.getUsedConstants.contains dep do + throwError "missing source-derived deposit operation: {dep}" + logInfo "CHECKED_TRANSPARENT_DECLARATIONS" +solidity_contract Existing from "../../Contracts/VaultFromSolidity/Vault.sol" +run_cmd do + let original ← getEnv + let mut rejected := false + try + SolidityImporter.elabSolidityContract + (← `(command| solidity_contract $(mkIdent `Existing):ident from "../../Contracts/VaultFromSolidity/Vault.sol")) + catch _ => rejected := true + unless rejected do throwError "duplicate alias accepted" + let some (.defnInfo before) := original.find? `Existing.deposit + | throwError "missing initial declaration" + let some (.defnInfo after) := (← getEnv).find? `Existing.deposit + | throwError "lost initial declaration" + unless before.value == after.value && before.type == after.type do + throwError "duplicate alias changed prior declaration" + logInfo "DUPLICATE_ALIAS_REJECTED" +''') + output = run(root, [LAKE, "env", "lean", str(probe)]) + check("CHECKED_TRANSPARENT_DECLARATIONS" in output and + "DUPLICATE_ALIAS_REJECTED" in output, + "safe transparent readable definitions and collision rollback") + check("Verity.setMapping" in output and "Verity.setStorage" in output and + "safeAdd" in output, + "#print deposit exposes readable source-derived behavior") + finally: + probe.unlink(missing_ok=True) + + before = artifacts() + build() + check(before == artifacts(), "unchanged build reuses Vault artifacts") + + theorem_starts = [ + (match.group(1), line_no) + for line_no, line in enumerate(proof_text.splitlines(), 1) + if (match := re.match(r"theorem\s+([A-Za-z0-9_']+)", line.strip())) + ] + theorem_ranges = { + name: (start, theorem_starts[index + 1][1] - 1 if index + 1 < len(theorem_starts) + else len(proof_text.splitlines())) + for index, (name, start) in enumerate(theorem_starts) + } + + edit_source(original.replace(b"assets", b"depositAmount")) + build() + check(True, "declaration-ID based parameter rename preserves proofs") + edit_source(original) + build() + + for name, theorem, old, new in ( + ("deposit behavior", "deposit_meets_spec", b"totalSupply += assets;", b"totalSupply = assets;"), + ("getter behavior", "balance_meets_spec", b"return shareBalances[account];", b"return totalAssets;"), + ): + check(original.count(old) == 1, name + " mutation has one source target") + before = artifacts() + edit_source(original.replace(old, new)) + output = build(False, "Contracts.VaultFromSolidity.Proofs.Execution") + error_lines = [int(value) for value in re.findall( + r"Contracts/VaultFromSolidity/Proofs/Execution\.lean:(\d+):", output)] + start, end = theorem_ranges[theorem] + check(any(start <= line <= end for line in error_lines), + name + f" mutation breaks {theorem}") + check(before != artifacts(), name + " preserved-mtime edit refreshes artifacts") + edit_source(original) + build() + + for name, old, new, diagnostic in ( + ("contract layout at", b"contract Vault {", b"contract Vault layout at 100 {", "layout at"), + ("initializer", b"uint256 public totalAssets;", b"uint256 public totalAssets = 1;", "initializer"), + ("unchecked block", b"totalAssets += assets;", b"unchecked { totalAssets += assets; }", "UncheckedBlock"), + ("loop", b"totalAssets += assets;", b"while (assets < totalAssets) { totalAssets += assets; }", "WhileStatement"), + ("second contract", b"contract Vault {", b"contract Other {}\ncontract Vault {", "exactly one"), + ("multiplication", b"totalAssets += assets;", b"totalAssets = totalAssets * assets;", "unsupported binary"), + ): + edit_source(original.replace(old, new)) + output = build(False, diagnostic) + check(re.search(r"Contracts/VaultFromSolidity/Vault.sol:\d+:\d+:", output) is not None, + name + " rejected with source position") + edit_source(original) + build() + + with tempfile.TemporaryDirectory(prefix="verity-vault-outside-", dir=ROOT.parent) as outside: + escaped = Path(outside) / "Vault.sol" + escaped.write_bytes(original) + source.unlink() + source.symlink_to(escaped) + try: + probe.write_text('''import Contracts.VaultFromSolidity.Importer.Importer +solidity_contract Escaped from "../../Contracts/VaultFromSolidity/Vault.sol" +''') + run(root, [LAKE, "env", "lean", str(probe)], False, "source outside package") + check(True, "registered-source symlink escape rejected") + finally: + probe.unlink(missing_ok=True) + source.unlink() + edit_source(original) + build() + + before = artifacts() + digest_before = source_digest() + importer.write_bytes(importer_original + b"\n-- acceptance translation identity probe\n") + os.utime(importer, ns=(importer_stamp.st_atime_ns, importer_stamp.st_mtime_ns)) + build() + check(before != artifacts(), "Lean importer content change invalidates Vault artifacts") + check(digest_before != source_digest(), "Lean importer content changes sourceDigest") + importer.write_bytes(importer_original) + build() + + policy = root / "lakefile.lean" + policy_original = policy.read_bytes() + before = artifacts() + policy.write_bytes(policy_original + b"\n-- acceptance build-policy probe\n") + build() + check(before != artifacts(), "build-policy content change invalidates Vault artifacts") + policy.write_bytes(policy_original) + build() + + compiler_stamp = compiler.stat() + compiler.write_bytes(compiler_original + b"\nacceptance-check\n") + os.utime(compiler, ns=(compiler_stamp.st_atime_ns, compiler_stamp.st_mtime_ns)) + build(False, "compiler checksum mismatch") + check(True, "compiler content mutation fails closed") + compiler.write_bytes(compiler_original) + build() + + # Synthetic compiler-output probes test the JSON boundary itself. The + # temporary wrapper is checksummed and accepted only in this disposable + # package; production still executes the pinned binary directly. + real_compiler = compiler.with_name("solc-real") + pin = b"1274e5c4621ae478090c5a1f48466fd3c5f658ed9e14b15a0b213dc806215468" + for mode, diagnostic in ( + ("ast", "unexpected AST fields"), + ("metadata", "unexpected AST fields"), + ("typed", "invalid AST metadata field Assignment.isLValue"), + ("missing", "missing AST fields"), + ("span", "source span outside registered source"), + ("layout", "missing/packed layout"), + ): + try: + real_compiler.write_bytes(compiler_original) + real_compiler.chmod(0o755) + compiler.write_text(f'''#!/usr/bin/env python3 +import json, pathlib, subprocess, sys +real = pathlib.Path(__file__).with_name("solc-real") +p = subprocess.run([str(real), *sys.argv[1:]], input=sys.stdin.buffer.read(), capture_output=True) +if "--standard-json" not in sys.argv: + sys.stdout.buffer.write(p.stdout); sys.stderr.buffer.write(p.stderr); raise SystemExit(p.returncode) +o = json.loads(p.stdout) +if {mode!r} in ("ast", "metadata", "typed", "missing", "span"): + def mutate(x): + if isinstance(x, dict): + if {mode!r} == "ast" and x.get("nodeType") == "Assignment": + x["unknownExecutableField"] = True; return True + if {mode!r} == "metadata" and x.get("nodeType") == "StructuredDocumentation": + x["unexpectedExecutable"] = {{"nodeType": "UncheckedBlock", "id": 999999, "src": "0:0:0"}} + return True + if {mode!r} == "typed" and x.get("nodeType") == "Assignment": + x["isLValue"] = {{"nodeType": "UncheckedBlock", "id": 999999, "src": "0:0:0"}} + return True + if {mode!r} == "missing" and x.get("nodeType") == "Assignment": + del x["isPure"] + return True + if {mode!r} == "span" and x.get("nodeType") == "Assignment": + start, size, _ = x["src"].split(":") + x["src"] = f"{{start}}:{{size}}:999" + return True + return any(mutate(v) for v in x.values()) + if isinstance(x, list): return any(mutate(v) for v in x) + return False + assert mutate(o) +else: + o["contracts"]["Contracts/VaultFromSolidity/Vault.sol"]["Vault"]["storageLayout"]["storage"][0]["offset"] = 1 +sys.stdout.write(json.dumps(o)) +''') + compiler.chmod(0o755) + wrapper_hash = hashlib.sha256(compiler.read_bytes()).hexdigest().encode() + check(pin in importer_original, "compiler pin occurs in Lean importer") + importer.write_bytes(importer_original.replace(pin, wrapper_hash)) + run(root, [LAKE, "build", "VaultSolidityImporter"]) + build(False, diagnostic) + check(True, f"synthetic {mode} compiler output fails closed") + finally: + real_compiler.unlink(missing_ok=True) + compiler.write_bytes(compiler_original) + compiler.chmod(0o755) + importer.write_bytes(importer_original) + build() + + # Corrupt a late declaration's type. Synchronous checking must reject it + # before any declaration from the failed namespace escapes the transaction. + try: + importer.write_bytes(importer_original.replace( + b" addDecl (.defnDecl { name, levelParams := [], type, value, hints := .regular 0, safety := .safe })", + b' let type := if name.toString.endsWith ".deposit" then mkConst ``Nat else type\n' + b" addDecl (.defnDecl { name, levelParams := [], type, value, hints := .regular 0, safety := .safe })", + )) + run(root, [LAKE, "build", "VaultSolidityImporter"]) + probe.write_text('''import Contracts.VaultFromSolidity.Importer.Importer +open Lean Elab Command +set_option Elab.async true +run_cmd do + let mut rejected := false + try + SolidityImporter.elabSolidityContract + (← `(command| solidity_contract $(mkIdent `Broken):ident from "../../Contracts/VaultFromSolidity/Vault.sol")) + catch e => + rejected := true + logInfo m!"EXPECTED_KERNEL_ERROR {e.toMessageData}" + unless rejected do throwError "malformed declaration accepted" + for suffix in ["totalAssetsSlot", "totalSupplySlot", "shareBalancesSlot", + "totalAssets", "totalSupply", "shareBalances", "deposit", "sourceDigest"] do + if (← getEnv).contains (`Broken ++ Name.mkSimple suffix) then + throwError "partial declaration escaped rollback: {suffix}" + logInfo "KERNEL_REJECTION_ROLLED_BACK" +''') + output = run(root, [LAKE, "env", "lean", str(probe)]) + check("KERNEL_REJECTION_ROLLED_BACK" in output and "(kernel)" in output, + "malformed late declaration rejected synchronously with full rollback") + finally: + probe.unlink(missing_ok=True) + importer.write_bytes(importer_original) + build() + + check(set(root.rglob("*.lean")) == lean_sources, + "no generated model .lean files") + check(source.read_bytes() == original and importer.read_bytes() == importer_original, + "temporary mutations restored; final baseline passes") + print(f"PASS all Lean-only Vault acceptance checks ({len(theorem_names)} audited theorems)", flush=True) + + +if __name__ == "__main__": + main() diff --git a/Contracts/VaultFromSolidity/Proofs/Execution.lean b/Contracts/VaultFromSolidity/Proofs/Execution.lean new file mode 100644 index 0000000000..be3f6f54ac --- /dev/null +++ b/Contracts/VaultFromSolidity/Proofs/Execution.lean @@ -0,0 +1,90 @@ +import Contracts.VaultFromSolidity.Spec + +/-! +# Proofs about the Vault imported from Solidity + +Two layers, deliberately kept small: + +1. `*_meets_spec` -- each entry point produces exactly the state + `Spec` describes. These unfold the definitions `Importer.lean` registered + from `Vault.sol`, so they fail if the Solidity source changes behaviour. +2. `*_preserves_solvency` -- the contract-level result. Neither a deposit nor a + withdrawal can break the one-for-one backing between assets and issued + shares. A reverting call leaves the state untouched (`Contract.run` rolls + back), so solvency can only ever be lost on a successful call, which is what + these two theorems rule out. +-/ + +namespace Contracts.VaultFromSolidity.Proofs.Execution +open Verity +open Verity.Stdlib.Math + +macro "reduce_vault" : tactic => `(tactic| + simp_all [Spec.deposit_execution, Spec.withdraw_execution, Spec.balance_execution, + Spec.accountingState, deposit, withdraw, balanceOf, totalAssets, totalSupply, + shareBalances, totalAssetsSlot, totalSupplySlot, shareBalancesSlot, + Contract.run, Bind.bind, Pure.pure, Verity.instMonadContract, Verity.bind, Verity.pure, + msgValue, msgSender, Verity.require, + getStorage, setStorage, getMapping, setMapping, requireSomeUint, safeSub, + Verity.EVM.Uint256.sub, Nat.not_le_of_lt, Nat.not_lt_of_ge, + ContractState.readSlot, ContractState.writeSlot, ContractState.readMap, + ContractState.writeMap, ContractState.storage, ContractState.storageMap]) + +/-! ## Exact behaviour of each entry point -/ + +theorem balance_meets_spec (s : ContractState) (account : Address) + (h0 : s.msgValue = 0) : Spec.balance_execution s account := by + reduce_vault + +theorem deposit_meets_spec (s : ContractState) (amount : Uint256) + (h0 : s.msgValue = 0) + (hs : safeAdd (s.readMap 2 s.sender) amount = some (s.readMap 2 s.sender + amount)) + (ha : safeAdd (s.readSlot 0) amount = some (s.readSlot 0 + amount)) + (ht : safeAdd (s.readSlot 1) amount = some (s.readSlot 1 + amount)) : + Spec.deposit_execution s amount := by + reduce_vault + +theorem withdraw_meets_spec (s : ContractState) (amount : Uint256) + (h0 : s.msgValue = 0) + (hs : amount.val ≤ (s.readMap 2 s.sender).val) + (ha : amount.val ≤ (s.readSlot 0).val) + (ht : amount.val ≤ (s.readSlot 1).val) : Spec.withdraw_execution s amount := by + reduce_vault + +/-! ## The vault stays solvent -/ + +/-- A successful deposit credits the caller's shares and both totals by the same +amount, so assets still exactly back the issued shares. -/ +theorem deposit_preserves_solvency (s : ContractState) (amount : Uint256) + (h0 : s.msgValue = 0) + (hs : safeAdd (s.readMap 2 s.sender) amount = some (s.readMap 2 s.sender + amount)) + (ha : safeAdd (s.readSlot 0) amount = some (s.readSlot 0 + amount)) + (ht : safeAdd (s.readSlot 1) amount = some (s.readSlot 1 + amount)) + (hsolvent : Spec.solvent s) : + Spec.solvent ((deposit amount).run s).snd := by + have h := deposit_meets_spec s amount h0 hs ha ht + rw [Spec.deposit_execution] at h + rw [h] + simp only [Spec.solvent, Spec.accountingState, ContractResult.snd, + ContractState.readSlot, ContractState.writeSlot, ContractState.writeMap, + ContractState.storage] at hsolvent ⊢ + simp [hsolvent] + +/-- A successful withdrawal debits the caller's shares and both totals by the +same amount, so assets still exactly back the issued shares. -/ +theorem withdraw_preserves_solvency (s : ContractState) (amount : Uint256) + (h0 : s.msgValue = 0) + (hs : amount.val ≤ (s.readMap 2 s.sender).val) + (ha : amount.val ≤ (s.readSlot 0).val) + (ht : amount.val ≤ (s.readSlot 1).val) + (hsolvent : Spec.solvent s) : + Spec.solvent ((withdraw amount).run s).snd := by + have h := withdraw_meets_spec s amount h0 hs ha ht + rw [Spec.withdraw_execution] at h + rw [h] + simp only [Spec.solvent, Spec.accountingState, ContractResult.snd, + ContractState.readSlot, ContractState.writeSlot, ContractState.writeMap, + ContractState.storage] at hsolvent ⊢ + simp [hsolvent] + +end Contracts.VaultFromSolidity.Proofs.Execution diff --git a/Contracts/VaultFromSolidity/Spec.lean b/Contracts/VaultFromSolidity/Spec.lean new file mode 100644 index 0000000000..3c7e05dcf8 --- /dev/null +++ b/Contracts/VaultFromSolidity/Spec.lean @@ -0,0 +1,57 @@ +import Verity.EVM.Uint256 +import Contracts.VaultFromSolidity.VaultFromSolidity + +/-! +# What the imported Vault is supposed to do + +`Importer.lean` turns `Vault.sol` into ordinary Verity definitions: `deposit`, +`withdraw`, `balanceOf`, and one `StorageSlot` per state variable +(slot `0 = totalAssets`, slot `1 = totalSupply`, slot `2 = shareBalances`). + +This file states two things about them: + +* `solvent` -- the property that matters for the contract as a whole. Shares are + issued one-for-one against assets, so every share outstanding must stay backed + by an asset the vault accounts for. +* `deposit_execution` / `withdraw_execution` / `balance_execution` -- the exact + state each entry point produces. These pin down behaviour precisely enough to + derive `solvent`, and they are what a Solidity mutation has to break. +-/ + +namespace Contracts.VaultFromSolidity.Spec + +open Verity +open Verity.EVM.Uint256 + +/-- The vault's main invariant: issued shares are exactly backed by assets +(`totalAssets = totalSupply`). If this ever breaks, shares stop being +redeemable one-for-one and the vault is insolvent. -/ +def solvent (s : ContractState) : Prop := + s.readSlot 0 = s.readSlot 1 + +/-- Exact post-state of a successful `deposit`/`withdraw`: the caller's share +balance and both totals move together, including Verity's ghost +key-enumeration metadata. -/ +def accountingState (s : ContractState) (shares assets supply : Uint256) : ContractState := + let mapped := { s.writeMap 2 s.sender shares with + knownAddresses := fun slotIdx => if slotIdx == 2 then + (s.knownAddresses slotIdx).insert s.sender else s.knownAddresses slotIdx } + (mapped.writeSlot 0 assets).writeSlot 1 supply + +def deposit_execution (s : ContractState) (amount : Uint256) : Prop := + (Contracts.VaultFromSolidity.deposit amount).run s = ContractResult.success () + (accountingState s (s.readMap 2 s.sender + amount) + (s.readSlot 0 + amount) + (s.readSlot 1 + amount)) + +def withdraw_execution (s : ContractState) (amount : Uint256) : Prop := + (Contracts.VaultFromSolidity.withdraw amount).run s = ContractResult.success () + (accountingState s (s.readMap 2 s.sender - amount) + (s.readSlot 0 - amount) + (s.readSlot 1 - amount)) + +def balance_execution (s : ContractState) (account : Address) : Prop := + (Contracts.VaultFromSolidity.balanceOf account).run s = + ContractResult.success (s.readMap 2 account) s + +end Contracts.VaultFromSolidity.Spec diff --git a/examples/solidity/Vault.sol b/Contracts/VaultFromSolidity/Vault.sol similarity index 94% rename from examples/solidity/Vault.sol rename to Contracts/VaultFromSolidity/Vault.sol index 2100748310..577aa14120 100644 --- a/examples/solidity/Vault.sol +++ b/Contracts/VaultFromSolidity/Vault.sol @@ -3,7 +3,7 @@ pragma solidity ^0.8.33; /// @title Vault /// @notice Minimal ERC4626-style vault with 1:1 asset/share accounting. -/// @dev Reference implementation matching `Contracts/Vault/Vault.lean`. +/// @dev Source contract for the proof-only Solidity importer example. contract Vault { uint256 public totalAssets; uint256 public totalSupply; diff --git a/Contracts/VaultFromSolidity/VaultFromSolidity.lean b/Contracts/VaultFromSolidity/VaultFromSolidity.lean new file mode 100644 index 0000000000..b0050628c1 --- /dev/null +++ b/Contracts/VaultFromSolidity/VaultFromSolidity.lean @@ -0,0 +1,7 @@ +import Contracts.VaultFromSolidity.Importer.Importer + +namespace Contracts + +solidity_contract VaultFromSolidity from "Vault.sol" + +end Contracts diff --git a/PrintAxioms.lean b/PrintAxioms.lean index bbf05cfad6..ddc580fa9c 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -35,6 +35,7 @@ import Contracts.SimpleToken.Proofs.Isolation import Contracts.SimpleToken.Proofs.Supply import Contracts.Vault.Proofs.Correctness import Contracts.Vault.Proofs.Native +import Contracts.VaultFromSolidity.Proofs.Execution import Verity.Proofs.CheckedExternalCallConsumer import Verity.Proofs.LoopSimulationResultAware import Verity.Proofs.Model.CommonExternalCallEquivalence @@ -687,6 +688,13 @@ end Verity.AxiomAudit Contracts.Vault.Proofs.Native.vaultMinimal_runtime_lowers_native Contracts.Vault.Proofs.Native.vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value + -- Contracts/VaultFromSolidity/Proofs/Execution.lean + Contracts.VaultFromSolidity.Proofs.Execution.balance_meets_spec + Contracts.VaultFromSolidity.Proofs.Execution.deposit_meets_spec + Contracts.VaultFromSolidity.Proofs.Execution.withdraw_meets_spec + Contracts.VaultFromSolidity.Proofs.Execution.deposit_preserves_solvency + Contracts.VaultFromSolidity.Proofs.Execution.withdraw_preserves_solvency + -- Verity/Proofs/CheckedExternalCallConsumer.lean Verity.Proofs.CheckedExternalCallConsumer.lido_submit_entry_installs_caller_context Verity.Proofs.CheckedExternalCallConsumer.lido_submit_success_world @@ -7515,4 +7523,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 6953 theorems/lemmas (4963 public, 1990 private, 0 sorry'd) +-- Total: 6958 theorems/lemmas (4968 public, 1990 private, 0 sorry'd) diff --git a/README.md b/README.md index 8fa5d83c3d..93120319bc 100644 --- a/README.md +++ b/README.md @@ -21,6 +21,37 @@ **Verity** is a formally verified smart contract compiler written in [Lean 4](https://lean-lang.org/). You write contracts in an embedded DSL, state what they should do, prove those properties hold, and compile to EVM bytecode. The compiler itself is proven to preserve semantics across three verified layers. Full documentation lives at [**veritylang.com**](https://veritylang.com). +## Proof-only Solidity Vault import (POC) + +`Contracts/VaultFromSolidity/VaultFromSolidity.lean` imports the colocated +`Vault.sol` with `solidity_contract VaultFromSolidity from "Vault.sol"`. +The Lean frontend invokes pinned solc 0.8.33 for typed AST and storage layout, +validates and translates them directly, then registers transparent, +kernel-checked `Verity.Contract` definitions in memory. There is no Python +frontend, custom serialized IR, generated `.lean`, CompilationModel, or +bytecode. The example is independent of the +handwritten `Contracts/Vault` contract. `Spec.lean` states the vault's solvency +invariant plus the exact post-state of each entry point, and +`Proofs/Execution.lean` proves them against the imported definitions. + +With the Lean/package prerequisites installed, put the official Linux-amd64 solc +0.8.33 binary at `.lake/solidity-import/solc` and make it executable. Its accepted +SHA-256 digest is +`1274e5c4621ae478090c5a1f48466fd3c5f658ed9e14b15a0b213dc806215468`, then run: + +```sh +lake build VaultFromSolidity +python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py +``` + +The acceptance script uses disposable copies for source mutations, fail-closed +rejection, content-based Lake freshness, compiler/importer/build-policy +invalidation, declaration-registration rollback, and an audit of every Vault +theorem. It never mutates the original Solidity file. +Save Solidity, rebuild this dedicated target, then reload the Lean editor: +an already-open editor snapshot does not automatically watch `.sol` changes. +See [the trust boundary](TRUST_ASSUMPTIONS.md#proof-only-solidity-vault-import). + ## Verification status All proofs are machine-checked by the Lean kernel. CI rebuilds the proof development on every commit, and repository checks enforce that no proof is left incomplete (no `sorry`) and that the compiler proof stack carries 0 axioms (see [AXIOMS.md](AXIOMS.md)). Verification is scoped rather than total: the generic compiler theorems cover an explicitly documented fragment of the language, and the precise boundary between what is proven and what is trusted is maintained in [TRUST_ASSUMPTIONS.md](TRUST_ASSUMPTIONS.md). diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 38b12c0d09..d180ca0250 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -2,6 +2,66 @@ This document states what Verity proves and what it still trusts. +## Proof-only Solidity Vault import + +This POC is separate from the verified compilation pipeline below. It trusts +pinned solc's typed AST/storage layout and the Lean translation in +`Contracts/VaultFromSolidity/Importer/Importer.lean` to preserve Solidity +meaning. Kernel checking establishes well-typed definitions and theorems about +their execution, not a Solidity-to-Verity equivalence theorem. `sourceDigest` +is provenance, not proof of correspondence. It hashes the compiler +input/output, Lean importer implementation, and verified solc checksum/version. +The Linux host's fixed `/usr/bin/sha256sum` is trusted for compiler-pin checks; +the digest is checked before version inspection, immediately before compilation, +and again after compilation, so `PATH` substitution and persistent compiler +replacement fail closed. As with all local builds, a concurrently malicious +process with the builder's own filesystem privileges is outside the threat model. +It is not full build identity: transitive Verity semantics, Lean toolchain, and +Lake build policy are tracked separately by normal build dependencies, not this +digest. The recursive closed AST schema rejects unknown fields/node kinds and +contract `layout at`; semantically used type metadata and all storage-layout +records are checked explicitly. Canonical package containment is checked +independently of source registration. + +`Importer.lean` runs pinned solc itself with `--standard-json` and +`--no-import-callback`, parses the typed AST/storage layout, validates the +closed subset, resolves IDs/types/storage slots, and constructs expressions +through explicit `translateExpr` / `translateStmt` cases. Declaration +registration disables asynchronous kernel checking inside the transaction, +restores the pre-import environment on failure, checks every body against its +typed return signature, and registers safe transparent definitions. The +frontend emits no generated Lean source and keeps no serialized AST/model +cache. + +The accepted fragment covers the existing Vault: full-width scalars, +address-to-uint256 mappings and public getters, straight-line reads/writes, +locals, checked addition/subtraction, and comparison/custom-error guards. +Unknown executable constructs are rejected; this is not general Solidity support. +Arguments/context are already typed and decoded. `Contract.run` rolls back +failed executions; errors are model strings, not verified ABI revert bytes. +The storage model uses logical keys, not a proof of physical keccak layout. +There is no deployment, calldata/dispatch, gas, external interaction, bytecode, +or full EVM equivalence claim. Initial states are arbitrary, not proven deployed +states. Arithmetic success premises restrict the success theorems. The example keeps one +readable proof set: the exact post-state of each entry point plus the vault's +solvency invariant (`totalAssets = totalSupply`) preserved by deposit and +withdrawal. Revert-path behaviour (nonpayability, insufficient +shares/assets/supply, late-overflow rollback) is exercised by the acceptance +suite, not proved here. + +The specification and execution proof file refer directly to the imported +definitions. Zero-argument custom errors use Verity's `Name()` model convention; +arithmetic panic strings remain a model representation, not an assertion of +matching EVM revert bytes. The statements do not assert full equivalence of all +executions or all public/deployment interfaces. + +Lake's dedicated `VaultFromSolidity` target tracks source/compiler/Lean-importer/build +policy bytes and normal Lean dependencies. Acceptance evidence is obtained with +`python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py`; +that Python file only orchestrates disposable builds and mutations and is not in +the translation path. Stale editor snapshots are not a current-source proof +certificate. No additional project axiom is introduced. + ## Compilation Pipeline ``` diff --git a/artifacts/trust_surface_report.json b/artifacts/trust_surface_report.json index ef14f60e7c..f94530f0b7 100644 --- a/artifacts/trust_surface_report.json +++ b/artifacts/trust_surface_report.json @@ -169,7 +169,7 @@ "mechanisms": { "@[implemented_by": 1, "native_decide": 584, - "partial def": 175 + "partial def": 180 }, "notes": "native_decide trusts Lean.ofReduceBool or Lean 4.31 generated per-proof native_decide axioms + Lean.trustCompiler. Prose registry: AXIOMS.md, TRUST_ASSUMPTIONS.md (enforced by scripts/check_trust_surface_registry.py).", "schema_version": 1 diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json index 3ed6aeae48..b93a6f999e 100644 --- a/artifacts/verification_status.json +++ b/artifacts/verification_status.json @@ -1,7 +1,7 @@ { "codebase": { "core_lines": 2040, - "example_contracts": 18 + "example_contracts": 19 }, "proofs": { "axioms": 1, @@ -15,11 +15,11 @@ "suites": 52 }, "theorems": { - "categories": 15, - "coverage_percent": 78, + "categories": 16, + "coverage_percent": 76, "covered": 255, - "excluded": 74, - "non_stdlib_total": 329, + "excluded": 79, + "non_stdlib_total": 334, "per_contract": { "Counter": 31, "ERC20": 22, @@ -35,11 +35,12 @@ "SafeCounter": 25, "SimpleStorage": 20, "SimpleToken": 61, - "Vault": 9 + "Vault": 9, + "VaultFromSolidity": 5 }, - "proven": 329, + "proven": 334, "stdlib": 0, - "total": 329 + "total": 334 }, "toolchain": { "lean": "leanprover/lean4:v4.31.0", diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index b4b89b6647..5abfb5b45d 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -31,9 +31,9 @@ Every transition inside the proof envelope is either fully verified or recorded - **Language**: Lean 4.31.0 -- **Core Size**: 1991 lines -- **Verified Contracts**: 15 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault) -- **Theorems**: 329 across 15 categories, 329 fully proven +- **Core Size**: 2040 lines +- **Verified Contracts**: 16 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault, VaultFromSolidity) +- **Theorems**: 334 across 16 categories, 334 fully proven - **Axioms**: 1 documented Lean axioms (see AXIOMS.md) - **Tests**: 528 Foundry tests, 239 property tests - **Build**: `lake build` verifies all proofs diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md index 08f4684387..ad95f36772 100644 --- a/docs/VERIFICATION_STATUS.md +++ b/docs/VERIFICATION_STATUS.md @@ -39,12 +39,13 @@ EVM Bytecode | ERC20 | 22 | Baseline | `Contracts/ERC20/Proofs/` | | ERC721 | 11 | Baseline | `Contracts/ERC721/Proofs/` | | Vault | 9 | Baseline | `Contracts/Vault/Proofs/` | +| VaultFromSolidity | 5 | Proof-only import | `Contracts/VaultFromSolidity/Proofs/` | | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` | | ReentrancyRelyGuarantee | 10 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` | | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` | -| **Total** | **329** | **✅ 100%** | — | +| **Total** | **334** | **✅ 100%** | — | -> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (329 total properties). +> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (334 total properties). Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, [#1747](https://github.com/lfglabs-dev/verity/issues/1747)) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the `CompilationModel` only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust. @@ -202,6 +203,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co |----------|----------|------------| | ERC20 | 86% (19/22) | 3 proof-only | | Vault | 0% (0/9) | 9 proof-only | +| VaultFromSolidity | 0% (0/5) | 5 proof-only | | ERC721 | 100% (11/11) | 0 | | SafeCounter | 100% (25/25) | 0 | | ReentrancyExample | 100% (5/5) | 0 | @@ -217,13 +219,13 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co | Counter | 74% (23/31) | 8 proof-only | | Stdlib | 0% (0/0) | 0 proof-only | -**Status**: 78% coverage (255/329), 74 remaining exclusions all proof-only +**Status**: 76% coverage (255/334), 79 remaining exclusions all proof-only -- **Total Properties**: 329 +- **Total Properties**: 334 - **Covered**: 255 -- **Excluded**: 74 (all proof-only) +- **Excluded**: 79 (all proof-only) -**Proof-Only Properties (59 exclusions)**: Internal proof machinery that cannot be tested in Foundry. +**Proof-Only Properties (74 exclusions)**: Internal proof machinery that cannot be tested in Foundry. 0 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules. 5266 theorems/lemmas (3645 public, 1621 private) verified by `lake build PrintAxioms`. diff --git a/lakefile.lean b/lakefile.lean index f988503830..ce4192c8c7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -22,6 +22,31 @@ lean_lib «Verity» where .one `Verity.Proofs.LoopSimulationResultAware ] +input_file vaultSolidity where + path := "Contracts/VaultFromSolidity/Vault.sol" + text := false + +input_file vaultLeanImporter where + path := "Contracts/VaultFromSolidity/Importer/Importer.lean" + text := false + +input_file vaultSolc where + path := ".lake/solidity-import/solc" + text := false + +input_file vaultBuildPolicy where + path := "lakefile.lean" + text := false + +lean_lib «VaultSolidityImporter» where + globs := #[.one `Contracts.VaultFromSolidity.Importer.Importer] + +lean_lib «VaultFromSolidity» where + globs := #[.one `Contracts.VaultFromSolidity.VaultFromSolidity, + .one `Contracts.VaultFromSolidity.Spec, + .one `Contracts.VaultFromSolidity.Proofs.Execution] + needs := #[vaultSolidity, vaultLeanImporter, vaultSolc, vaultBuildPolicy] + lean_lib «Contracts» where globs := #[ .one `Contracts, @@ -38,7 +63,11 @@ lean_lib «Contracts» where .andSubmodules `Contracts.OwnedCounterComposed, .andSubmodules `Contracts.SafeCounter, .andSubmodules `Contracts.Ledger, - .andSubmodules `Contracts.Vault, + .one `Contracts.Vault, .one `Contracts.Vault.Vault, + .one `Contracts.Vault.Spec, .one `Contracts.Vault.Invariants, + .one `Contracts.Vault.SpecProofs, .one `Contracts.Vault.Proofs.Basic, + .one `Contracts.Vault.Proofs.Correctness, .one `Contracts.Vault.Proofs.Conservation, + .one `Contracts.Vault.Proofs.Native, .andSubmodules `Contracts.ERC20, .andSubmodules `Contracts.ERC721, .andSubmodules `Contracts.SimpleToken, diff --git a/scripts/check_contract_structure.py b/scripts/check_contract_structure.py index 9a063a23a0..ddf5428da3 100755 --- a/scripts/check_contract_structure.py +++ b/scripts/check_contract_structure.py @@ -21,6 +21,7 @@ "ReentrancyRelyGuarantee", # Proof-only rely-guarantee framework example, inline proofs "Ownable", # Mixin facet: named-slot proofs + footprint, no Foundry/Yul twin "OwnedCounterComposed", # Include-host acceptance example; OwnedCounter keeps Yul/difftest + "VaultFromSolidity", # Proof-only imported model with its own focused structure } # Contracts excluded from property test check @@ -30,6 +31,7 @@ "ReentrancyRelyGuarantee", # Abstract state-transformer proofs, no compiled contract to property-test "Ownable", # Mixin proofs are reused by hosts; no compiled property harness "OwnedCounterComposed", # Proof-composition host; OwnedCounter remains the Foundry target + "VaultFromSolidity", # Imported-model theorems are covered by the focused mutation suite } # Contracts excluded from differential test check @@ -40,6 +42,7 @@ "ReentrancyRelyGuarantee", # No compiled bytecode (abstract proofs), nothing to differential-test "Ownable", # Mixin facet; no dedicated Yul/Foundry twin "OwnedCounterComposed", # Selectors/layout stay on OwnedCounter until bit-identical + "VaultFromSolidity", # Proof-only importer emits no bytecode for differential testing } # Expected files for each contract (relative to ROOT) diff --git a/test/Vault.t.sol b/test/Vault.t.sol index b7d9941b78..c221dd2761 100644 --- a/test/Vault.t.sol +++ b/test/Vault.t.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.33; import "forge-std/Test.sol"; -import "../examples/solidity/Vault.sol"; +import "../Contracts/VaultFromSolidity/Vault.sol"; contract VaultTest is Test { Vault internal vault; diff --git a/test/property_exclusions.json b/test/property_exclusions.json index b02ea2d277..e8d020fa34 100644 --- a/test/property_exclusions.json +++ b/test/property_exclusions.json @@ -15,6 +15,13 @@ "vaultMinimal_runtime_lowers_native", "vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value" ], + "VaultFromSolidity": [ + "balance_meets_spec", + "deposit_meets_spec", + "deposit_preserves_solvency", + "withdraw_meets_spec", + "withdraw_preserves_solvency" + ], "Counter": [ "getStorage_reads_count", "previewAddTwice_correct", diff --git a/test/property_manifest.json b/test/property_manifest.json index b43566798a..db7b8830a2 100644 --- a/test/property_manifest.json +++ b/test/property_manifest.json @@ -357,5 +357,12 @@ "vaultMinimal_functions_bridged", "vaultMinimal_runtime_lowers_native", "vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value" + ], + "VaultFromSolidity": [ + "balance_meets_spec", + "deposit_meets_spec", + "deposit_preserves_solvency", + "withdraw_meets_spec", + "withdraw_preserves_solvency" ] }