Skip to content

Prove admit() related to va level - #70

Merged
rikosellic merged 4 commits into
asterinas:mainfrom
Marsman1996:va
Jul 10, 2025
Merged

Prove admit() related to va level#70
rikosellic merged 4 commits into
asterinas:mainfrom
Marsman1996:va

Conversation

@Marsman1996

@Marsman1996 Marsman1996 commented Jul 9, 2025

Copy link
Copy Markdown
Collaborator

Prove the

lemma_va_level_to_nid_inc 
lemma_is_child_level_relation 
lemma_va_range_get_guard_level 
lemma_va_range_get_tree_path

@rikosellic rikosellic added AI-assist AI-aided proof or generation pure proof Exec-unrelated proofs labels Jul 10, 2025
@rikosellic
rikosellic merged commit 4fcc240 into asterinas:main Jul 10, 2025
2 checks passed
@Marsman1996
Marsman1996 deleted the va branch August 1, 2025 10:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

AI-assist AI-aided proof or generation pure proof Exec-unrelated proofs

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Marsman1996 @rikosellic