Merged
Conversation
Introduces a small new Move module, prover::vector_ext, as the first of what can become a family of "extension" modules adding spec-only helpers over types we don't own. borrow_or_unknown(v, i): &T is a total borrow — for in-range indices it returns v[i]; for out-of-range indices it returns an uninterpreted but deterministic value. Unlike vector::borrow, it never aborts, so it can be used freely in spec expressions without a guard. The Boogie model is trivially ReadVec(v, i): the underlying vector theory already returns an unspecified value for out-of-bounds reads. Method syntax (v.borrow_or_unknown(i)) is available via a local `use fun` alias at the caller, since Move forbids `public use fun` for types defined outside the declaring module. Tests (under tests/inputs/vector_ext/): - borrow_or_unknown.ok: in-range matches vector::borrow, method syntax works, concrete reads. - borrow_or_unknown.fail: out-of-range value is not pinnable to a specific constant — correctly fails to verify. A snapshot in multiple_specs/include_external.fail shifted by 10 lines because the prelude grew; updated. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…vec_set) Scaffolds six spec-only extension modules in the prover package for the Sui framework container types we don't own: prover::vec_map_ext prover::vec_set_ext prover::table_ext prover::object_table_ext prover::dynamic_field_ext prover::dynamic_object_field_ext Each is intended as a home for "total" variants of container operations — lookups that never abort, returning an uninterpreted value for missing keys / out-of-range indices. To host Sui types, added Sui as a dependency of the prover package. Implemented in this commit (Boogie axiomatization + tests): vec_map_ext::get_or_unknown<K, V>(m, k): &V vec_set_ext::at_or_unknown<K>(s, i): &K Both are added inside the existing vec_map/vec_set macros in native.bpl. Semantics: in-domain lookups match the underlying operation; out-of-domain lookups reduce to ReadVec at an invalid index, which the vector theory leaves uninterpreted — callers cannot pin the result to any specific value. The other four modules (table/object_table, dynamic_field/object_field) are only scaffolded — the native fns are declared but Boogie modeling requires adding per-impl fun_borrow_or_unknown fields to the Rust TableImpl / DynamicFieldInfo structs. Deferred to a follow-up. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ect_}field
Completes the scaffolding from the previous commit by wiring up Rust-side
plumbing + Boogie axiomatization for the four Sui-intrinsic container
types that use the impl-based macro dispatch pattern.
Rust changes:
- model.rs: new module-name and function-name constants for the four
ext modules; new qid accessors (table_ext_borrow_or_unknown_qid,
object_table_ext_borrow_or_unknown_qid, etc.); registered in the
native_fn_ids list.
- lib.rs: added fun_borrow_or_unknown: String fields to TableImpl and
DynamicFieldInfo; populated them in the four constructors.
- dynamic_field_analysis.rs: added the two df/dof ext qids to the
name_value list of DfQids. This makes the DynamicFieldAnalysisProcessor
push the parent object type onto the call's type_inst, so the Boogie
name mangling matches the per-parent-struct procedures emitted by the
dynamic_field_module macro.
Boogie (native.bpl):
- table_module: emits {{impl.fun_borrow_or_unknown}}{{S}} as a procedure
+ $pure function; both reduce to GetTable, letting the table theory
return an uninterpreted value for missing keys.
- dynamic_field_module: same pattern, with GetTable over
t->$dynamic_fields{{S}} + the IsValid assumption to match the behavior
of fun_borrow on the value path.
All four tests verify successfully:
- table_ext::borrow_or_unknown (ok + fail)
- object_table_ext::borrow_or_unknown (ok)
- dynamic_field_ext::borrow_or_unknown (ok + fail)
- dynamic_object_field_ext::borrow_or_unknown (ok)
420 tests pass.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Total indexed entry accessor, the (&K, &V)-returning counterpart to vec_map::get_entry_by_idx. For in-range indices this is ReadVec-backed; for out-of-range indices the pair is uninterpreted — no abort. Boogie procedure returns both fields of the Entry struct: entry := ReadVec(vm->$contents, idx); res0 := entry->$key; res1 := entry->$value; Mirrors vec_set_ext::at_or_unknown; fills the "indexed-access total" slot for VecMap that was previously absent. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Rename vec_map_ext::entry_at_or_unknown -> vec_map_ext::get_entry_by_idx_or_unknown, matching the source Sui API `vec_map::get_entry_by_idx`. - Empty vec_set_ext (was: at_or_unknown). VecSet has no indexed accessor in the Sui framework to build `_or_unknown` from; kept the module as a placeholder so the convention holds uniformly for any future additions. Boogie modeling and tests for at_or_unknown removed. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
concat is a non-iterator vector utility — belongs in the general-purpose
vector extension module rather than the iterator helper module. No
semantic change.
- Move the native declaration from vector.move to vector_ext.move.
- Add PROVER_VECTOR_EXT_MODULE_NAME constant; retarget prover_vec_concat_qid
to the new module.
- Rename Boogie function $0_vector_iter_concat{S} -> $0_vector_ext_concat{S}.
- Split `use prover::vector_iter::{..., concat}` into two imports across
the 5 tests that use concat.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ve pure variants)
Tier 1:
- vec_map_ext::get_idx_or_unknown — total index lookup.
Tier 2 (functional variants of mutating ops):
- vec_map_ext::insert_pure, remove_pure
- vec_set_ext::insert_pure, remove_pure
- table_ext::add_pure, remove_pure
- object_table_ext::add_pure, remove_pure
Rust plumbing for table/object_table (impl-based dispatch):
- New function name constants ADD_PURE_FUNCTION_NAME, REMOVE_PURE_FUNCTION_NAME.
- New qid accessors; registered in native_fn_ids list.
- TableImpl gains fun_add_pure, fun_remove_pure fields; populated in
table and object_table constructors.
Boogie axiomatization:
- vec_map_ext / vec_set_ext: self-contained, use ExtendVec / RemoveAtVec.
- table_ext / object_table_ext: use AddTable / RemoveTable, via
{{impl.fun_add_pure}} / {{impl.fun_remove_pure}}.
remove_pure variants return the container unchanged if the key isn't
present — never aborts.
Tests assert reference equality between the mutable result and the
functional model's result (references are copy even when the container
isn't).
All 429 tests pass.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…nsertAtVec
vector_ext renames + new functions:
- concat -> append_pure (matches std::vector::append; updates 5 test files
that imported concat)
- push_back_pure, pop_back_pure, push_front_pure, pop_front_pure,
insert_pure, remove_pure — functional variants of std::vector ops
(push_front/pop_front have no std counterpart)
Boogie:
- New InsertAtVec<T>(v, i, e) primitive in all three vector theories
(vector-array, vector-array-intern, vector-smt-seq), parallel to
RemoveAtVec.
- vector_ext pure helpers use InsertAtVec / RemoveAtVec / InRangeVec
consistently.
- Fixed swapped argument order in $1_vector_insert{S}: Move signature
is insert(v, e, i) but the Boogie procedure had (m, i, e) — corrected
to (m, e, i). Was unused by any prior test, surfaced now by
vector_ext::insert_pure's test_insert_matches.
Tests: 7 *_pure tests for vector_ext, all verifying the functional
helpers match the corresponding mutating ops via reference equality.
All 436 tests pass.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
All single-return _or_unknown / _pure helpers in vector_ext, vec_set_ext, vec_map_ext, table_ext, object_table_ext, dynamic_field_ext, and dynamic_object_field_ext are now plain Boogie functions (no separate procedure + $pure pair). The only exception is vec_map_ext::get_entry_by_idx_or_unknown, which stays a procedure because Boogie functions can't return tuples. To make the function-style call site work from procedural Boogie, the new ext qids are registered in native_fn_ids() (drives should_be_used_as_func), deterministic_native_functions(), and no_aborting_native_functions(). The previously-defined table_ext / object_table_ext / dynamic_field_ext / dynamic_object_field_ext qids were also missing from native_fn_ids() and are added now. Also drops a redundant push_front_pure length-arithmetic test. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The recursive defn axioms for count, sum_map, find_index, range_count, and
range_sum_map were single-pattern (`{$Helper(v, start, end)}`) with the
recursive sub-term in the body. That's a textbook matching cascade: every
fired instance creates a new sub-range Helper term that immediately
re-matches the trigger.
Converted to compound multi-pattern triggers
(`{$Helper(v, start, end), $Helper(v, next_start, end)}` and the symmetric
end-step), matching the shape filter / find_indices / map already use.
Concrete impact on `count_loop`:
- quant-instantiations: 101,252 -> 70 (1,400x)
- max-generation: 11 -> 3
- SMT solve time: 6.56s -> <0.01s
Trade-off: concrete-vector tests (e.g. `count!(&[10,20,10,30], pred) == 2`)
no longer unfold automatically, so they need single-trigger end-step
helper axioms supplied via `extra_bpl` — same pattern filter has used all
along. Added per-test `.bpl` helpers for count.ok, count_big.ok,
nested_pure.ok, nested_pure_params.ok, nested_helpers.ok,
range_count.ok, range_count_pure.ok, range_sum_map.ok.
Also added range_sum_map_pure.ok.move (mirrors range_count_pure.ok.move,
which previously had no sum_map analogue).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The #[spec_only] native helpers (borrow_or_unknown, *_pure variants) previously lived in separate prover::*_ext modules. With the matching commit in asymptotic-code/sui@315873449 ("feat: move spec-only ext helpers into their natural home modules"), they now live in the canonical modules: std::vector, sui::vec_map, sui::vec_set, sui::table, sui::object_table, sui::dynamic_field, sui::dynamic_object_field. Changes: - Deleted all 7 packages/prover/sources/*_ext.move files. - Renamed Boogie prelude qids: $0_vector_ext_* → $1_vector_*, $0_vec_map_ext_* → $2_vec_map_*, $0_vec_set_ext_* → $2_vec_set_*. Table / dynamic_field qids auto-update via Tera template variables. - Removed obsolete _EXT module-name constants from model.rs; qid accessors now reference the non-ext module names. - Updated 33 test files: imports switch from prover::*_ext to std::vector / sui::vec_map / etc. - Removed 2 explicit `use fun` aliases that now conflict with Move's auto-generated method aliases. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
1 participant
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.