Start fixing assume false's

Author: tchajed

Makefile

@@ -44,7 +44,7 @@ src/nonlin/%.dfy.ok: DAFNY_ARGS = /arith:1
 # up unused imports emitted by Dafny.
 dafnygen/dafnygen.go: src/compile.dfy $(DFY_FILES)
 	@echo "DAFNY COMPILE $<"
-	$(Q)$(DAFNY) /countVerificationErrors:0 /spillTargetCode:2 /out dafnygen $<
+	$(Q)$(DAFNY) /noVerify /spillTargetCode:2 /out dafnygen $<
 	$(Q)rm -rf dafnygen
 	$(Q)cd dafnygen-go/src && ../../etc/dafnygen-imports.py ../../dafnygen
 	$(Q)rm -r dafnygen-go

src/fs/indirect/pos.dfy

@@ -301,7 +301,13 @@ module IndirectPos
         assert 8 <= from_flat(n0).k < 8+3;
         if n < 512 {
           assert from_flat(n0).k == 8;
-          assert from_flat(n0).flat() == n0 by { assume false; }
+          assert from_flat(n0).off.ilevel == 1;
+          assert from_flat(n0).off.j == n % 512;
+          // this lemma is actually required to prove this equality (it's hard
+          // to get Dafny to compute this recursive function)
+          config_totals_after_8(8);
+          assert config.total_to(8) == 8;
+          assert from_flat(n0).flat() == n0;
           return;
         }
         if n < 2*512 {

src/fs/indirect_fs.dfy

@@ -690,7 +690,10 @@ module IndFs
       ok, bn := allocateIndirectMetadata(txn, pos, ibn, pblock);
       c.ok := false;
       c.bs := NewBytes(0);
-      assert ValidIno(pos.ino, i) by { assume false; }
+      assert ValidIno(pos.ino, i) by {
+        assume false; // otherwise times out
+        assert i.Valid() && fs.is_cur_inode(pos.ino, i.val());
+      }
       if !ok {
         IndBlocks.to_blknos_zero();
         reveal ValidIndirect();

src/fs/inode_fs.dfy

@@ -478,15 +478,24 @@ module InodeFs {
       }
       assert Valid() by {
         reveal Valid_jrnl_super_block();
-        reveal Valid_jrnl_to_data_block();
         reveal Valid_jrnl_to_block_used();
         assert && Valid_basics(jrnl)
                && Valid_domains()
                && Valid_jrnl_super_block(ballocActualMax)
                && Valid_jrnl_to_block_used(block_used)
                && Valid_jrnl_to_inodes(inodes)
                && Valid_balloc();
-        assert && Valid_jrnl_to_data_block(data_block) by { assume false; }
+        assert Valid_jrnl_to_data_block(data_block) by {
+          reveal Valid_jrnl_to_data_block();
+        forall bn | blkno_ok(bn) && bn != 0
+            ensures (
+              datablk_inbounds(jrnl, bn);
+              jrnl.data[DataBlk(bn)] == ObjData(data_block[bn])) {
+                datablk_inbounds(jrnl, bn);
+                assert jrnl.data[DataBlk(bn)] == old(jrnl.data[DataBlk(bn)]);
+          }
+          assert Valid_jrnl_to_data_block(data_block);
+        }
       }
     }
 

src/fs/typed_fs.dfy

@@ -549,15 +549,16 @@ module TypedFs {
         eof := true;
         return;
       }
-      assume false;
       var readLen: uint64 := len;
       if off + len >= i.sz {
         readLen := i.sz - off;
         eof := true;
       } else {
         eof := false;
       }
+      reveal_valids();
       bs, ok := fs.readWithInode(txn, ino, i, off, readLen);
+      reveal_valids();
       reveal ValidFields();
     }