prove: 12 `axiom` in page table and freshness - #531

Merged

rikosellic merged 13 commits into

asterinas:mainfrom

Marsman1996:fix-axiom

Jun 19, 2026

Commits on Jun 16, 2026

Commits on Jun 18, 2026

Merge remote-tracking branch 'origin/main' into fix-axiom
Marsman1996
committed
91abb15
refactor: move `lemma_finite_int_set_has_unused` into `vstd_extra`
Marsman1996
committed
d7f8669
Merge remote-tracking branch 'origin/main' into fix-axiom
Marsman1996
committed
1225d70
refactor: consolidate PageTableConfig proof lemmas into requirements/derived pattern
Marsman1996
committed
8a0a6e5
chore: `C::C` to `C`, except for spec code
Marsman1996
committed
89ad08b
simplify: ostd/specs/mm/page_table/vaddr_range_proofs.rs
Marsman1996
committed
d7b97e8
Merge remote-tracking branch 'origin/main' into fix-axiom
Marsman1996
committed
db21c08
chore: remove useless `as` convert
Marsman1996
committed
518c045

Commits on Jun 19, 2026

refactor(page_table): update paging constants and proofs
Marsman1996
committed
43521d9