Prove admit() related to va level (#70)

* Prove `lemma_va_range_get_guard_level`

* Prove `lemma_va_range_get_tree_path`

* Prove `lemma_is_child_level_relation`

* Prove `lemma_va_level_to_nid_inc`

Author: Marsman1996

lock-protocol/src/exec/rw/common.rs

@@ -135,7 +135,123 @@ pub proof fn lemma_va_level_to_nid_inc(va: Vaddr, level: PagingLevel, nid: NodeI
     ensures
         NodeHelper::get_child(nid, idx) == va_level_to_nid(va, level),
 {
-    admit();  // TODO
+    // Establish the relationship between traces at consecutive levels
+    let trace_level_plus_1 = va_level_to_trace(va, (level + 1) as PagingLevel);
+    let trace_level = va_level_to_trace(va, level);
+
+    // Show that trace_level = trace_level_plus_1.push(idx)
+    assert(trace_level == trace_level_plus_1.push(idx)) by {
+        // By definition: va_level_to_trace(va, level) = va_level_to_trace_rec(va >> 12, level)
+        // And: va_level_to_trace_rec(va >> 12, level) = va_level_to_trace_rec(va >> 12, level + 1).push(((va >> 12 >> (level * 9)) & mask) as nat)
+        // We need to show that ((va >> 12 >> (level * 9)) & mask) as nat == idx
+        // Since idx = va_level_to_offset(va, level + 1) = ((va >> (12 + level * 9)) & mask) as nat
+        // And (va >> 12 >> (level * 9)) = (va >> (12 + level * 9)) by bit shift properties
+        // reveal(va_level_to_trace_rec);
+        assert(va_level_to_trace_rec(va >> 12, level) == va_level_to_trace_rec(
+            va >> 12,
+            (level + 1) as PagingLevel,
+        ).push(((va >> 12 >> (level * 9)) & low_bits_mask(9) as usize) as nat));
+
+        // Show the bit extraction equivalence
+        let offset = (va >> 12 >> (level * 9)) & low_bits_mask(9) as usize;
+        assert(offset as nat == idx) by {
+            // va_level_to_offset(va, level + 1) = ((va >> (12 + ((level + 1) - 1) * 9)) & mask) as nat
+            //                                   = ((va >> (12 + level * 9)) & mask) as nat
+            // We need to show: (va >> 12 >> (level * 9)) & mask == (va >> (12 + level * 9)) & mask
+            // This follows from bit shift associativity: a >> b >> c == a >> (b + c)
+            assert(low_bits_mask(9) == 511) by {
+                lemma_low_bits_mask_values();
+            };
+            assert((va >> 12 >> (level * 9)) == (va >> (12 + level * 9))) by (bit_vector);
+            assert(((va >> 12 >> (level * 9)) & 511 as usize) == ((va >> (12 + level * 9))
+                & 511 as usize)) by (bit_vector);
+        }
+    };
+
+    // Now use the fact that nid = trace_to_nid(trace_level_plus_1)
+    // and get_child(nid, idx) = trace_to_nid(nid_to_trace(nid).push(idx))
+    assert(NodeHelper::nid_to_trace(nid) == trace_level_plus_1) by {
+        // First establish that trace_level_plus_1 is a valid trace
+        assert(NodeHelper::valid_trace(trace_level_plus_1)) by {
+            // trace_level_plus_1 = va_level_to_trace(va, level + 1)
+            // Use the lemma that directly proves va_level_to_trace produces valid traces
+            lemma_va_level_to_trace_valid(va, (level + 1) as PagingLevel);
+        };
+
+        // Since nid = trace_to_nid(trace_level_plus_1) and trace_to_nid is bijective
+        NodeHelper::lemma_nid_to_trace_sound(nid);
+        NodeHelper::lemma_trace_to_nid_sound(trace_level_plus_1);
+        // From the precondition: nid == va_level_to_nid(va, level + 1)
+        // And va_level_to_nid(va, level + 1) == trace_to_nid(trace_level_plus_1)
+        // So nid == trace_to_nid(trace_level_plus_1)
+        // Since trace_to_nid is bijective, nid_to_trace(nid) == trace_level_plus_1
+        assert(nid == NodeHelper::trace_to_nid(trace_level_plus_1));
+        assert(NodeHelper::trace_to_nid(NodeHelper::nid_to_trace(nid)) == nid);
+        assert(NodeHelper::trace_to_nid(NodeHelper::nid_to_trace(nid)) == NodeHelper::trace_to_nid(
+            trace_level_plus_1,
+        ));
+        NodeHelper::lemma_trace_to_nid_bijective();
+    };
+
+    // Therefore get_child(nid, idx) = trace_to_nid(trace_level_plus_1.push(idx)) = trace_to_nid(trace_level)
+    assert(NodeHelper::get_child(nid, idx) == NodeHelper::trace_to_nid(
+        trace_level_plus_1.push(idx),
+    ));
+    assert(trace_level_plus_1.push(idx) == trace_level);
+    assert(NodeHelper::get_child(nid, idx) == NodeHelper::trace_to_nid(trace_level));
+    assert(NodeHelper::trace_to_nid(trace_level) == va_level_to_nid(va, level));
+}
+
+pub proof fn lemma_va_level_to_trace_rec_len(va: Vaddr, level: PagingLevel)
+    requires
+        1 <= level <= 4,
+    ensures
+        va_level_to_trace_rec(va, level).len() == 4 - level,
+    decreases 4 - level,
+{
+    if level < 4 {
+        lemma_va_level_to_trace_rec_len(va, (level + 1) as PagingLevel);
+    }
+}
+
+pub proof fn lemma_va_level_to_trace_valid(va: Vaddr, level: PagingLevel)
+    requires
+        1 <= level <= 4,
+    ensures
+        NodeHelper::valid_trace(va_level_to_trace(va, level)),
+{
+    lemma_va_level_to_trace_rec_valid(va >> 12, level);
+}
+
+pub proof fn lemma_va_level_to_trace_rec_valid(va: Vaddr, level: PagingLevel)
+    requires
+        1 <= level <= 4,
+    ensures
+        NodeHelper::valid_trace(va_level_to_trace_rec(va, level)),
+    decreases 4 - level,
+{
+    if level < 4 {
+        lemma_va_level_to_trace_rec_valid(va, (level + 1) as PagingLevel);
+        let offset = (va >> (level * 9)) & low_bits_mask(9) as usize;
+        assert(offset < 512) by {
+            assert(low_bits_mask(9) == 511) by {
+                lemma_low_bits_mask_values();
+            };
+            assert((va >> (level * 9)) & 511 <= 511) by (bit_vector);
+        }
+        // By inductive hypothesis, the recursive trace is valid
+        assert(NodeHelper::valid_trace(va_level_to_trace_rec(va, (level + 1) as PagingLevel)));
+        // Therefore its length is < 4
+        assert(va_level_to_trace_rec(va, (level + 1) as PagingLevel).len() < 4);
+        // Since we add exactly one element, the new length is still < 4
+        assert(va_level_to_trace_rec(va, level).len() == va_level_to_trace_rec(
+            va,
+            (level + 1) as PagingLevel,
+        ).len() + 1);
+        assert(va_level_to_trace_rec(va, (level + 1) as PagingLevel).len() + 1 <= 3) by {
+            lemma_va_level_to_trace_rec_len(va, (level + 1) as PagingLevel);
+        };
+    }
 }
 
 } // verus!

lock-protocol/src/exec/rw/cursor.rs

@@ -6,6 +6,7 @@ use builtin::*;
 use builtin_macros::*;
 use vstd::prelude::*;
 use vstd::atomic_with_ghost;
+use vstd::bits::*;
 use vstd::rwlock::{ReadHandle, WriteHandle};
 use vstd::vpanic;
 use vstd::pervasive::allow_panic;
@@ -162,13 +163,30 @@ pub open spec fn va_range_get_guard_level(va: Range<Vaddr>) -> PagingLevel
     va_range_get_guard_level_rec(va, 4)
 }
 
+pub proof fn lemma_va_range_get_guard_level_rec(va: Range<Vaddr>, level: PagingLevel)
+    requires
+        va_range_wf(va),
+        1 <= level <= 4,
+    ensures
+        1 <= va_range_get_guard_level_rec(va, level) <= level,
+    decreases level,
+{
+    if level > 1 {
+        let st = va.start;
+        let en = (va.end - 1) as usize;
+        if va_level_to_offset(st, level) == va_level_to_offset(en, level) {
+            lemma_va_range_get_guard_level_rec(va, (level - 1) as PagingLevel);
+        }
+    }
+}
+
 pub proof fn lemma_va_range_get_guard_level(va: Range<Vaddr>)
     requires
         va_range_wf(va),
     ensures
         1 <= va_range_get_guard_level(va) <= 4,
 {
-    admit();  // TODO
+    lemma_va_range_get_guard_level_rec(va, 4);
 }
 
 pub open spec fn va_range_get_tree_path(va: Range<Vaddr>) -> Seq<NodeId>
@@ -191,7 +209,26 @@ pub proof fn lemma_va_range_get_tree_path(va: Range<Vaddr>)
             ),
         va_range_get_tree_path(va).len() == 5 - va_range_get_guard_level(va),
 {
-    admit();  //TODO
+    let guard_level = va_range_get_guard_level(va);
+    let trace = va_level_to_trace(va.start, guard_level);
+    lemma_va_range_get_guard_level(va);
+    lemma_va_level_to_trace_rec_len(va.start >> 12, guard_level);
+    assert(trace.len() == 4 - guard_level);
+    let path = va_range_get_tree_path(va);
+    assert(path.len() == 1 + trace.len());
+    assert(path.len() == 5 - guard_level);
+    assert forall|i| 0 <= i < path.len() implies NodeHelper::valid_nid(path[i]) by {
+        let nid = path[i];
+        if i == 0 {
+            assert(nid == NodeHelper::root_id());
+            NodeHelper::lemma_root_id();
+        } else {
+            let sub_trace = trace.subrange(0, i);
+            assert(nid == NodeHelper::trace_to_nid(sub_trace));
+            lemma_va_level_to_trace_valid(va.start, guard_level);
+            NodeHelper::lemma_trace_to_nid_sound(sub_trace);
+        }
+    }
 }
 
 // pub proof fn lemma_va_range_get_tree_path_inc(

lock-protocol/src/spec/utils.rs

@@ -1653,7 +1653,9 @@ impl NodeHelper {
         ensures
             Self::nid_to_level(pa) == Self::nid_to_level(ch) + 1,
     {
-        admit();  // TODO
+        Self::lemma_is_child_implies_in_subtree(pa, ch);
+        Self::lemma_level_dep_relation(pa);
+        Self::lemma_level_dep_relation(ch);
     }
 }