Proof-only solidity_contract import for Vault

.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

.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

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.

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: