src/storage/PROOF.bend

bendtorch-core@0.1.0.0 · 70 lines · 0 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
4import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as Laws
5import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
6import bendtorch-core@0.1.0.0/src/storage/frame.bend as Frame
7import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
8import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
9
10def Laws.write_read(T, d, array, path, value, valid):
11  Frame.write_read(T, d, array, path, value, valid)
12
13def Laws.update_frame(T, d, array, i, j, value, valid):
14  Frame.update_frame(T, d, array, i, j, value, valid)
15
16def Laws.read_refines(T, d, array, path, valid):
17  Frame.read_refines(T, d, array, path, valid)
18
19def Laws.read_retains(T, d, array, path, valid):
20  Frame.read_retains(T, d, array, path, valid)
21
22def Laws.primitive_update_frame(T, d, array, i, other, value, valid):
23  Frame.primitive_update_frame(T, d, array, i, other, value, valid)
24
25def Laws.path_self_same(d, path):
26  Frame.path_self_same(d, path)
27
28def Laws.primitive_write_read(T, d, array, i, value, valid):
29  Frame.primitive_write_read(T, d, array, i, value, valid)
30
31def Laws.new_too_large(n, value, over):
32  Api.new_refused(U32.to_nat(n), value, U32.is_le(n, 1048576), Equal.sym(Bool, U32.is_le(n, 1048576), False{}, over),
33    Api.positive_of(U32.to_nat(n), U32.to_nat(1048576), Api.over_nat(n, over)))
34
35def Laws.get_outside(storage, i, outside):
36  match storage:
37    case Storage.Empty{}:
38      {==}
39    case Storage.Owned{+d, +n, array, balanced, valid}:
40      Api.get_checked_miss(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid,
41        Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), False{}, outside))
42
43def Laws.set_outside(storage, i, value, outside):
44  match storage:
45    case Storage.Empty{}:
46      {==}
47    case Storage.Owned{+d, +n, array, balanced, valid}:
48      %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid),
49        (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}),
50        Api.set_checked_miss(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid,
51          Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), False{}, outside))) :
52        {Laws.outcome(Result<&2, &2, Storage.Error, Unit>, _) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, Unit>}
53      {==}
54
55def Laws.replay_size(n, value, ops, fits):
56  Api.new_size(U32.to_nat(n), value, U32.is_le(n, 1048576), ops, Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits), Api.cap_from(n, fits))
57
58def Laws.replay_get(n, value, ops, j, fits, inside):
59  Api.new_read(U32.to_nat(n), value, U32.is_le(n, 1048576), ops, j, Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits),
60    Api.cap_from(n, fits), inside)
61
62def Laws.new_fits(n, value, fits):
63  Api.new_fits(U32.to_nat(n), value, U32.is_le(n, 1048576), Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits), Api.cap_from(n, fits))
64
65def Laws.new_empty(value):
66  {==}
67
68def Laws.replay_set(n, value, ops, j, w, fits, inside):
69  Api.new_status(U32.to_nat(n), value, U32.is_le(n, 1048576), ops, j, w, Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits),
70    Api.cap_from(n, fits), inside)