Core models option#2
Draft
maximebuyse wants to merge 41 commits into
Draft
Conversation
fix: `do` elab regressions
Fix syntax issues leading to tokens being reserved
Fix an issue in `Decompose.hasNoncomputableDep`
Add support for multi-target extraction
* Mark {UScalarTy,IScalarTy}.numBits as implicit_reducible
* Tweak and add some simp lemmas about scalars
* add unused var regressions * fix * address review comments * fix merge errors
…sVerif#894) * Add wrapping shift definitions and fix OWrap shift extraction Define UScalar/IScalar wrapping_shl and wrapping_shr in the Lean backend, and route OWrap shifts through the wrapping extraction path in Extract.ml so they emit valid Lean names. Fixes AeneasVerif#816. * Address review: add rust_fun bindings and tests for wrapping shifts - Bind core::num::{TYPE}::wrapping_shl|shr → core.num.LeanType.wrapping_shl|shr via attribute [rust_fun ...] on each per-type definition. - Add scalars.rs tests covering both the method-call form and the OWrap binop form (IndexMut shift, per Charon AeneasVerif#1041). * Regenerate ExtractBuiltinLean.ml * Fix wrapping_shl/shr signature and regenerate Scalars.lean - Take U32 (not Nat) as the shift count, matching Rust's wrapping_{shl,shr}(self, rhs: u32) signature and the U32 that aeneas emits at call sites. - Add -canFail to the rust_fun attributes so aeneas wraps calls in `ok`, since these operations are total. - Regenerate ExtractBuiltinLean.ml and tests/lean/Scalars.lean. * Update backends/lean/Aeneas/Std/Scalar/WrappingOps/Shl.lean * Update backends/lean/Aeneas/Std/Scalar/WrappingOps/Shl.lean * Update backends/lean/Aeneas/Std/Scalar/WrappingOps/Shr.lean * Update backends/lean/Aeneas/Std/Scalar/WrappingOps/Shr.lean * Run make format on ExtractBuiltinLean.ml Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv> --------- Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv> Co-authored-by: Son HO <son.marc.ho@hotmail.com>
maximebuyse
force-pushed
the
core-models-option
branch
from
c34ab33 to
90d17d5
Compare
abentkamp
force-pushed
the
core-models-option
branch
from
97df742 to
210ed8c
Compare
Do not mark trait instances as `reducible` and add missing lemmas
* Add namespaces in the #decompose tests * Fix an issue and add a test
karthikbhargavan
added a commit
that referenced
this pull request
May 19, 2026
CertObserver registers with the [Observer.current] slot from commit #1 when [-emit-cert] is set. Its [event_to_cert] dispatch is empty — commits 3-9 grow it one Event variant at a time. Until then, no inline emit site calls [Observer.notify], so cert output stays byte-equal (the existing [ctx_emit_event] -> [eval_ctx.cert_event_buffer] path is untouched). * src/cert/CertObserver.{ml,mli} — install / event_to_cert / on_event. on_event respects ctx.cert_events_suppressed so the migration in commit AeneasVerif#6 (which moves the InterpLoops suppression call to Observer.with_suppressed) can swap atomically without intermediate drift. * src/Main.ml — call Aeneas.CertObserver.install () before CertGen.emit under -emit-cert. * src/dune — wire CertObserver, Event, Observer into the library's explicit (modules ...) list. (Event/Observer landed in commit #1 but had no consumer, so dune silently dropped them; CertObserver surfaces the dependency.) Gates: G_cert 89/89, G_build clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
maximebuyse
force-pushed
the
core-models-option
branch
from
210ed8c to
01a4ba3
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.