Project P155
File share
Documents reached by path and saved by a handler that looks the path up twice and one that resolves it once: a move between the check and the write sends a save to a document the caller does not own.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-18
Every screen below was recorded under CPython. When this page was built, the EML interpreter replayed each session from the same input and printed the same bytes.
About
Documents reached by path, saved by two handlers - one that looks the path up to check and again to write, one that resolves it once - with an admin moving a path at a chosen point.
main.eml- the menu, the share, one save seen by both handlers, every save, and choosing the moveshare.eml- the paths, the owners, the users, the points a move can fall at, resolving a path, the owner of a document, a move, and a save by either handler
How each part works:
- Three paths: /reports/q3 to ann's doc-a, /reports/archive to root's doc-b, /notes/bob to bob's doc-c. The move an admin makes points /reports/q3 at doc-b, the archive.
- As in the corpus case
path-resolved-twice, the handler that looks the path up twice checks that the caller owns the document, then looks the path up again to write. If the move falls between the two, ann's save of /reports/q3 passes the check on her doc-a and writes root's doc-b: the value did not change under the write, the subject did. - The handler that resolves the path once checks and writes the same document, and never writes one the caller does not own. A move before the check refuses both; a move after the write changes neither.
- Over every user, path and point - 24 saves - looking up twice writes another document than it checked exactly when the saved path is moved between check and write. No test that moves a path first or last can see it.
What is checked: menu choices 1 to 5; the user ann or bob; a path from 1 to 3; the point never, before, between or after; for the move, a path from 1 to 3 and doc-a, doc-b or doc-c. An empty answer cancels.
Sessions: sessions/basic.in gives: - the share; ann saving /reports/q3 with the move between, before and after, and bob with no move; - every save; the move changed to /notes/bob pointed at doc-a, every save again, and bob saving /notes/bob with the move between.
sessions/bad-input.in gives: - menu choices 0 and x; - a save: a cancel and cy for the user, a cancel and 4 for the path, a cancel and later for the point; - the move: a cancel and 9 for the path, a cancel and doc-z for the document, then /reports/archive pointed at doc-b, where it already points; every save, none of them wrong.
Built on the verified corpus case path-resolved-twice (a permission check and a write that each resolve the name, against resolving it once, with the rename at every point).
Recorded sessions
What the screen shows while someone uses the program. Each typed line appears after its prompt, the way a terminal shows it.
bad-input
interpreter: byte-equal== File share ==
Documents reached by path, saved by a handler that looks the path up twice and one that resolves it once.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 0
Pick a number from 1 to 5.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> x
Pick a number from 1 to 5.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)>
Cancelled.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> cy
Type ann or bob.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)>
Cancelled.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)> 4
Type a path from 1 to 3.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)> 1
the move happens (never, before, between, after)>
Cancelled.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)> 1
the move happens (never, before, between, after)> later
Type never, before, between or after.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 4
path to move (1 to 3)>
Cancelled.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 4
path to move (1 to 3)> 9
Type a path from 1 to 3.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 4
path to move (1 to 3)> 2
point it at (doc-a, doc-b or doc-c)>
Cancelled.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 4
path to move (1 to 3)> 2
point it at (doc-a, doc-b or doc-c)> doc-z
Type doc-a, doc-b or doc-c.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 4
path to move (1 to 3)> 2
point it at (doc-a, doc-b or doc-c)> doc-b
The move is now: /reports/archive pointed at doc-b, root's document.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 3
Every user, path and point of the move (24 saves):
looks the path up twice: 8 writes, 0 to a document the caller does not own
resolves it once: 8 writes, 0 to a document the caller does not own
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 5
Bye.
What was typed (35 lines)
0
x
2
2
cy
2
ann
2
ann
4
2
ann
1
2
ann
1
later
4
4
9
4
2
4
2
doc-z
4
2
doc-b
3
5
basic
interpreter: byte-equal== File share ==
Documents reached by path, saved by a handler that looks the path up twice and one that resolves it once.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 1
The paths and the documents they point at:
/reports/q3 doc-a owned by ann
/reports/archive doc-b owned by root
/notes/bob doc-c owned by bob
The move an admin makes: /reports/q3 is pointed at doc-b, root's document.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)> 1
the move happens (never, before, between, after)> between
ann saves /reports/q3, the move between:
looks the path up twice: wrote doc-b, root's document - not ann's
resolves it once: wrote doc-a, ann's document
The check passed on doc-a and the write went to doc-b: between the two lookups the path was moved.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)> 1
the move happens (never, before, between, after)> before
ann saves /reports/q3, the move before:
looks the path up twice: refused: not ann's document
resolves it once: refused: not ann's document
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> ann
path (1 to 3)> 1
the move happens (never, before, between, after)> after
ann saves /reports/q3, the move after:
looks the path up twice: wrote doc-a, ann's document
resolves it once: wrote doc-a, ann's document
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> bob
path (1 to 3)> 1
the move happens (never, before, between, after)> never
bob saves /reports/q3, the move never:
looks the path up twice: refused: not bob's document
resolves it once: refused: not bob's document
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 3
Every user, path and point of the move (24 saves):
looks the path up twice: 7 writes, 1 to a document the caller does not own
resolves it once: 7 writes, 0 to a document the caller does not own
ann saving /reports/q3 with the move between wrote doc-b, root's
Only a move between the check and the write does it, which is why no test that moves a path first or last can see it.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 4
path to move (1 to 3)> 3
point it at (doc-a, doc-b or doc-c)> doc-a
The move is now: /notes/bob pointed at doc-a, ann's document.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 3
Every user, path and point of the move (24 saves):
looks the path up twice: 8 writes, 1 to a document the caller does not own
resolves it once: 8 writes, 0 to a document the caller does not own
bob saving /notes/bob with the move between wrote doc-a, ann's
Only a move between the check and the write does it, which is why no test that moves a path first or last can see it.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 2
user (ann or bob)> bob
path (1 to 3)> 3
the move happens (never, before, between, after)> between
bob saves /notes/bob, the move between:
looks the path up twice: wrote doc-a, ann's document - not bob's
resolves it once: wrote doc-c, bob's document
The check passed on doc-c and the write went to doc-a: between the two lookups the path was moved.
1) the share 2) a save 3) every save 4) choose the move 5) quit
choice> 5
Bye.
What was typed (27 lines)
1
2
ann
1
between
2
ann
1
before
2
ann
1
after
2
bob
1
never
3
4
3
doc-a
3
2
bob
3
between
5
Modules
The program as written, entry module first. Each module transpiles to its own Python file, which is what eml project run executes.
main.eml(entry)
eml# P155 file share: the paths, documents and owners, one save seen by both
# handlers with a move at a chosen point, every user, path and point, and
# choosing the move.
import share
def plain(s):
0 => i
len(s) => j
while i < j and s[i] == " ":
i + 1 => i
while j > i and s[j - 1] == " ":
j - 1 => j
return s[i:j]
def pad(s, n):
s => out
while len(out) < n:
out + " " => out
return out
def show(move):
"The paths and the documents they point at:" ^0
for p in share.paths():
(" " + pad(p[0], 18) + pad(p[1], 7) + "owned by " + share.owner(p[1])) ^0
("The move an admin makes: " + move[0] + " is pointed at " + move[1] + ", " + share.owner(move[1]) + "'s document.") ^0
def said(r, user):
if r[0] == "refused":
return "refused: not " + user + "'s document"
share.owner(r[1]) => o
if o == user:
return "wrote " + r[1] + ", " + o + "'s document"
return "wrote " + r[1] + ", " + o + "'s document - not " + user + "'s"
def one_save(move):
plain(input("user (ann or bob)> ")) => u
if u == "":
"Cancelled." ^0
return
if u != "ann" and u != "bob":
"Type ann or bob." ^0
return
plain(input("path (1 to 3)> ")) => t
if t == "":
"Cancelled." ^0
return
if t != "1" and t != "2" and t != "3":
"Type a path from 1 to 3." ^0
return
share.paths()[int(t) - 1][0] => name
plain(input("the move happens (never, before, between, after)> ")) => at
if at == "":
"Cancelled." ^0
return
False => ok
for p in share.points():
if p == at:
True => ok
if not ok:
"Type never, before, between or after." ^0
return
share.save("twice", u, name, at, move) => a
share.save("once", u, name, at, move) => b
(u + " saves " + name + ", the move " + at + ":") ^0
(" looks the path up twice: " + said(a, u)) ^0
(" resolves it once: " + said(b, u)) ^0
if a[0] == "written" and a[1] != b[1]:
("The check passed on " + b[1] + " and the write went to " + a[1] + ": between the two lookups the path was moved.") ^0
def every(move):
0 => n2
0 => bad2
0 => n1
0 => bad1
[] => wrongs
for u in share.users():
for p in share.paths():
for at in share.points():
share.save("twice", u, p[0], at, move) => a
share.save("once", u, p[0], at, move) => b
if a[0] == "written":
n2 + 1 => n2
if share.owner(a[1]) != u:
bad2 + 1 => bad2
wrongs + [u + " saving " + p[0] + " with the move " + at + " wrote " + a[1] + ", " + share.owner(a[1]) + "'s"] => wrongs
if b[0] == "written":
n1 + 1 => n1
if share.owner(b[1]) != u:
bad1 + 1 => bad1
("Every user, path and point of the move (" + str(len(share.users()) * len(share.paths()) * len(share.points())) + " saves):") ^0
(" looks the path up twice: " + str(n2) + " writes, " + str(bad2) + " to a document the caller does not own") ^0
(" resolves it once: " + str(n1) + " writes, " + str(bad1) + " to a document the caller does not own") ^0
for w in wrongs:
(" " + w) ^0
if bad2 > 0:
"Only a move between the check and the write does it, which is why no test that moves a path first or last can see it." ^0
def set_move(move):
plain(input("path to move (1 to 3)> ")) => t
if t == "":
"Cancelled." ^0
return move
if t != "1" and t != "2" and t != "3":
"Type a path from 1 to 3." ^0
return move
plain(input("point it at (doc-a, doc-b or doc-c)> ")) => d
if d == "":
"Cancelled." ^0
return move
if d != "doc-a" and d != "doc-b" and d != "doc-c":
"Type doc-a, doc-b or doc-c." ^0
return move
share.paths()[int(t) - 1][0] => name
("The move is now: " + name + " pointed at " + d + ", " + share.owner(d) + "'s document.") ^0
return [name, d]
["/reports/q3", "doc-b"] => move
"== File share ==" ^0
"Documents reached by path, saved by a handler that looks the path up twice and one that resolves it once." ^0
True => running
while running:
"" ^0
"1) the share 2) a save 3) every save 4) choose the move 5) quit" ^0
plain(input("choice> ")) => choice
if choice == "1":
show(move)
elif choice == "2":
one_save(move)
elif choice == "3":
every(move)
elif choice == "4":
set_move(move) => move
elif choice == "5":
False => running
else:
"Pick a number from 1 to 5." ^0
"Bye." ^0
Python projection (main.py)
import share
def plain(s):
i = 0
j = len(s)
while i < j and s[i] == " ":
i = i + 1
while j > i and s[j - 1] == " ":
j = j - 1
return s[i:j]
def pad(s, n):
out = s
while len(out) < n:
out = out + " "
return out
def show(move):
print("The paths and the documents they point at:")
for p in share.paths():
print(" " + pad(p[0], 18) + pad(p[1], 7) + "owned by " + share.owner(p[1]))
print("The move an admin makes: " + move[0] + " is pointed at " + move[1] + ", " + share.owner(move[1]) + "'s document.")
def said(r, user):
if r[0] == "refused":
return "refused: not " + user + "'s document"
o = share.owner(r[1])
if o == user:
return "wrote " + r[1] + ", " + o + "'s document"
return "wrote " + r[1] + ", " + o + "'s document - not " + user + "'s"
def one_save(move):
u = plain(input("user (ann or bob)> "))
if u == "":
print("Cancelled.")
return
if u != "ann" and u != "bob":
print("Type ann or bob.")
return
t = plain(input("path (1 to 3)> "))
if t == "":
print("Cancelled.")
return
if t != "1" and t != "2" and t != "3":
print("Type a path from 1 to 3.")
return
name = share.paths()[int(t) - 1][0]
at = plain(input("the move happens (never, before, between, after)> "))
if at == "":
print("Cancelled.")
return
ok = False
for p in share.points():
if p == at:
ok = True
if not ok:
print("Type never, before, between or after.")
return
a = share.save("twice", u, name, at, move)
b = share.save("once", u, name, at, move)
print(u + " saves " + name + ", the move " + at + ":")
print(" looks the path up twice: " + said(a, u))
print(" resolves it once: " + said(b, u))
if a[0] == "written" and a[1] != b[1]:
print("The check passed on " + b[1] + " and the write went to " + a[1] + ": between the two lookups the path was moved.")
def every(move):
n2 = 0
bad2 = 0
n1 = 0
bad1 = 0
wrongs = []
for u in share.users():
for p in share.paths():
for at in share.points():
a = share.save("twice", u, p[0], at, move)
b = share.save("once", u, p[0], at, move)
if a[0] == "written":
n2 = n2 + 1
if share.owner(a[1]) != u:
bad2 = bad2 + 1
wrongs = wrongs + [u + " saving " + p[0] + " with the move " + at + " wrote " + a[1] + ", " + share.owner(a[1]) + "'s"]
if b[0] == "written":
n1 = n1 + 1
if share.owner(b[1]) != u:
bad1 = bad1 + 1
print("Every user, path and point of the move (" + str(len(share.users()) * len(share.paths()) * len(share.points())) + " saves):")
print(" looks the path up twice: " + str(n2) + " writes, " + str(bad2) + " to a document the caller does not own")
print(" resolves it once: " + str(n1) + " writes, " + str(bad1) + " to a document the caller does not own")
for w in wrongs:
print(" " + w)
if bad2 > 0:
print("Only a move between the check and the write does it, which is why no test that moves a path first or last can see it.")
def set_move(move):
t = plain(input("path to move (1 to 3)> "))
if t == "":
print("Cancelled.")
return move
if t != "1" and t != "2" and t != "3":
print("Type a path from 1 to 3.")
return move
d = plain(input("point it at (doc-a, doc-b or doc-c)> "))
if d == "":
print("Cancelled.")
return move
if d != "doc-a" and d != "doc-b" and d != "doc-c":
print("Type doc-a, doc-b or doc-c.")
return move
name = share.paths()[int(t) - 1][0]
print("The move is now: " + name + " pointed at " + d + ", " + share.owner(d) + "'s document.")
return [name, d]
move = ["/reports/q3", "doc-b"]
print("== File share ==")
print("Documents reached by path, saved by a handler that looks the path up twice and one that resolves it once.")
running = True
while running:
print("")
print("1) the share 2) a save 3) every save 4) choose the move 5) quit")
choice = plain(input("choice> "))
if choice == "1":
show(move)
elif choice == "2":
one_save(move)
elif choice == "3":
every(move)
elif choice == "4":
move = set_move(move)
elif choice == "5":
running = False
else:
print("Pick a number from 1 to 5.")
print("Bye.")
share.eml
eml# P155 file share - documents reached by path, saved by two handlers. As in
# the corpus case path-resolved-twice, the handler that looks the path up
# to check the caller owns the document, and looks it up again to write,
# can check one document and write another when a path is moved between
# the two lookups: the value did not change under the write, the subject
# did. The handler that resolves the path once and uses the document for
# both cannot. Paths and owners are lists of pairs.
def paths():
return [["/reports/q3", "doc-a"], ["/reports/archive", "doc-b"], ["/notes/bob", "doc-c"]]
def owners():
return [["doc-a", "ann"], ["doc-b", "root"], ["doc-c", "bob"]]
def users():
return ["ann", "bob"]
def points():
return ["never", "before", "between", "after"]
def resolve(ps, name):
for p in ps:
if p[0] == name:
return p[1]
return ""
def owner(doc):
for o in owners():
if o[0] == doc:
return o[1]
return ""
def moved(ps, name, doc):
# the paths with name pointed at doc: an ordinary admin action
[] => out
for p in ps:
if p[0] == name:
out + [[name, doc]] => out
else:
out + [p] => out
return out
def save(handler, user, name, at, move):
# [outcome, the document written or ""]; move is [path, document] and
# at the point it happens: never, before, between (after the check,
# before the write) or after
paths() => ps
if at == "before":
moved(ps, move[0], move[1]) => ps
resolve(ps, name) => checked
if owner(checked) != user:
return ["refused", ""]
if at == "between":
moved(ps, move[0], move[1]) => ps
if handler == "twice":
resolve(ps, name) => written
else:
checked => written
return ["written", written]
Python projection (share.py)
def paths():
return [["/reports/q3", "doc-a"], ["/reports/archive", "doc-b"], ["/notes/bob", "doc-c"]]
def owners():
return [["doc-a", "ann"], ["doc-b", "root"], ["doc-c", "bob"]]
def users():
return ["ann", "bob"]
def points():
return ["never", "before", "between", "after"]
def resolve(ps, name):
for p in ps:
if p[0] == name:
return p[1]
return ""
def owner(doc):
for o in owners():
if o[0] == doc:
return o[1]
return ""
def moved(ps, name, doc):
out = []
for p in ps:
if p[0] == name:
out = out + [[name, doc]]
else:
out = out + [p]
return out
def save(handler, user, name, at, move):
ps = paths()
if at == "before":
ps = moved(ps, move[0], move[1])
checked = resolve(ps, name)
if owner(checked) != user:
return ["refused", ""]
if at == "between":
ps = moved(ps, move[0], move[1])
if handler == "twice":
written = resolve(ps, name)
else:
written = checked
return ["written", written]