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

@@ -198,58 +198,6 @@ pub open spec fn va_range_get_tree_path(va: Range<Vaddr>) -> Seq<NodeId>
     NodeHelper::trace_to_tree_path(trace)
 }
 
-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_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);
-        };
-    }
-}
-
-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_range_get_tree_path(va: Range<Vaddr>)
     requires
         va_range_wf(va),