feat: named storage view for VaultFromSolidity

[fricoben]

Answers Quentin's (Morpho) review on #2407: "referencing mapping names instead of slots would make it easier to read".

What changes

The Lean importer now also registers a read-only, named storage view for the imported contract, and Spec.lean is rewritten on top of it:

• Storage (a definition equal to ContractState)
• Storage.<var>, one reader per state variable, reading through the solc-derived <var>Slot handle
• view : ContractState → Storage

These are safe transparent defnDecls registered through the existing register path, so kernel checking, collision checks, and rollback all still apply. Storage and view are reserved Solidity names.

Before

-- slot 0 = totalAssets, slot 1 = totalSupply (only a comment says so)
def solvent (s : ContractState) : Prop := s.readSlot 0 = s.readSlot 1

def deposit_execution (s : ContractState) (amount : Uint256) : Prop :=
  (deposit amount).run s = ContractResult.success ()
    (accountingState s (s.readMap 2 s.sender + amount)
      (s.readSlot 0 + amount) (s.readSlot 1 + amount))

After

def solvent (v : Storage) : Prop := v.totalAssets = v.totalSupply

def deposit_spec (amount : Uint256) (caller : Address) (pre post : Storage) : Prop :=
  post.totalAssets = pre.totalAssets + amount ∧
  post.totalSupply = pre.totalSupply + amount ∧
  post.shareBalances caller = pre.shareBalances caller + amount ∧
  ∀ other, other ≠ caller → post.shareBalances other = pre.shareBalances other

Details

• Proofs/Execution.lean is renamed to Proofs/ExecutionProof.lean. The five public theorem names are kept and restated over the named spec. They are derived from three new exact-state lemmas: deposit_exact_state, withdraw_exact_state, and balance_exact_state. accountingState now lives in the proof file and uses slot handles rather than numbers.
• New spec_named_storage lean_lint rule, run in make check: opted-in spec files (currently Contracts/VaultFromSolidity/Spec.lean) must not use numeric slot literals or knownAddresses.
• Acceptance suite additions:
  • dot-notation and #print probes for the view
  • rollback coverage for the new declarations
  • reorder mutation: swapping totalAssets/totalSupply moves the solc slots [0,1,2] → [1,0,2], and all proofs still build
  • rename mutation: totalAssets → assetsTotal makes Spec.lean fail to elaborate
  • a state variable named Storage is rejected with its source position
• TRUST_ASSUMPTIONS.md, AUDIT.md, AXIOMS.md, and README.md are updated. PrintAxioms.lean and the verification status files are regenerated (VaultFromSolidity: 5 → 8 theorems).

Evidence

• lake build VaultFromSolidity: passes.
• python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py: all 55 checks pass. The 8 audited theorems depend only on propext and Quot.sound.
• make check: passes. Adding s.readSlot 0 to Spec.lean makes spec_named_storage fail.

Out of scope: named views for handwritten verity_contract contracts; structs, nested mappings, and packed slots.