Vector ext borrow or unknown#585

Merged

andreistefanescu merged 12 commits intomainfrom

vector-ext-borrow-or-unknown

Apr 16, 2026

Commits on Apr 14, 2026

feat: add prover::vector_ext module with borrow_or_unknown

andreistefanescu
and
claude
committed

Commits on Apr 15, 2026

feat: add ext modules for Sui container types (scaffolding + vec_map/vec_set)

andreistefanescu
and
claude
committed
feat: implement borrow_or_unknown for table/object_table/dynamic_{object_}field

andreistefanescu
and
claude
committed
feat: add vec_map_ext::entry_at_or_unknown

andreistefanescu
and
claude
committed
refactor: enforce foo -> foo_or_unknown naming convention

andreistefanescu
and
claude
committed
refactor: move concat from prover::vector_iter to prover::vector_ext

andreistefanescu
and
claude
committed
feat: tier 1 + tier 2 ext functions (get_idx_or_unknown + insert/remove pure variants)

andreistefanescu
and
claude
committed
feat: rename concat -> append_pure; add 6 vector pure variants; new InsertAtVec

andreistefanescu
and
claude
committed
Merge branch 'main' into vector-ext-borrow-or-unknown
andreistefanescu
authored
refactor: ext native helpers as Boogie functions, not procedures

andreistefanescu
and
claude
committed
perf: convert recursive quantifier-helper axioms to compound triggers

andreistefanescu
and
claude
committed

Commits on Apr 16, 2026

refactor: move ext functions from prover to native Sui modules

andreistefanescu
and
claude
committed