Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
446 commits
Select commit Hold shift + click to select a range
1ff0d2b
Move native result surface to harness
Th0rgal May 5, 2026
441b1a5
Add native projected result match intro
Th0rgal May 5, 2026
717778c
Lift native projected result match to runtime
Th0rgal May 5, 2026
9475558
Add compiled native projected result seams
Th0rgal May 5, 2026
18fda54
Move singleton native lowering fact to harness
Th0rgal May 5, 2026
2d8f71f
Package native environment validation for IR tx
Th0rgal May 5, 2026
2c7fc8b
Add native public env closure seams
Th0rgal May 5, 2026
6fb9c57
Add native global-default env closure seams
Th0rgal May 5, 2026
d64deeb
Name compiled native fragment validation seam
Th0rgal May 5, 2026
0333a3c
Package helper-free native lowering seam
Th0rgal May 5, 2026
1be24a7
Add no-mapping dispatcher lowering wrappers
Th0rgal May 5, 2026
64c6e07
Add no-mapping dispatcher env wrappers
Th0rgal May 5, 2026
eedb0da
Add layer3 no-mapping dispatcher env wrappers
Th0rgal May 5, 2026
d64046f
Package native mapping helper lowering
Th0rgal May 5, 2026
b25794e
Add native mapping dispatcher lowering wrappers
Th0rgal May 5, 2026
20ef1ad
Add mapping dispatcher env wrappers
Th0rgal May 5, 2026
23481e3
Add mapping dispatcher layer23 wrappers
Th0rgal May 5, 2026
bdee387
Add mapping dispatcher layer3 wrappers
Th0rgal May 5, 2026
2353b03
Track mapping reserved native transition surface
Th0rgal May 5, 2026
4982856
Expose native dispatcher lowering from successful runtime lowering
Th0rgal May 5, 2026
d309758
Compose runtime lowering with dispatcher statement wrappers
Th0rgal May 5, 2026
f46bccd
Lift runtime dispatcher statement wrappers to layer3
Th0rgal May 5, 2026
8b4f28f
Lift runtime dispatcher statement wrappers to layer23
Th0rgal May 5, 2026
64c17e5
Route SimpleStorage native proof through runtime dispatcher seam
Th0rgal May 5, 2026
93e0446
Rename EVMYulLean backend theorem off oracle alias
Th0rgal May 5, 2026
1ab1aa1
Expose lowered runtime native env wrappers
Th0rgal May 5, 2026
16b40c8
Deprecate fuel wrapper EndToEnd surface
Th0rgal May 5, 2026
7d6d9f3
Expose slim native EndToEnd seams
Th0rgal May 5, 2026
45fab1a
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
052e39b
Split neutral Yul runtime types
Th0rgal May 5, 2026
c0535c4
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
4302be1
Move YulState to neutral runtime types
Th0rgal May 5, 2026
08e3ce2
Make EndToEnd native surface authoritative
Th0rgal May 5, 2026
8e6786b
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
d181959
Remove EndToEnd legacy EVMYulLean wrappers
Th0rgal May 5, 2026
f6f8ae4
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
62e2ad3
Keep native identity seams private
Th0rgal May 5, 2026
54b3a38
Add canonical native dispatcher fuel wrappers
Th0rgal May 5, 2026
799869c
Add canonical native project wrappers
Th0rgal May 5, 2026
12350ce
Add canonical native layer3 wrappers
Th0rgal May 5, 2026
91558c2
Add canonical native runtime wrappers
Th0rgal May 5, 2026
7f52c6c
Add canonical no-mapping dispatcher wrappers
Th0rgal May 5, 2026
7c2ab29
Add canonical mapping dispatcher wrappers
Th0rgal May 5, 2026
0bb7c07
Add canonical layer3 dispatcher wrappers
Th0rgal May 5, 2026
83fdc43
Add canonical native dispatcher wrappers
Th0rgal May 5, 2026
3dc35b8
Add canonical lowered native wrappers
Th0rgal May 5, 2026
0275a22
Add canonical lowered layer3 wrappers
Th0rgal May 5, 2026
f7b980d
Add canonical lowered layer2 wrappers
Th0rgal May 5, 2026
b9fb9b5
Add canonical dispatcher exec match wrappers
Th0rgal May 5, 2026
592480d
Keep legacy EVMYulLean retarget private
Th0rgal May 5, 2026
0dd6992
Keep backend interpreter retarget private
Th0rgal May 5, 2026
658870d
Keep backend fuel retarget private
Th0rgal May 5, 2026
a9a537a
Keep expression bridge retarget private
Th0rgal May 5, 2026
1d76829
Isolate legacy Yul preservation from EndToEnd
Th0rgal May 5, 2026
2ad4ff7
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
b79d6db
Remove legacy imports from native harness path
Th0rgal May 5, 2026
57b1366
Isolate native smoke legacy oracle import
Th0rgal May 5, 2026
991d295
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
c18ce2e
Split native bridge predicates from retarget
Th0rgal May 5, 2026
170f247
chore: auto-refresh derived artifacts
github-actions[bot] May 5, 2026
e2300fa
Add native pure builtin reductions
Th0rgal May 5, 2026
bf41907
Localize IR sload reduction
Th0rgal May 5, 2026
d7d4253
Guard EndToEnd against legacy backend terms
Th0rgal May 5, 2026
c0fecd6
Expand native pure builtin reductions
Th0rgal May 5, 2026
6457d0c
Add native signed comparison reductions
Th0rgal May 5, 2026
9b24d45
Add native sdiv reduction
Th0rgal May 5, 2026
4d135f9
Add native smod reduction
Th0rgal May 5, 2026
76ec92a
Add native sar reduction
Th0rgal May 5, 2026
bad4ed1
Retarget IR and Yul builtin dispatch to native backend
Th0rgal May 5, 2026
398e007
Isolate native builtin semantics from reference oracle
Th0rgal May 5, 2026
e4b6c54
Split contract shape facts from proof stack
Th0rgal May 5, 2026
b67382c
Hide native match premise wrappers
Th0rgal May 5, 2026
4bfb415
Keep native dispatcher lift premises private
Th0rgal May 5, 2026
561ec9e
Make native dispatcher match predicate private
Th0rgal May 5, 2026
1ba62b6
Hide unused all-storage native result surface
Th0rgal May 5, 2026
5727397
Keep generated runtime helpers private
Th0rgal May 5, 2026
2d7d4a5
Keep SimpleStorage reduction helpers private
Th0rgal May 5, 2026
4e2bb91
Compose source correctness with native runtime
Th0rgal May 5, 2026
a74971f
Split neutral IR fuel aliases from legacy Yul equivalence
Th0rgal May 5, 2026
2a0bf1e
Remove duplicate legacy oracle imports
Th0rgal May 5, 2026
d700f06
Stop root aggregate re-exporting legacy Yul proofs
Th0rgal May 5, 2026
e4e7c43
Keep legacy Yul function equivalence file-local
Th0rgal May 5, 2026
529ca1e
Narrow legacy Yul equivalence helpers
Th0rgal May 5, 2026
3922cdb
Localize legacy Yul runtime wrappers
Th0rgal May 5, 2026
c4812d2
Keep legacy statement equivalence file-local
Th0rgal May 5, 2026
725ead4
Keep legacy preservation predicates file-local
Th0rgal May 5, 2026
9b8ed92
Keep EndToEnd native reduction helpers file-local
Th0rgal May 5, 2026
92b7590
Isolate legacy statement equivalence import
Th0rgal May 5, 2026
3f27bb8
Keep retarget bridge closure witnesses file-local
Th0rgal May 5, 2026
fffbb57
Hide EndToEnd arbitrary native fuel seam
Th0rgal May 5, 2026
69facbc
Hide native runtime match fuel predicate
Th0rgal May 5, 2026
e388357
Update native EndToEnd public surface docs
Th0rgal May 5, 2026
2247a8a
Refresh proof axiom audit after native surface cleanup
Th0rgal May 5, 2026
56d2d31
Keep SimpleStorage native harness helpers file-local
Th0rgal May 5, 2026
732796c
Isolate macro legacy Yul regression imports
Th0rgal May 5, 2026
fef5823
Stop retarget importing legacy preservation
Th0rgal May 5, 2026
8771f22
Move Yul exec result projection to runtime types
Th0rgal May 5, 2026
72b2dc3
Localize retarget backend eval helpers
Th0rgal May 5, 2026
b97c17d
Hide retarget target predicate
Th0rgal May 5, 2026
52c2e3b
Hide reference oracle builtin helper facts
Th0rgal May 5, 2026
4d99d1e
Localize legacy Yul dispatch lemmas
Th0rgal May 5, 2026
744b63d
Hide legacy Yul sequence unfolding facts
Th0rgal May 5, 2026
d22175e
Hide legacy codegen selector helpers
Th0rgal May 5, 2026
7a69bd5
Hide legacy codegen switch reducers
Th0rgal May 5, 2026
af4d199
Hide legacy codegen switch shapes
Th0rgal May 5, 2026
d7ba8aa
Hide legacy equivalence predicates
Th0rgal May 5, 2026
f04333e
Guard native legacy proof boundary
Th0rgal May 5, 2026
5dbc195
Expose native supported compiler theorem
Th0rgal May 5, 2026
119386c
Expose native dispatcher compiler theorem
Th0rgal May 5, 2026
14d4d26
Derive native theorem static params from support
Th0rgal May 5, 2026
ace7a61
Widen native source expression bridge
Th0rgal May 5, 2026
cb932e3
Widen native branchless expression bridge
Th0rgal May 5, 2026
542c3e9
Bridge native environment source reads
Th0rgal May 5, 2026
f4d86f9
Bridge native unary source reads
Th0rgal May 5, 2026
6dbb2e5
Bridge compile-core memory safe bodies
Th0rgal May 5, 2026
2b865c1
Widen native safe-body singleton coverage
Th0rgal May 5, 2026
ff38ce8
Package compile-core native safe bodies
Th0rgal May 5, 2026
e4bfb0a
Retarget arithmetic profile to native evaluator
Th0rgal May 5, 2026
c3a71b2
Package public native body closure
Th0rgal May 5, 2026
c1d708d
Expose native env facts in dispatcher theorem
Th0rgal May 5, 2026
f5618cf
Expose SimpleStorage native env facts
Th0rgal May 5, 2026
ad63c44
Add no-mapping native dispatcher wrapper
Th0rgal May 5, 2026
9b1641b
Add mapping native dispatcher wrapper
Th0rgal May 5, 2026
a28dbd1
Update native verification status
Th0rgal May 5, 2026
9dfd6b5
Refresh native transition done criteria
Th0rgal May 5, 2026
e6d2aa7
Document native proof surface
Th0rgal May 5, 2026
b12c99b
Guard native public import boundary
Th0rgal May 5, 2026
b12deb1
Guard public native theorem signatures
Th0rgal May 5, 2026
1a52540
Guard public native fuel surface
Th0rgal May 5, 2026
8f77190
Add native callDispatcher correctness wrapper
Th0rgal May 5, 2026
a5caeae
Add lowered native callDispatcher wrappers
Th0rgal May 5, 2026
c6239d4
Document native callDispatcher public surface
Th0rgal May 5, 2026
7dd557c
Guard retarget imports at native public boundary
Th0rgal May 5, 2026
8d7c6e4
Guard native adapter public imports
Th0rgal May 5, 2026
91d951f
Guard transitive native public imports
Th0rgal May 5, 2026
9d3e90c
Guard transitive native public legacy terms
Th0rgal May 6, 2026
f0f3f05
Privatize transition pure bridge helper
Th0rgal May 6, 2026
f41cd02
Keep generated dispatcher exec helpers private
Th0rgal May 6, 2026
7de0444
Privatize legacy Yul fuel simp lemmas
Th0rgal May 6, 2026
2fe9bbf
Keep builtin backend aliases private
Th0rgal May 6, 2026
9ae4746
Privatize default builtin call wrapper
Th0rgal May 6, 2026
b00517c
Guard public EndToEnd builtin wrapper mentions
Th0rgal May 6, 2026
cf98931
Describe native bridge predicates without legacy authority
Th0rgal May 6, 2026
80ba3de
Split neutral Yul log-name helper
Th0rgal May 6, 2026
d5febcf
Split IR runtime records from interpreter
Th0rgal May 6, 2026
005a16f
Decouple native harness from IR interpreter
Th0rgal May 6, 2026
03a4a53
Avoid root IR interpreter re-export
Th0rgal May 6, 2026
e1cd096
Expose direct native callDispatcher result theorem
Th0rgal May 6, 2026
1e25779
Target lowered native wrappers at callDispatcher result
Th0rgal May 6, 2026
9569066
Hide generated callDispatcher adapter theorem
Th0rgal May 6, 2026
a7b6d78
Keep generic native adapter theorem private
Th0rgal May 6, 2026
201ece9
Hide adapter correctness transition lemmas
Th0rgal May 6, 2026
03ab782
Guard adapter correctness private surface
Th0rgal May 6, 2026
0b357e2
Target SimpleStorage public theorem at callDispatcher
Th0rgal May 6, 2026
ee5387d
Keep native source-result helper private
Th0rgal May 6, 2026
28df6f1
Narrow public callDispatcher theorem assumptions
Th0rgal May 6, 2026
3a682f1
Guard public callDispatcher signatures
Th0rgal May 6, 2026
1de8b25
Keep SimpleStorage native scaffold private
Th0rgal May 6, 2026
1c0db41
Keep body-closure scaffold private
Th0rgal May 6, 2026
fba47df
Guard bridge lemma import isolation
Th0rgal May 6, 2026
1d41540
Guard ReferenceOracle import isolation
Th0rgal May 6, 2026
8159e57
Guard base callDispatcher public target
Th0rgal May 6, 2026
f731147
Remove SimpleStorage native runtime wrapper
Th0rgal May 6, 2026
c857213
Remove generated native runtime adapters
Th0rgal May 6, 2026
96394e9
Update native runtime roadmap status
Th0rgal May 6, 2026
5b83aae
Remove orphan native body-closure adapters
Th0rgal May 6, 2026
4095927
Clarify native theorem transition boundary
Th0rgal May 6, 2026
dae241d
Remove unused layers2 native runtime wrapper
Th0rgal May 6, 2026
b5c2c20
Remove unused native runtime canonical wrapper
Th0rgal May 6, 2026
8b5c848
Remove unused native projected canonical wrapper
Th0rgal May 6, 2026
870b15f
Remove unused layer3 canonical runtime wrapper
Th0rgal May 6, 2026
f13496d
Remove unused external bodies canonical wrapper
Th0rgal May 6, 2026
9996e79
Remove unused projected canonical wrapper
Th0rgal May 6, 2026
85168dd
Remove unused layer3 projected canonical wrapper
Th0rgal May 6, 2026
618dc93
Remove unused supported external canonical wrappers
Th0rgal May 6, 2026
c6c7d22
Remove unused layer3 body closure canonical wrappers
Th0rgal May 6, 2026
328dfe5
Remove unused native positive environment canonical wrappers
Th0rgal May 6, 2026
2cff352
Remove unused native positive canonical wrapper
Th0rgal May 6, 2026
06dad9f
Remove unused native projected environment canonical wrappers
Th0rgal May 6, 2026
e7cb53d
Remove unused native projected canonical wrapper
Th0rgal May 6, 2026
4d9f805
Remove unused native dispatcher canonical wrappers
Th0rgal May 6, 2026
d31114c
Remove unused native no-mapping env canonical wrappers
Th0rgal May 6, 2026
c79ead5
Remove unused native mapping env canonical wrappers
Th0rgal May 6, 2026
2257f9c
Remove unused native lowered dispatcher canonical wrappers
Th0rgal May 6, 2026
8e61410
Remove unused layer3 lowered dispatcher canonical wrappers
Th0rgal May 6, 2026
243e546
Remove unused layers23 lowered dispatcher canonical wrappers
Th0rgal May 6, 2026
a1ad5e3
Remove unused layers23 lowered environment canonical wrappers
Th0rgal May 6, 2026
16f53b5
Remove unused layer3 dispatcher environment canonical wrappers
Th0rgal May 6, 2026
90666c0
Remove unused layers23 dispatcher exec canonical wrappers
Th0rgal May 6, 2026
31d0f6e
Remove remaining layers23 dispatcher canonical wrappers
Th0rgal May 6, 2026
22a71fc
Fail closed on native selfbalance boundary
Th0rgal May 6, 2026
b5ad087
Bridge source keccak expressions syntactically
Th0rgal May 6, 2026
5f2d4e1
Name source keccak compile-core bridge
Th0rgal May 6, 2026
7542eed
Guard source keccak closure theorem
Th0rgal May 6, 2026
0a92ecf
Package source keccak bindings as safe bodies
Th0rgal May 6, 2026
d124c4e
Package mstore keccak preimage bodies
Th0rgal May 6, 2026
103d7f4
Bridge storage reads in source expression closure
Th0rgal May 6, 2026
425ee7c
Bridge storage array length reads
Th0rgal May 6, 2026
990e06a
Bridge ADT storage reads
Th0rgal May 6, 2026
ecd9f0f
Bridge parameter length reads
Th0rgal May 6, 2026
914f9ec
Bridge reserved exponentiation source expressions
Th0rgal May 6, 2026
ea84a4f
Bridge singleton mapping source reads
Th0rgal May 6, 2026
1f27e95
Bridge nested mapping source reads
Th0rgal May 6, 2026
f085768
Bridge struct member source reads
Th0rgal May 6, 2026
b3e9d09
Bridge struct member2 source reads
Th0rgal May 6, 2026
9cd9dfc
Bridge mapping chain source expressions
Th0rgal May 6, 2026
2ecdb3f
chore: auto-refresh derived artifacts
github-actions[bot] May 6, 2026
b350fb8
Sync native Yul boundary checks
Th0rgal May 6, 2026
3ac4531
Add DGX CI resource profiling notes
Th0rgal May 6, 2026
d3e3705
Prove native generated dispatcher closure
Th0rgal May 7, 2026
b8029d9
chore: auto-refresh derived artifacts
github-actions[bot] May 7, 2026
d82dd41
Prove more native dispatcher generated paths
Th0rgal May 9, 2026
727f116
Tighten native transition documentation checks
Th0rgal May 9, 2026
075235f
Refresh proof axiom report
Th0rgal May 9, 2026
a66392d
Align legacy preservation with cleared return values
Th0rgal May 9, 2026
d7eb2b5
Allowlist native dispatcher proof spans
Th0rgal May 9, 2026
ca5d627
Move calldata threshold into SupportedSpec
Th0rgal May 9, 2026
a71f65f
chore: auto-refresh derived artifacts
github-actions[bot] May 9, 2026
be72793
Hide lowering witness from public native theorem
Th0rgal May 9, 2026
e14b5da
Retarget public source theorem to native runtime
Th0rgal May 9, 2026
5102b18
Document selected body bridge proof gaps
Th0rgal May 9, 2026
5cd9812
Package selected body switch freshness
Th0rgal May 9, 2026
b8a6199
Add native lowering determinism helper
Th0rgal May 9, 2026
421d17c
Prove mapping-free switch freshness preservation
Th0rgal May 9, 2026
4ede904
Bridge mapping-free selected exec with switch freshness
Th0rgal May 9, 2026
6dc0ac1
Add mapping-free switch-fresh dispatcher wrapper
Th0rgal May 9, 2026
f246a82
Tighten switch freshness dispatcher premise
Th0rgal May 9, 2026
4765c99
Add switch case freshness proof assets
Th0rgal May 9, 2026
eb24a0e
Raise verify checks timeout
Th0rgal May 9, 2026
550de14
Quarantine native result match wrapper
Th0rgal May 9, 2026
61ed6d1
Quarantine native lowering hLower wrappers
Th0rgal May 9, 2026
7498180
Quarantine native result lowering helpers
Th0rgal May 9, 2026
0c2135c
Add selected body closure guard assets
Th0rgal May 9, 2026
b37b166
Pin selected body closure transition guard
Th0rgal May 9, 2026
ff4e341
Add selected body artifact handoff lemmas
Th0rgal May 9, 2026
6764ad7
Document selected body freshness handoff blocker
Th0rgal May 9, 2026
4b3604f
Add mapping switch freshness success adapter
Th0rgal May 9, 2026
981011c
Add mapping switch freshness dispatcher wrapper
Th0rgal May 9, 2026
05dd96b
Add case freshness dispatcher adapters
Th0rgal May 9, 2026
5535376
Document G1 incremental plan for Revived exec bridge
Th0rgal May 11, 2026
a5d2e0d
Add .of_block_leave Revived exec bridge constructor
Th0rgal May 11, 2026
215233f
chore: auto-refresh derived artifacts
github-actions[bot] May 11, 2026
8b46a6e
Add .of_block_empty Revived exec bridge constructor
Th0rgal May 11, 2026
ed60faa
chore: auto-refresh derived artifacts
github-actions[bot] May 11, 2026
06723c8
Add .of_singleton_comment Revived exec bridge constructor
Th0rgal May 11, 2026
8e31e75
Defer G1 step 4 (.of_comment_cons) to wiring layer
Th0rgal May 11, 2026
ce892d0
chore: auto-refresh derived artifacts
github-actions[bot] May 11, 2026
f67d081
Track G1 increment status and remaining sketches
Th0rgal May 11, 2026
f19f5c8
Summarize PR 1822 achievement and scope follow-up
Th0rgal May 11, 2026
06d2aea
Fix flaky source-level dispatcher public-note test
Th0rgal May 11, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions .github/actions/setup-lean/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -221,6 +221,11 @@ runs:
--path ".lake/build" \
--fallback-key "${{ steps.persistence.outputs.build_main_fallback_sticky_key }}"

- name: Prune stale sticky Lake packages
if: steps.persistence.outputs.use_sticky_disks == 'true'
shell: bash
run: python3 scripts/prune_lake_cache.py --packages-only

- name: Refresh Lake dependency state on partial cache hit
if: steps.persistence.outputs.use_sticky_disks != 'true' && steps.cache-lake.outputs.cache-hit != 'true'
shell: bash
Expand Down
38 changes: 31 additions & 7 deletions .github/actions/setup-solc/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,41 @@ runs:
id: cache-solc
uses: actions/cache@v5
with:
path: /usr/local/bin/solc
path: .cache/solc/${{ env.SOLC_VERSION }}
key: solc-${{ env.SOLC_VERSION }}

- name: Install solc
if: steps.cache-solc.outputs.cache-hit != 'true'
- name: Install or repair solc
shell: bash
run: |
curl -sSfL "$SOLC_URL" -o solc
echo "${SOLC_SHA256} solc" | sha256sum -c -
sudo mv solc /usr/local/bin/solc
sudo chmod +x /usr/local/bin/solc
solc_bin_dir="$PWD/.cache/solc/${SOLC_VERSION}"
solc_path="${solc_bin_dir}/solc"
mkdir -p "$solc_bin_dir"
echo "$solc_bin_dir" >> "$GITHUB_PATH"

if [ -x "$solc_path" ] && "$solc_path" --version | grep -q "$SOLC_VERSION"; then
exit 0
fi

for delay in 0 5 15; do
if [ "$delay" -gt 0 ]; then
echo "::warning::solc install failed; retrying in ${delay}s"
sleep "$delay"
fi

rm -f solc
if \
curl -sSfL --retry 3 --retry-delay 5 "$SOLC_URL" -o solc && \
echo "${SOLC_SHA256} solc" | sha256sum -c - && \
mv solc "$solc_path" && \
chmod +x "$solc_path" && \
"$solc_path" --version | grep -q "$SOLC_VERSION"
then
exit 0
fi
done

echo "::error::Unable to install solc ${SOLC_VERSION}"
exit 1

- name: Verify solc
shell: bash
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/verify.yml
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ jobs:

checks:
runs-on: [self-hosted, linux, ARM64, dgx-spark, verity, fastlane]
timeout-minutes: 5
timeout-minutes: 10
permissions:
contents: write
steps:
Expand Down
11 changes: 0 additions & 11 deletions Compiler.lean
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ import Compiler.Keccak.SpongeProperties
import Compiler.Proofs.KeccakBound
import Compiler.Proofs.MappingSlot
import Compiler.Proofs.IRGeneration.Expr
import Compiler.Proofs.IRGeneration.IRInterpreter
import Compiler.Proofs.IRGeneration.SupportedFragment
import Compiler.Proofs.IRGeneration.Contract
import Compiler.Proofs.IRGeneration.Dispatch
Expand All @@ -39,15 +38,5 @@ import Compiler.Proofs.IRGeneration.ParamLoading
import Compiler.Proofs.IRGeneration.SupportedSpec
import Compiler.Proofs.IRGeneration.SourceSemantics
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeTest
import Compiler.Proofs.YulGeneration.ReferenceOracle.Builtins
import Compiler.Proofs.YulGeneration.Codegen
import Compiler.Proofs.YulGeneration.Equivalence
import Compiler.Proofs.YulGeneration.Lemmas
import Compiler.Proofs.YulGeneration.PatchRulesProofs
import Compiler.Proofs.YulGeneration.Preservation
import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
import Compiler.Proofs.YulGeneration.StatementEquivalence
import Compiler.Proofs.EndToEnd
import Compiler.Proofs.ArithmeticProfile
6 changes: 4 additions & 2 deletions Compiler/CompilationModel/ExpressionCompile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,8 @@ def yulNegatedBinOp (op : String) (a b : YulExpr) : YulExpr :=
def yulToBool (e : YulExpr) : YulExpr :=
YulExpr.call "iszero" [YulExpr.call "iszero" [e]]

private def compileMappingSlotRead (fields : List Field) (field : String) (keyExpr : YulExpr)
-- Exposed so proof modules can name the exact mapping-read lowering shape.
def compileMappingSlotRead (fields : List Field) (field : String) (keyExpr : YulExpr)
(label : String) (wordOffset : Nat := 0) : Except String YulExpr :=
if !isMapping fields field then
throw s!"Compilation error: field '{field}' is not a mapping"
Expand All @@ -33,7 +34,8 @@ private def compileMappingSlotRead (fields : List Field) (field : String) (keyEx
pure (YulExpr.call "sload" [finalSlot])
| none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"

private def compileMappingSlotChain (baseSlot : YulExpr) (keys : List YulExpr) : YulExpr :=
-- Exposed so proof modules can name the exact nested mapping-chain lowering shape.
def compileMappingSlotChain (baseSlot : YulExpr) (keys : List YulExpr) : YulExpr :=
keys.foldl (fun slotExpr keyExpr => YulExpr.call "mappingSlot" [slotExpr, keyExpr]) baseSlot

-- Compile expression to Yul (using mutual recursion for lists)
Expand Down
164 changes: 73 additions & 91 deletions Compiler/Proofs/ArithmeticProfile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,26 +7,22 @@

This file serves as the single formal reference for arithmetic behavior:
- Proves wrapping is consistent across EDSL and compiler layers
- Proves EVMYulLean bridge agreement for pure builtins
- States compiler pure-builtin facts directly against EVMYulLean
- Documents the checked (safe) arithmetic alternative at EDSL level
- Establishes that all backend profiles share identical arithmetic semantics
- Keeps legacy/native bridge comparisons out of the public profile surface

Run: lake build Compiler.Proofs.ArithmeticProfile
-/

import Compiler.Constants
import Compiler.Proofs.IRGeneration.IRStorageWord
import Compiler.Proofs.YulGeneration.ReferenceOracle.Builtins
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanPureBuiltinLemmas
import Verity.Core.Uint256
import EvmYul.UInt256

namespace Compiler.Proofs.ArithmeticProfile

open Compiler.Constants (evmModulus)
open Compiler.Proofs.IRGeneration (IRStorageWord IRStorageSlot)
open Compiler.Proofs.YulGeneration (evalBuiltinCall)
open Compiler.Proofs.YulGeneration.Backends (evalPureBuiltinViaEvmYulLean)

-- ============================================================================
Expand All @@ -44,130 +40,117 @@ theorem evmyullean_size_eq_verity_modulus :
-- § 2. Wrapping semantics: compiler builtins are total and wrapping
-- ============================================================================

-- Dummy state parameters (arithmetic builtins are state-independent).
private def s : IRStorageSlot → IRStorageWord := fun _ => 0
private def sender : Nat := 0
private def sel : Nat := 0
private def cd : List Nat := []

/-- Addition wraps: (a + b) mod 2^256. -/
theorem add_wraps (a b : Nat) :
evalBuiltinCall s sender sel cd "add" [a, b] = some ((a + b) % evmModulus) := by
simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]
evalPureBuiltinViaEvmYulLean "add" [a, b] =
some ((a + b) % evmModulus) := by
simp

/-- Subtraction wraps: (2^256 + a - b) mod 2^256. -/
theorem sub_wraps (a b : Nat) :
evalBuiltinCall s sender sel cd "sub" [a, b] =
evalPureBuiltinViaEvmYulLean "sub" [a, b] =
some ((evmModulus + a % evmModulus - b % evmModulus) % evmModulus) := by
simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]
simp

/-- Multiplication wraps: (a * b) mod 2^256. -/
theorem mul_wraps (a b : Nat) :
evalBuiltinCall s sender sel cd "mul" [a, b] = some ((a * b) % evmModulus) := by
simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]
evalPureBuiltinViaEvmYulLean "mul" [a, b] =
some ((a * b) % evmModulus) := by
simp

/-- Division by zero returns 0. -/
theorem div_by_zero (a : Nat) :
evalBuiltinCall s sender sel cd "div" [a, 0] = some 0 := by
simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]
evalPureBuiltinViaEvmYulLean "div" [a, 0] = some 0 := by
simp

/-- Modulo by zero returns 0. -/
theorem mod_by_zero (a : Nat) :
evalBuiltinCall s sender sel cd "mod" [a, 0] = some 0 := by
simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]
evalPureBuiltinViaEvmYulLean "mod" [a, 0] = some 0 := by
simp

-- ============================================================================
-- § 3. EVMYulLean bridge agreement for pure arithmetic
-- § 3. EVMYulLean pure-builtin facts
-- ============================================================================

-- Arithmetic bridging is now universally proved for add/sub/mul/div/mod.
-- Bitwise `and`/`or`/`xor` plus the shift family now also have direct symbolic bridge lemmas.
-- `not` still retains concrete bridge coverage here.
-- The theorem names retain the historical `_bridge` suffix for downstream
-- compatibility, but their semantic authority is the native EVMYulLean
-- evaluator rather than the legacy Verity Yul oracle.

/-- Universal bridge theorem for addition. -/
/-- Native evaluator theorem for addition. -/
theorem add_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "add" [a, b] =
evalPureBuiltinViaEvmYulLean "add" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_add_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "add" [a, b] =
some ((a + b) % evmModulus) :=
add_wraps a b

/-- Universal bridge theorem for subtraction. -/
/-- Native evaluator theorem for subtraction. -/
theorem sub_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "sub" [a, b] =
evalPureBuiltinViaEvmYulLean "sub" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_sub_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "sub" [a, b] =
some ((evmModulus + a % evmModulus - b % evmModulus) % evmModulus) :=
sub_wraps a b

/-- Universal bridge theorem for multiplication. -/
/-- Native evaluator theorem for multiplication. -/
theorem mul_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "mul" [a, b] =
evalPureBuiltinViaEvmYulLean "mul" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_mul_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "mul" [a, b] =
some ((a * b) % evmModulus) :=
mul_wraps a b

/-- Universal bridge theorem for division. -/
/-- Native evaluator theorem for division. -/
theorem div_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "div" [a, b] =
evalPureBuiltinViaEvmYulLean "div" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_div_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "div" [a, b] =
some (if b % evmModulus = 0 then 0 else (a % evmModulus) / (b % evmModulus)) := by
simp

/-- Universal bridge theorem for modulo. -/
/-- Native evaluator theorem for modulo. -/
theorem mod_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "mod" [a, b] =
evalPureBuiltinViaEvmYulLean "mod" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_mod_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "mod" [a, b] =
some (if b % evmModulus = 0 then 0 else
(a % evmModulus) % (b % evmModulus)) := by
simp

/-- Universal bridge theorem for bitwise and. -/
/-- Native evaluator theorem for bitwise and. -/
theorem and_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "and" [a, b] =
evalPureBuiltinViaEvmYulLean "and" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_and_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "and" [a, b] =
some (EvmYul.UInt256.toNat
(EvmYul.UInt256.land (EvmYul.UInt256.ofNat a) (EvmYul.UInt256.ofNat b))) := by
rfl

/-- Universal bridge theorem for bitwise or. -/
/-- Native evaluator theorem for bitwise or. -/
theorem or_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "or" [a, b] =
evalPureBuiltinViaEvmYulLean "or" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_or_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "or" [a, b] =
some (EvmYul.UInt256.toNat
(EvmYul.UInt256.lor (EvmYul.UInt256.ofNat a) (EvmYul.UInt256.ofNat b))) := by
rfl

/-- Universal bridge theorem for bitwise xor. -/
/-- Native evaluator theorem for bitwise xor. -/
theorem xor_bridge (a b : Nat) :
evalBuiltinCall s sender sel cd "xor" [a, b] =
evalPureBuiltinViaEvmYulLean "xor" [a, b] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_xor_bridge
s sender sel cd a b
evalPureBuiltinViaEvmYulLean "xor" [a, b] =
some (EvmYul.UInt256.toNat
(EvmYul.UInt256.xor (EvmYul.UInt256.ofNat a) (EvmYul.UInt256.ofNat b))) := by
rfl

/-- Universal bridge theorem for shift-left. -/
/-- Native evaluator theorem for shift-left. -/
theorem shl_bridge (shift value : Nat) :
evalBuiltinCall s sender sel cd "shl" [shift, value] =
evalPureBuiltinViaEvmYulLean "shl" [shift, value] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_shl_bridge
s sender sel cd shift value
evalPureBuiltinViaEvmYulLean "shl" [shift, value] =
some (EvmYul.UInt256.toNat
(EvmYul.UInt256.shiftLeft
(EvmYul.UInt256.ofNat value) (EvmYul.UInt256.ofNat shift))) := by
rfl

/-- Universal bridge theorem for shift-right. -/
/-- Native evaluator theorem for shift-right. -/
theorem shr_bridge (shift value : Nat) :
evalBuiltinCall s sender sel cd "shr" [shift, value] =
evalPureBuiltinViaEvmYulLean "shr" [shift, value] := by
exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_shr_bridge
s sender sel cd shift value
evalPureBuiltinViaEvmYulLean "shr" [shift, value] =
some (EvmYul.UInt256.toNat
(EvmYul.UInt256.shiftRight
(EvmYul.UInt256.ofNat value) (EvmYul.UInt256.ofNat shift))) := by
rfl

-- ============================================================================
-- § 4. Backend profile invariant
-- ============================================================================

-- All backend profiles (semantic, solidity-parity-ordering, solidity-parity)
-- use the same evalBuiltinCall function. The profiles differ only in Yul
-- output shape (selector sorting, patch pass enablement), not arithmetic
-- semantics. This is enforced structurally: there is a single evalBuiltinCall
-- definition that all codepaths use.

/-- The BuiltinBackend enum has exactly two variants. -/
example : ∀ b : Compiler.Proofs.YulGeneration.BuiltinBackend,
b = .verity ∨ b = .evmYulLean := by
intro b; cases b <;> simp
-- Public arithmetic facts in this module are stated directly against
-- `evalPureBuiltinViaEvmYulLean`; legacy backend comparison lemmas remain in
-- the transition bridge modules, not as this profile's semantic authority.

-- ============================================================================
-- § 5. Scope boundaries (what is NOT proved here)
Expand All @@ -183,9 +166,8 @@ example : ∀ b : Compiler.Proofs.YulGeneration.BuiltinBackend,
-- Cryptographic primitives: keccak256 is axiomatized (see AXIOMS.md).
-- The mapping-slot derivation trusts the keccak FFI.
--
-- Universal bridge equivalence: all pure arithmetic/comparison builtins plus
-- bitwise and/or/xor and the shift family now have direct symbolic bridge lemmas
-- in `Backends/EvmYulLeanBridgeLemmas.lean`.
-- `not` still relies on concrete bridge coverage.
-- Legacy/native bridge equivalence: comparison lemmas are part of the
-- transition bridge modules. This profile intentionally exposes only native
-- evaluator facts.

end Compiler.Proofs.ArithmeticProfile
Loading
Loading