Make a byte_fs proof more robust

mit-pdos · Jan 12, 2024 · 6f0c12a · 6f0c12a
1 parent 07dd2f5
commit 6f0c12a
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/src/fs/byte_fs.dfy b/src/fs/byte_fs.dfy
@@ -267,10 +267,16 @@ module ByteFs {
 
       bs.AppendBytes(bs2);
       assert (off + len) as nat == bs2_upper_bound;
+      assert off + len <= i.sz;
+      assert (off + len) as nat <= i.sz as nat;
       calc {
         bs.data;
         raw_data(ino)[off..off''] + raw_data(ino)[off''..bs2_upper_bound];
-        raw_data(ino)[off..off + len];
+        raw_data(ino)[off..(off + len) as nat];
+        raw_inode_data(block_data(fs.data)[ino])[off..off + len];
+        raw_inode_data(block_data(fs.data)[ino])[..i.sz][off..off + len];
+        inode_data(i.sz as nat, block_data(fs.data)[ino])[off..bs2_upper_bound];
+        this.data()[ino][off..bs2_upper_bound];
       }
     }