hauleth.dev
Pure Erlang implementation of 9p2000 protocol
filesystem
fs
9p2000
erlang
9p
1% SPDX-FileCopyrightText: 2026 Łukasz Niemier <~@hauleth.dev>
2%
3% SPDX-License-Identifier: GPL-3.0-only
4
5-module(prop_e9p_msg).
6
7-include("e9p_internal.hrl").
8-include_lib("proper/include/proper.hrl").
9% -include_lib("stdlib/include/assert.hrl").
10
11int(N) ->
12 Min = 0,
13 Max = 1 bsl (N * 8) - 1,
14 integer(Min, Max).
15
16fid() -> int(2).
17
18bin_str() -> ?LET({Charlist}, {string()},
19 unicode:characters_to_binary(Charlist)).
20
21qid_type() -> union([directory,
22 append,
23 excl,
24 device,
25 auth,
26 tmp,
27 symlink,
28 regular
29 ]).
30
31qid() ->
32 ?LET({Type, Version, Path}, {qid_type(), int(4), int(8)},
33 e9p:make_qid(Type, Version, Path)).
34
35prop_tversion() ->
36 ?FORALL({Version, MPS}, {bin_str(), int(4)},
37 enc_dec(#tversion{version = Version, max_packet_size = MPS})).
38prop_rversion() ->
39 ?FORALL({Version, MPS}, {bin_str(), fid()},
40 enc_dec(#rversion{version = Version, max_packet_size = MPS})).
41
42prop_tauth() ->
43 ?FORALL({Afid, Uname, Aname}, {fid(), bin_str(), bin_str()},
44 enc_dec(#tauth{afid = Afid,
45 uname = Uname,
46 aname = Aname})).
47prop_rauth() ->
48 ?FORALL({AQID}, {qid()},
49 enc_dec(#rauth{aqid = AQID})).
50
51prop_rerror() ->
52 ?FORALL({Msg}, {bin_str()},
53 begin
54 enc_dec(#rerror{msg = Msg})
55 end).
56
57prop_tattach() ->
58 ?FORALL({FID, AFID, Uname, Aname}, {fid(), fid(), bin_str(), bin_str()},
59 enc_dec(#tattach{
60 fid = FID,
61 afid = AFID,
62 uname = Uname,
63 aname = Aname
64 })).
65prop_rattach() ->
66 ?FORALL({QID}, {qid()},
67 enc_dec(#rattach{qid = QID})).
68
69prop_twalk() ->
70 ?FORALL({FID, NewFID, Names}, {fid(), fid(), list(bin_str())},
71 enc_dec(#twalk{fid = FID, new_fid = NewFID, names = Names})).
72prop_rwalk() ->
73 ?FORALL({QIDs}, {list(qid())},
74 enc_dec(#rwalk{qids = QIDs})).
75
76prop_topen() ->
77 ?FORALL({FID, Mode}, {fid(), int(1)},
78 enc_dec(#topen{fid = FID, mode = Mode})).
79prop_ropen() ->
80 ?FORALL({QID, IOUnit}, {qid(), int(4)},
81 enc_dec(#ropen{qid = QID, io_unit = IOUnit})).
82
83prop_tcreate() ->
84 ?FORALL({FID, Name, Perm, Mode}, {fid(), bin_str(), int(4), int(1)},
85 enc_dec(#tcreate{fid = FID,
86 name = Name,
87 perm = Perm,
88 mode = Mode})).
89prop_rcreate() ->
90 ?FORALL({QID, IOUnit}, {qid(), int(4)},
91 enc_dec(#rcreate{qid = QID, io_unit = IOUnit})).
92
93prop_tremove() ->
94 ?FORALL({FID}, {fid()},
95 enc_dec(#tremove{fid = FID})).
96
97prop_tclunk() ->
98 ?FORALL({FID}, {fid()},
99 enc_dec(#tclunk{fid = FID})).
100
101prop_tread() ->
102 ?FORALL({FID, Offset, Len}, {fid(), int(8), int(4)},
103 enc_dec(#tread{fid = FID, offset = Offset, len = Len})).
104prop_rread() ->
105 ?FORALL({Data}, {binary()},
106 enc_dec(#rread{data = Data})).
107
108prop_twrite() ->
109 ?FORALL({FID, Offset, Data}, {fid(), int(8), binary()},
110 enc_dec(#twrite{fid = FID, offset = Offset, data = Data})).
111prop_rwrite() ->
112 ?FORALL({Len}, {int(4)},
113 enc_dec(#rwrite{len = Len})).
114
115prop_tstat() ->
116 ?FORALL({FID}, {fid()},
117 enc_dec(#tstat{fid = FID})).
118prop_rstat() ->
119 ?FORALL({QID, Type, Dev, Mode, Atime, Mtime, Len, Name, Uid, Gid, Muid},
120 {qid(), int(2), int(2), integer(0, 8#777), int(4), int(4), int(8), bin_str(), bin_str(),
121 bin_str(), bin_str()},
122 begin
123 enc_dec(#rstat{
124 stat = #{
125 type => Type,
126 dev => Dev,
127 qid => QID,
128 mode => Mode,
129 atime => Atime,
130 mtime => Mtime,
131 length => Len,
132 name => Name,
133 uid => Uid,
134 gid => Gid,
135 muid => Muid
136 }})
137 end).
138
139prop_tflush() ->
140 ?FORALL({Tag}, {int(2)}, enc_dec(#tflush{tag = Tag})).
141
142enc_dec(Data) ->
143 Tag = 1,
144 Out = e9p_msg:encode(Tag, Data),
145 Encoded = iolist_to_binary(Out),
146 {ok, Tag, Data} =:= e9p_msg:parse(Encoded).