1	import Base
2	
3	# Audited host effects (spec §3.3). Thin syscall wrappers with .c + .js
4	# twins and matching intended semantics. No laws — validated empirically.
5	
6	def fsync(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
7	  import "./effs/fsync.c"
8	  import "./effs/fsync.js"
9	
10	def rename(old: String, new: String) -> IO(Result<&1, &1, U32 & String, Unit>):
11	  import "./effs/rename.c"
12	  import "./effs/rename.js"
13	
14	def remove(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
15	  import "./effs/remove.c"
16	  import "./effs/remove.js"
17	
18	def read_dir_count(path: String) -> IO(Result<&1, &1, U32 & String, Nat>):
19	  import "./effs/read_dir.c"
20	  import "./effs/read_dir.js"
21	
22	def read_dir_at(path: String, idx: Nat) -> IO(Result<&1, &1, U32 & String, String>):
23	  import "./effs/read_dir.c"
24	  import "./effs/read_dir.js"
25	
26	def make_dir(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
27	  import "./effs/make_dir.c"
28	  import "./effs/make_dir.js"
29	
30	def chmod(path: String, bits: U32) -> IO(Result<&1, &1, U32 & String, Unit>):
31	  import "./effs/chmod.c"
32	  import "./effs/chmod.js"
33	
34	def exists(path: String) -> IO(Result<&1, &1, U32 & String, Bool>):
35	  import "./effs/exists.c"
36	  import "./effs/exists.js"
37	
38	# Returns `<byte-count>;<text>` for a positional chunk whose end is adjusted to
39	# a complete UTF-8 boundary. The byte count advances the next positional read.
40	def read_utf8_chunk(path: String, offset: Nat, max_bytes: Nat) -> IO(Result<&1, &1, U32 & String, String>):
41	  import "./effs/read_utf8_chunk.c"
42	  import "./effs/read_utf8_chunk.js"
43	
44	# Pure accumulator step (leaf: matches structurally, never recurses).
45	# Past-end fetches answer "" (SNil{}), which is skipped.
46	
47	def grab_name(nm: String, acc: List<String>) -> List<String>:
48	  match nm:
49	    case SNil{}:
50	      acc
51	    case SCon{_, _}:
52	      Con{nm, acc}
53	
54	# Fuel-bounded sweep 0..count-1. Startup-only use (spec §10 below): the
55	# directory is stable during recovery, so count-then-fetch is exact.
56	
57	def read_go(fuel: Nat, +path: String, +idx: Nat, acc: List<String>) -> IO(List<String>):
58	  match fuel:
59	    case 0n:
60	      IO.pure(List<String>, List.reverse(&1, String, acc))
61	    case 1n+f:
62	      do IO<List<String>>:
63	        nm : String <- IO.try(String, read_dir_at(path, idx))
64	        read_go(f, path, Nat.add(idx, 1n), grab_name(nm, acc))
65	
66	def read_dir(+path: String) -> IO(Result<&1, &1, U32 & String, List<String>>):
67	  do IO<Result<&1, &1, U32 & String, List<String>>>:
68	    n : Nat <- IO.try(Nat, read_dir_count(path))
69	    names : List<String> <- read_go(Nat.add(n, 1n), path, 0n, Nil{})
70	    return Done{names}