Skip to content

Extensions #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maximebuyse wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Extensions #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
17082ff
Extensions.
maximebuyse Jun 4, 2026
db1718c
Enforce no error from Aeneas extraction.
maximebuyse Jun 4, 2026
441a998
Extensions.
maximebuyse Jun 4, 2026
dab1160
Extensions cleanup.
maximebuyse Jun 4, 2026
47e6cd8
Tests for extensions.
maximebuyse Jun 4, 2026
0dd2fb8
Update aeneas commit.
maximebuyse Jun 4, 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
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ on:
env:
RUST_TOOLCHAIN: nightly-2026-02-07
CHARON_REV: a535e914f74db4fd9e6be7048f4233270d8945c0
AENEAS_REV: 8d2077ce4946b52d2d199fe9d2f2d520a4bf8184
AENEAS_REV: 157c25e0010dd4a010813fa5094cd0055ac055b1
# Where the cache step stages the charon / aeneas binaries.
AENEAS_DIR: ${{ github.workspace }}/.tools/aeneas

Expand Down
19 changes: 8 additions & 11 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,11 @@ ALLOC_CHARON_EXCLUDES = \
--exclude '{impl alloc_models::collections::binary_heap::BinaryHeap<_, _>}::*' \
--exclude 'alloc_models::string::*' \
--exclude '{impl alloc_models::string::String}::*' \
--exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_, _>}' \
--exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_, _>}::*' \
--exclude 'alloc_models::slice::_::sort_by' \
--exclude '{impl core::ops::index::Index<_> for alloc_models::vec::Vec<_, _>}' \
--exclude '{impl core::ops::index::Index<_> for alloc_models::vec::Vec<_, _>}::*'
--exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_>}' \
--exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_>}::*' \
--exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::collections::vec_deque::VecDeque<_, _>}' \
--exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::collections::vec_deque::VecDeque<_, _>}::*' \
--exclude 'alloc_models::slice::_::sort_by'

.PHONY: all llbc extract patch lean build clean clean-generated tests \
tests-clean alloc-stage alloc-llbc alloc-extract alloc-clean
Expand All @@ -66,8 +66,7 @@ CHARON_EXCLUDES = \
--exclude 'core_models::option::_::is_some' \
--exclude 'core_models::option::_::is_none' \
--exclude 'core_models::option::_::unwrap_or' \
--exclude 'core_models::option::_::take' \
--exclude 'core_models::slice::index::*'
--exclude 'core_models::option::_::take'

llbc: $(LLBC_FILE)

Expand All @@ -82,9 +81,7 @@ $(LLBC_FILE): $(CORE_MODELS_DIR)/src/**/*.rs $(CORE_MODELS_DIR)/Cargo.toml
# $(LEAN_DIR)/Aeneas/ is left untouched.
extract: $(LLBC_FILE) alloc-extract
mkdir -p $(LEAN_DIR)
# Aeneas may exit non-zero while still producing partial files; that's OK,
# our patcher and the surrounding hand-written library handle the gaps.
-$(AENEAS) -core-models-lib -backend lean $(LLBC_FILE) -split-files -dest $(LEAN_DIR) \
$(AENEAS) -core-models-lib -backend lean $(LLBC_FILE) -split-files -dest $(LEAN_DIR) \
-subdir CoreModels/Core -all-computable

# -----------------------------------------------------------------------------
Expand Down Expand Up @@ -119,7 +116,7 @@ alloc-llbc: $(ALLOC_LLBC_FILE)
# `-subdir CoreModels/Alloc` makes Aeneas emit `import CoreModels.Alloc.<X>` rather
# than the auto-derived `Alloc_models.<X>` prefix.
alloc-extract: $(ALLOC_LLBC_FILE)
-$(AENEAS) -core-models-lib -backend lean $(ALLOC_LLBC_FILE) -split-files \
$(AENEAS) -core-models-lib -backend lean $(ALLOC_LLBC_FILE) -split-files \
-dest $(LEAN_DIR) -subdir CoreModels/Alloc -all-computable

# 3. Move generated files into $(LEAN_DIR)/CoreModels/ and apply our patches
Expand Down
Loading