Try to fix broken proof

mit-pdos · Oct 16, 2024 · 68530c3 · 68530c3
1 parent 5be664f
commit 68530c3
Showing 1 changed file with 22 additions and 0 deletions.
diff --git a/src/util/marshal.i.dfy b/src/util/marshal.i.dfy
@@ -158,11 +158,33 @@ module Marshal
     if es == [] { return; }
     decode_encode_uint64(es[0]);
     decode_encode_uint64_seq_id(es[1..]);
+    assert es == [es[0]] + es[1..];
+    enc_uint64_len(es);
     enc_uint64_len(es[1..]);
+    assert |seq_enc_uint64(es)| == 8*|es|;
     assert seq_fmap(encUInt64, es[1..]) == seq_fmap(encUInt64, es)[1..];
     assert seq_encode(seq_fmap(encUInt64, es[1..])) == seq_encode(seq_fmap(encUInt64, es))[8..];
   }
 
+  /*
+  lemma decode_encode_uint64_seq_id(es: seq<uint64>)
+    ensures |seq_enc_uint64(es)| == 8*|es|
+    ensures decode_uint64_seq(seq_encode(seq_fmap(encUInt64, es))) == es
+  {
+    enc_uint64_len(es);
+    assert |seq_enc_uint64(es)| == 8*|es|;
+    if es == [] { return; }
+    decode_encode_uint64(es[0]);
+    decode_encode_uint64_seq_id(es[1..]);
+    enc_uint64_len(es[1..]);
+    assert seq_fmap(encUInt64, es[1..]) == seq_fmap(encUInt64, es)[1..];
+    assert seq_encode(seq_fmap(encUInt64, es[1..])) == seq_encode(seq_fmap(encUInt64, es))[8..];
+    assert es == [es[0]] + es[1..];
+    assert seq_encode(seq_fmap(encUInt64, es)) == enc_encode(encUInt64(es[0])) + seq_encode(seq_fmap(encUInt64, es[1..]));
+    assert decode_uint64(seq_encode(seq_fmap(encUInt64, es))[..8]) == es[0];
+  }
+  */
+
   ghost function decode_uint64_seq_one(bs: seq<byte>, k: nat): uint64
     requires |bs| % 8 == 0
     requires k*8 < |bs|