Skip to content

Commit

Permalink
Update for Dafny 4.8 compatibility
Browse files Browse the repository at this point in the history
  • Loading branch information
@tchajed
tchajed committed Oct 16, 2024
1 parent 26f42d8 commit aa3cd3c
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 30 deletions.
6 changes: 3 additions & 3 deletions .github/workflows/main.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,8 @@ on:

# settings shared across all jobs
env:
dafny: "4.4.0"
go: "^1.21.0"
dafny: "4.8.1"
go: "^1.23.0"

jobs:
verify:
Expand All @@ -20,7 +20,7 @@ jobs:
steps:
- uses: actions/checkout@v4
- name: Install Dafny
uses: dafny-lang/setup-dafny-action@v1.7.0
uses: dafny-lang/setup-dafny-action@v1.8.0
with:
dafny-version: ${{ env.dafny }}
- name: Verify
Expand Down
6 changes: 4 additions & 2 deletions src/fs/byte_fs.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module ByteFs {
{}

class ByteFilesys
{
{
const fs: IndFilesys
ghost const Repr: set<object> := fs.Repr

Expand Down Expand Up @@ -276,13 +276,15 @@ module ByteFs {
assert off as nat + len as nat == bs2_upper_bound;
assert off + len <= i.sz;
assert (off + len) as nat <= i.sz as nat;
assert off' <= off + len;
calc {
bs.data;
raw_data(ino)[off..off''] + raw_data(ino)[off''..bs2_upper_bound];
raw_data(ino)[off..off''] + raw_data(ino)[off''..(off + len) as nat];
raw_data(ino)[off..(off + len) as nat];
raw_inode_data(block_data(fs.data)[ino])[off..(off + len) as nat];
{ seq_prefix_helper(raw_inode_data(block_data(fs.data)[ino]),
i.sz as nat, off as nat, (off + len) as nat); }
i.sz as nat, off as nat, (off + len) as nat); }
raw_inode_data(block_data(fs.data)[ino])[..i.sz][off..(off + len) as nat];
inode_data(i.sz as nat, block_data(fs.data)[ino])[off..bs2_upper_bound];
this.data()[ino][off..bs2_upper_bound];
Expand Down
24 changes: 12 additions & 12 deletions src/jrnl/jrnl.s.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
&& max % 8 == 0
}

constructor {:extern}(max: uint64)
constructor {:axiom} {:extern}(max: uint64)
requires 0 < max
requires max%8 == 0
ensures this.max == max
Expand All @@ -97,27 +97,27 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
}

// MarkUsed prevents an index from being allocated. Used during recovery.
method {:extern} MarkUsed(x: uint64)
method {:axiom} {:extern} MarkUsed(x: uint64)
requires Valid()
requires x < max
{
}

method {:extern} Alloc() returns (x:uint64)
method {:axiom} {:extern} Alloc() returns (x:uint64)
requires Valid()
ensures x < max
{
x := 1;
}

method {:extern} Free(x: uint64)
method {:axiom} {:extern} Free(x: uint64)
requires Valid()
requires x != 0
requires x < max
{
}

method {:extern} NumFree() returns (num: uint64)
method {:axiom} {:extern} NumFree() returns (num: uint64)
requires Valid()
ensures num <= max
{
Expand All @@ -126,7 +126,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec

}

method {:extern} NewAllocator(max: uint64) returns (a:Allocator)
method {:axiom} {:extern} NewAllocator(max: uint64) returns (a:Allocator)
requires 0 < max
requires max%8 == 0
ensures a.max == max
Expand Down Expand Up @@ -257,7 +257,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
&& jrnl.Valid()
}

method {:extern} Read(a: Addr, sz: uint64)
method {:axiom} {:extern} Read(a: Addr, sz: uint64)
returns (buf:Bytes)
requires Valid() ensures Valid()
requires a in jrnl.data && jrnl.size(a) == sz as nat
Expand All @@ -277,7 +277,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
// return new Bytes(jrnl.data[a].bs);
// }

method {:extern} ReadBit(a: Addr)
method {:axiom} {:extern} ReadBit(a: Addr)
returns (b:bool)
requires Valid() ensures Valid()
requires a in jrnl.data && jrnl.size(a) == 1
Expand All @@ -287,7 +287,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
// return jrnl.data[a].b;
// }

method {:extern} Write(a: Addr, bs: Bytes)
method {:axiom} {:extern} Write(a: Addr, bs: Bytes)
modifies jrnl, bs
requires Valid() ensures Valid()
ensures bs.data == []
Expand All @@ -301,7 +301,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
// bs.data := [];
// }

method {:extern} WriteBit(a: Addr, b: bool)
method {:axiom} {:extern} WriteBit(a: Addr, b: bool)
modifies jrnl
requires Valid() ensures Valid()
requires a in jrnl.data && jrnl.size(a) == 1
Expand All @@ -313,7 +313,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec

// wait=false is not modeled; it is up to the code to use this only when
// deferred durability is acceptable
method {:extern} Commit(wait: bool) returns (ok:bool)
method {:axiom} {:extern} Commit(wait: bool) returns (ok:bool)
requires wait
requires Valid() ensures Valid()
// {
Expand All @@ -338,7 +338,7 @@ module {:extern "jrnl", "github.com/mit-pdos/daisy-nfsd/dafny_go/jrnl"} JrnlSpec
// The best we can do is manually check that NewJrnl has about the same spec
// as the constructor, except for adding fresh(jrnl) which is implied by the
// constructor.
method {:extern} NewJrnl(d: Disk, ghost kinds: map<Blkno, Kind>)
method {:axiom} {:extern} NewJrnl(d: Disk, ghost kinds: map<Blkno, Kind>)
returns (jrnl:Jrnl)
requires kindsValid(kinds)
ensures fresh(jrnl)
Expand Down
18 changes: 9 additions & 9 deletions src/machine/bytes.s.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,46 +14,46 @@ module {:extern "bytes", "github.com/mit-pdos/daisy-nfsd/dafny_go/bytes"} ByteSl
|data| < U64.MAX
}

constructor {:extern} (data_: seq<byte>)
constructor {:axiom} {:extern} (data_: seq<byte>)
requires |data_| < U64.MAX
ensures data == data_
// {
// this.data := data_;
// }

function {:extern} Len(): (len:uint64)
function {:axiom} {:extern} Len(): (len:uint64)
reads this
requires Valid()
ensures len as nat == |data|
// {
// |data|
// }

function {:extern} Get(i: uint64): (x: byte)
function {:axiom} {:extern} Get(i: uint64): (x: byte)
reads this
requires i as nat < |data|
ensures x == data[i]
// {
// data[i]
// }

method {:extern} Set(i: uint64, b: byte)
method {:axiom} {:extern} Set(i: uint64, b: byte)
modifies this
requires i as nat < |data|
ensures data == old(data)[i as nat:=b]
// {
// data := data[i as nat := b];
// }

method {:extern} Append(b: byte)
method {:axiom} {:extern} Append(b: byte)
modifies this
requires no_overflow(|data|, 1)
ensures data == old(data) + [b]
// {
// data := data + [b];
// }

method {:extern} AppendBytes(bs: Bytes)
method {:axiom} {:extern} AppendBytes(bs: Bytes)
modifies this
// NOTE: I did not think of this initially, until the model proof
// caught it
Expand All @@ -64,7 +64,7 @@ module {:extern "bytes", "github.com/mit-pdos/daisy-nfsd/dafny_go/bytes"} ByteSl
// data := data + bs.data;
// }

method {:extern} Subslice(start: uint64, end: uint64)
method {:axiom} {:extern} Subslice(start: uint64, end: uint64)
modifies this
requires start as nat <= end as nat <= |data|
ensures data == old(data[start..end])
Expand All @@ -76,7 +76,7 @@ module {:extern "bytes", "github.com/mit-pdos/daisy-nfsd/dafny_go/bytes"} ByteSl
// copy some range of bs into some part of this
//
// Go: copy(this[dst:], bs[src:src+len])
method {:extern} CopySegment(dst: uint64, bs: Bytes, src: uint64, len: uint64)
method {:axiom} {:extern} CopySegment(dst: uint64, bs: Bytes, src: uint64, len: uint64)
modifies this
requires bs != this
requires src as nat + len as nat <= |bs.data|
Expand All @@ -86,7 +86,7 @@ module {:extern "bytes", "github.com/mit-pdos/daisy-nfsd/dafny_go/bytes"} ByteSl
// data := C.splice(data, dst as nat, bs.data[src..src as nat+len as nat]);
// }

method {:extern} Split(off: uint64) returns (bs: Bytes)
method {:axiom} {:extern} Split(off: uint64) returns (bs: Bytes)
modifies this
ensures fresh(bs)
requires off as nat <= |data|
Expand Down
8 changes: 4 additions & 4 deletions src/machine/int_encoding.s.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,25 +42,25 @@ module {:extern "encoding", "github.com/mit-pdos/daisy-nfsd/dafny_go/encoding"}
lemma {:axiom} lemma_enc_32_0()
ensures le_enc32(0) == [0,0,0,0]

method {:extern} UInt64Put(x: uint64, off: uint64, bytes: Bytes)
method {:axiom} {:extern} UInt64Put(x: uint64, off: uint64, bytes: Bytes)
modifies bytes
requires bytes.Valid() ensures bytes.Valid()
requires off as nat + u64_bytes <= |bytes.data|
ensures bytes.data == old(bytes.data[..off as nat] + le_enc64(x) + bytes.data[off as nat+u64_bytes..])

method {:extern} UInt64Get(bytes: Bytes, off: uint64)
method {:axiom} {:extern} UInt64Get(bytes: Bytes, off: uint64)
returns (x:uint64)
requires bytes.Valid()
requires off as nat + u64_bytes <= |bytes.data|
ensures x == le_dec64(bytes.data[off as nat..off as nat+u64_bytes])

method {:extern} UInt32Put(x: uint32, off: uint64, bytes: Bytes)
method {:axiom} {:extern} UInt32Put(x: uint32, off: uint64, bytes: Bytes)
modifies bytes
requires bytes.Valid() ensures bytes.Valid()
requires off as nat + u32_bytes <= |bytes.data|
ensures bytes.data == old(bytes.data[..off as nat] + le_enc32(x) + bytes.data[off as nat+u32_bytes..])

method {:extern} UInt32Get(bytes: Bytes, off: uint64)
method {:axiom} {:extern} UInt32Get(bytes: Bytes, off: uint64)
returns (x:uint32)
requires bytes.Valid()
requires off as nat + u32_bytes <= |bytes.data|
Expand Down

0 comments on commit aa3cd3c

Please sign in to comment.