feat: named storage view for VaultFromSolidity

AUDIT.md

@@ -13,15 +13,29 @@ 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.
+malformed late declaration and complete registration rollback (including the
+named storage view), plus the pinned compiler's checksum. Named-storage checks
+cover `v.totalAssets` dot notation and `#print Storage.shareBalances`, a
+declaration-reorder mutation that moves solc slots while every proof still
+builds, a state-variable rename that makes `Spec.lean` fail to elaborate, and a
+Solidity variable named `Storage` rejected with a source position. Behaviour
+mutations must break both the exact-state lemma and the `*_meets_spec`
+theorem of the affected entry point, and three `Spec.lean` mutations that
+weaken a promise must fail inside the corresponding `*_meets_spec` theorem
+while leaving the exact-state lemmas green. The `spec_named_storage`
+lean_lint rule (in `make check`) rejects every raw `ContractState` accessor
+(the list is read from `Verity/Core.lean`), raw storage fields, direct
+`ContractState` mentions, positional projections, and `knownAddresses` in
+opted-in spec files. 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
+proofs to fail at both the exact-state and spec layer, weakens the named spec
+and requires the spec theorems 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.

AXIOMS.md

@@ -6,7 +6,7 @@ This file is the authoritative registry of axioms used by Verity proof code.
 
 `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
+every theorem in `Contracts/VaultFromSolidity/Proofs/ExecutionProof.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.

Contracts/VaultFromSolidity/Importer/Importer.lean

@@ -6,6 +6,11 @@ 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.
+
+Besides the executable model it registers a read-only storage view: `Storage` is a
+synonym for `ContractState`, `Storage.<var>` reads each state variable through its
+`<var>Slot` handle, and `view` coerces a state into it. Specs can then say
+`v.totalAssets` instead of naming a raw slot number.
 -/
 
 open Lean Meta Elab Command
@@ -324,6 +329,7 @@ private partial def validateNode (ctx : SourceContext) (j : Json) : MetaM Unit :
 
 private structure FieldInfo where
   id : Nat
+  var : String
   name : String
   getter : Option String
   slot : Nat
@@ -340,7 +346,8 @@ private structure Frontend where
 private def validName (name : String) : Bool :=
   match name.toList with
   | [] => false
-  | c :: cs => c.isAlpha && cs.all (fun c => c.isAlphanum || c == '_') && name != "sourceDigest"
+  | c :: cs => c.isAlpha && cs.all (fun c => c.isAlphanum || c == '_') &&
+      !["sourceDigest", "Storage", "view"].contains name
 
 private def identifier (ctx : SourceContext) (j : Json) : MetaM String := do
   let name ← str (← field j "name")
@@ -469,7 +476,7 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St
         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
+        fields := FieldInfo.mk id name (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"
@@ -510,10 +517,10 @@ private def seq (m t : Expr) (k : Expr → MetaM Expr) : MetaM Expr :=
     let next ← k x
     mkAppM ``Verity.bind #[m, ← mkLambdaFVars #[x] next]
 
-private def register (name : Name) (value : Expr) : MetaM Unit := do
+private def register (name : Name) (value : Expr) (type? : Option Expr := none) : MetaM Unit := do
   if (← getEnv).contains name then throwError "declaration collision: {name}"
   let value ← instantiateMVars value
-  let type ← instantiateMVars (← inferType value)
+  let type ← instantiateMVars (← type?.getDM (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 })
@@ -742,9 +749,10 @@ private partial def translateParams (frontend : Frontend) (params : List Json) (
 
 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]
+  let mut names := #[ns ++ `sourceDigest, ns ++ `Storage, ns ++ `view]
   for f in frontend.fields do
     names := names.push (ns ++ Name.mkSimple f.name)
+    names := names.push (ns ++ `Storage ++ Name.mkSimple f.var)
     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
@@ -759,6 +767,22 @@ private def importFrontend (ns : Name) (frontend : Frontend) : MetaM Unit := do
     let name := ns ++ Name.mkSimple f.name
     register name slot
     slots := (f.id, mkConst name) :: slots
+  -- Read-only named storage view. Every reader goes through the registered
+  -- `<var>Slot` handle, so `#print` shows which slot a name denotes.
+  let state := mkConst ``Verity.ContractState
+  let storageView := mkConst (ns ++ `Storage)
+  register (ns ++ `Storage) state
+  for f in frontend.fields do
+    let slot ← mkAppM ``Verity.StorageSlot.slot #[← lookupSlot slots f.id]
+    let value ← withLocalDeclD `v storageView fun v => do
+      if f.mapping then
+        withLocalDeclD `key address fun key =>
+          mkLambdaFVars #[v, key] (mkAppN (mkConst ``Verity.ContractState.readMap) #[v, slot, key])
+      else
+        mkLambdaFVars #[v] (mkAppN (mkConst ``Verity.ContractState.readSlot) #[v, slot])
+    register (ns ++ `Storage ++ Name.mkSimple f.var) value
+  let view ← withLocalDeclD `s state fun s => mkLambdaFVars #[s] s
+  register (ns ++ `view) view (some (← mkArrow state storageView))
   for f in frontend.fields do
     if let some getter := f.getter then
       let slot ← lookupSlot slots f.id

Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py

@@ -137,15 +137,15 @@ def source_digest() -> str:
         finally:
             ux_probe.unlink(missing_ok=True)
 
-        proof = root / "Contracts/VaultFromSolidity/Proofs/Execution.lean"
+        proof = root / "Contracts/VaultFromSolidity/Proofs/ExecutionProof.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"
+                "import Contracts.VaultFromSolidity.Proofs.ExecutionProof\n"
                 + "\n".join(
-                    "#print axioms Contracts.VaultFromSolidity.Proofs.Execution." + name
+                    "#print axioms Contracts.VaultFromSolidity.Proofs.ExecutionProof." + name
                     for name in theorem_names
                 )
                 + "\n"
@@ -154,7 +154,7 @@ def source_digest() -> str:
         finally:
             audit_file.unlink(missing_ok=True)
         entries = re.findall(
-            r"'Contracts.VaultFromSolidity.Proofs.Execution.(\w+)' depends on axioms: \[([^\]]*)\]", audit
+            r"'Contracts.VaultFromSolidity.Proofs.ExecutionProof.(\w+)' depends on axioms: \[([^\]]*)\]", audit
         )
         check(set(theorem_names) == {name for name, _ in entries},
               "every theorem appears in actual #print axioms output")
@@ -167,11 +167,14 @@ def source_digest() -> str:
             probe.write_text('''import Contracts.VaultFromSolidity.VaultFromSolidity
 open Lean Elab Command
 #print Contracts.VaultFromSolidity.deposit
+#check fun (v : Contracts.VaultFromSolidity.Storage) => v.totalAssets
+#print Contracts.VaultFromSolidity.Storage.shareBalances
 run_cmd do
   for suffix in ["totalAssetsSlot", "totalSupplySlot", "shareBalancesSlot",
                  "deposit", "withdraw", "balanceOf", "totalAssets", "totalSupply",
-                 "shareBalances", "sourceDigest"] do
-    let name := `Contracts.VaultFromSolidity ++ Name.mkSimple suffix
+                 "shareBalances", "sourceDigest", "Storage", "Storage.totalAssets",
+                 "Storage.totalSupply", "Storage.shareBalances", "view"] do
+    let name := `Contracts.VaultFromSolidity ++ suffix.toName
     let some (.defnInfo info) := (← getEnv).find? name
       | throwError "not a transparent definition: {name}"
     unless info.safety == .safe && !info.value.hasMVar && !info.value.hasFVar do
@@ -210,6 +213,11 @@ def source_digest() -> str:
             check("Verity.setMapping" in output and "Verity.setStorage" in output and
                   "safeAdd" in output,
                   "#print deposit exposes readable source-derived behavior")
+            check("fun v => v.totalAssets : Contracts.VaultFromSolidity.Storage → Verity.Uint256" in output,
+                  "named storage view supports v.totalAssets dot notation")
+            check("def Contracts.VaultFromSolidity.Storage.shareBalances" in output and
+                  "shareBalancesSlot.slot" in output and "readMap" in output,
+                  "#print Storage.shareBalances reads through the named slot handle")
         finally:
             probe.unlink(missing_ok=True)
 
@@ -234,30 +242,99 @@ def source_digest() -> str:
         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;"),
+        def slot_numbers() -> list[str]:
+            slot_probe = root / ".lake/solidity-import/SlotProbe.lean"
+            try:
+                slot_probe.write_text(
+                    "import Contracts.VaultFromSolidity.VaultFromSolidity\n"
+                    "#eval [Contracts.VaultFromSolidity.totalAssetsSlot.slot,"
+                    " Contracts.VaultFromSolidity.totalSupplySlot.slot,"
+                    " Contracts.VaultFromSolidity.shareBalancesSlot.slot]\n"
+                )
+                return re.findall(r"\[\d+, \d+, \d+\]", run(root, [LAKE, "env", "lean", str(slot_probe)]))
+            finally:
+                slot_probe.unlink(missing_ok=True)
+
+        declarations = b"    uint256 public totalAssets;\n    uint256 public totalSupply;\n"
+        check(original.count(declarations) == 1 and slot_numbers() == ["[0, 1, 2]"],
+              "baseline storage layout puts totalAssets, totalSupply, shareBalances at slots 0, 1, 2")
+        edit_source(original.replace(
+            declarations, b"    uint256 public totalSupply;\n    uint256 public totalAssets;\n"))
+        build()
+        check(slot_numbers() == ["[1, 0, 2]"],
+              "reordering state variables binds the spec names to the new slots and proofs still pass")
+        edit_source(original)
+        build()
+
+        edit_source(original.replace(b"totalAssets", b"assetsTotal"))
+        output = build(False, "Invalid field `totalAssets`")
+        check(re.search(r"Contracts/VaultFromSolidity/Spec\.lean:\d+:\d+:", output) is not None,
+              "renaming a state variable makes the named spec fail to elaborate")
+        edit_source(original)
+        build()
+
+        def broken_theorems(output: str) -> set[str]:
+            error_lines = [int(value) for value in re.findall(
+                r"Contracts/VaultFromSolidity/Proofs/ExecutionProof\.lean:(\d+):", output)]
+            return {name for name, (start, end) in theorem_ranges.items()
+                    if any(start <= line <= end for line in error_lines)}
+
+        # A behaviour change in Vault.sol must break both the internal exact-state
+        # lemma and the human-facing `*_meets_spec` theorem. Lean adds a failed
+        # theorem with `sorry`, so a spec theorem derived from the exact-state
+        # lemma would keep elaborating; requiring an error inside its own range
+        # shows the spec layer is proved against the imported definitions itself.
+        for name, theorems, old, new in (
+            ("deposit behavior", ("deposit_exact_state", "deposit_meets_spec"),
+             b"totalSupply += assets;", b"totalSupply = assets;"),
+            ("getter behavior", ("balance_exact_state", "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}")
+            output = build(False, "Contracts.VaultFromSolidity.Proofs.ExecutionProof")
+            broken = broken_theorems(output)
+            for theorem in theorems:
+                check(theorem in broken, name + f" mutation breaks {theorem}")
             check(before != artifacts(), name + " preserved-mtime edit refreshes artifacts")
             edit_source(original)
             build()
 
+        # The spec layer is not vacuous: a wrong promise in Spec.lean is unprovable
+        # against the unchanged Solidity, and the failure lands in the spec
+        # theorem, not in the exact-state lemmas.
+        spec = root / "Contracts/VaultFromSolidity/Spec.lean"
+        spec_original = spec.read_bytes()
+        for name, theorem, old, new in (
+            ("deposit spec without the supply increment", "deposit_meets_spec",
+             b"post.totalSupply = pre.totalSupply + amount", b"post.totalSupply = pre.totalSupply"),
+            ("withdraw spec without the supply decrement", "withdraw_meets_spec",
+             b"post.totalSupply = pre.totalSupply - amount", b"post.totalSupply = pre.totalSupply"),
+            ("getter spec returning the wrong variable", "balance_meets_spec",
+             b"result = v.shareBalances account", b"result = v.totalSupply"),
+        ):
+            check(spec_original.count(old) == 1, name + " mutation has one spec target")
+            spec.write_bytes(spec_original.replace(old, new))
+            try:
+                output = build(False, "Contracts.VaultFromSolidity.Proofs.ExecutionProof")
+            finally:
+                spec.write_bytes(spec_original)
+            broken = broken_theorems(output)
+            check(theorem in broken, name + f" is unprovable: breaks {theorem}")
+            check(not any(candidate.endswith("_exact_state") for candidate in broken),
+                  name + " leaves the exact-state lemmas untouched")
+        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"),
+            ("reserved Storage name", b"uint256 public totalSupply;",
+             b"uint256 public totalSupply;\n    uint256 public Storage;", "unsupported/reserved name"),
         ):
             edit_source(original.replace(old, new))
             output = build(False, diagnostic)
@@ -395,8 +472,10 @@ def mutate(x):
     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
+                 "totalAssets", "totalSupply", "shareBalances", "deposit", "sourceDigest",
+                 "Storage", "Storage.totalAssets", "Storage.totalSupply",
+                 "Storage.shareBalances", "view"] do
+    if (← getEnv).contains (`Broken ++ suffix.toName) then
       throwError "partial declaration escaped rollback: {suffix}"
   logInfo "KERNEL_REJECTION_ROLLED_BACK"
 ''')