Import Solidity function slices with execution coverage and A/B/C validation

.github/CODEOWNERS

@@ -7,8 +7,8 @@
 * @Th0rgal
 
 # Axioms and trust assumptions — any change weakens guarantees
-AXIOMS.md @Th0rgal
-TRUST_ASSUMPTIONS.md @Th0rgal
+docs/AXIOMS.md @Th0rgal
+docs/TRUST_ASSUMPTIONS.md @Th0rgal
 
 # Lean proof files — ensure no sorry regressions
 Verity/Proofs/ @Th0rgal
@@ -20,10 +20,8 @@ Verity/Specs/ @Th0rgal
 Verity/Core.lean @Th0rgal
 
 # Compiler trusted code — bugs here break soundness
-Compiler/Specs.lean @Th0rgal
 Compiler/IR.lean @Th0rgal
 Compiler/Codegen.lean @Th0rgal
-Compiler/Interpreter.lean @Th0rgal
 
 # CI pipeline — governs what gets checked
 .github/workflows/ @Th0rgal

.github/ocr/rules.json

@@ -1,7 +1,7 @@
 {
   "rules": [
     {
-      "path": "{AUDIT.md,TRUST_ASSUMPTIONS.md,AXIOMS.md}",
+      "path": "docs/{TRUST_ASSUMPTIONS.md,AXIOMS.md}",
       "rule": "Treat trust-boundary documentation changes as high-risk. Check whether a code/proof change weakens, broadens, or silently depends on assumptions, axioms, admitted facts, trusted external semantics, compiler equivalence, or audit exclusions. Flag any mismatch between these docs and changed Lean/Solidity/Yul/Cairo code. Prefer concrete line-linked findings; do not comment on wording unless it changes the trust model.",
       "merge_system_rule": true
     },
@@ -50,9 +50,8 @@
     "**/*.sol",
     "**/*.yul",
     "**/*.cairo",
-    "AUDIT.md",
-    "TRUST_ASSUMPTIONS.md",
-    "AXIOMS.md",
+    "docs/TRUST_ASSUMPTIONS.md",
+    "docs/AXIOMS.md",
     "README.md",
     "docs/**/*.md",
     ".github/**/*"

.github/scripts/ocr-router.js

@@ -1345,7 +1345,7 @@ function countCategories(included, supportedFiles) {
 function categorize(filePath) {
   const base = path.posix.basename(filePath);
   if (filePath.endsWith('.lean')) return 'lean';
-  if (['AUDIT.md', 'TRUST_ASSUMPTIONS.md', 'AXIOMS.md'].includes(base)) return 'trust-doc';
+  if (['TRUST_ASSUMPTIONS.md', 'AXIOMS.md'].includes(base)) return 'trust-doc';
   if (filePath.startsWith('.github/')) return 'workflow-script';
   if (/\.(sol|yul|cairo)$/.test(filePath)) return 'contract';
   if (filePath === 'README.md' || (filePath.startsWith('docs/') && filePath.endsWith('.md'))) return 'doc';
@@ -1358,7 +1358,7 @@ function isSupported(filePath) {
   const base = path.posix.basename(filePath);
   return filePath.endsWith('.lean') ||
     /\.(sol|yul|cairo)$/.test(filePath) ||
-    ['AUDIT.md', 'TRUST_ASSUMPTIONS.md', 'AXIOMS.md', 'README.md'].includes(base) ||
+    ['TRUST_ASSUMPTIONS.md', 'AXIOMS.md', 'README.md'].includes(base) ||
     (filePath.startsWith('docs/') && filePath.endsWith('.md')) ||
     filePath.startsWith('.github/') ||
     /\.(py|sh|bash|js|ts|json|ya?ml|toml)$/.test(filePath);

.github/workflows/verify.yml

@@ -28,9 +28,7 @@ on:
       - 'lean-toolchain'
       - 'foundry.toml'
       - 'Makefile'
-      - 'AXIOMS.md'
       - 'README.md'
-      - 'TRUST_ASSUMPTIONS.md'
   pull_request:
     types: [opened, synchronize, reopened, closed]
     paths:
@@ -56,9 +54,7 @@ on:
       - 'lean-toolchain'
       - 'foundry.toml'
       - 'Makefile'
-      - 'AXIOMS.md'
       - 'README.md'
-      - 'TRUST_ASSUMPTIONS.md'
   workflow_dispatch:
     inputs:
       clean_build:
@@ -231,6 +227,11 @@ jobs:
               - 'packages/**'
               - 'lakefile.lean'
               - 'lake-manifest.json'
+              - 'scripts/solidity_differential/**'
+              - 'scripts/solidity_import_differential.py'
+              - 'scripts/check_solidity_differential.sh'
+              - 'scripts/solidity_import_mutations.py'
+              - 'scripts/setup_solc_import.py'
               - 'lean-toolchain'
             compiler:
               - '.github/actions/**'
@@ -255,6 +256,11 @@ jobs:
               - 'scripts/property_utils.py'
               - 'lakefile.lean'
               - 'lake-manifest.json'
+              - 'scripts/solidity_differential/**'
+              - 'scripts/solidity_import_differential.py'
+              - 'scripts/check_solidity_differential.sh'
+              - 'scripts/solidity_import_mutations.py'
+              - 'scripts/setup_solc_import.py'
               - 'lean-toolchain'
               - 'foundry.toml'
       - name: Resolve effective change flags
@@ -391,11 +397,6 @@ 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
@@ -424,6 +425,12 @@ jobs:
             exit "${build_status}"
           fi
 
+      - name: Check Solidity slice imports and mutation regressions
+        run: |
+          python3 scripts/setup_solc_import.py
+          lake build SolidityImportSmoke
+          python3 scripts/solidity_import_mutations.py
+
       - name: Check storage layout audit artifacts (#1897)
         run: make verify-storage-layout
 
@@ -1228,6 +1235,38 @@ jobs:
         if: steps.local-restore-compiler-workspace.outcome != 'success'
         run: tar -xf lean-workspace-compiler-build.tar
 
+      - name: Install Foundry for Solidity slice comparisons
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: v1.5.0
+
+      - name: Compare Solidity, Denote and compiled models
+        timeout-minutes: 10
+        run: |
+          scripts/check_solidity_differential.sh --config Contracts/SolidityImportSmoke/differential.json --output .lake/import-differential/smoke --cases 128 --seed 2438
+          scripts/check_solidity_differential.sh --config Contracts/SolidityImportSmoke/differential-loss.json --output .lake/import-differential/loss --cases 64 --seed 2438
+          scripts/check_solidity_differential.sh --programs 5 --cases 16 --seed 2438 --output .lake/import-differential/programs
+
+      - name: Extended Solidity slice campaigns
+        if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+        timeout-minutes: 60
+        run: |
+          scripts/check_solidity_differential.sh --config Contracts/SolidityImportSmoke/differential.json --output .lake/import-differential/nightly-inputs --cases 2048 --seed "$GITHUB_RUN_NUMBER"
+          scripts/check_solidity_differential.sh --programs 20 --cases 64 --seed "$GITHUB_RUN_NUMBER" --output .lake/import-differential/nightly-programs
+          scripts/check_solidity_differential.sh --mutations --output .lake/import-differential/mutants
+
+      - name: Archive Solidity slice comparison evidence
+        if: always()
+        uses: actions/upload-artifact@v7
+        with:
+          name: solidity-import-differential
+          path: |
+            .lake/import-differential/**
+            !.lake/import-differential/**/.lake/build/**
+            !.lake/import-differential/**/.lake/packages/**
+          include-hidden-files: true
+          retention-days: 14
+
       - name: Build compiler CLI regression executable
         run: stdbuf -oL -eL lake build compiler-main-test