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	# Read-only byte size for Bend-side accounting (no shell wc needed).
39	def file_size(path: String) -> IO(Result<&1, &1, U32 & String, Nat>):
40	  import "./effs/file_size.c"
41	  import "./effs/file_size.js"
42	
43	# Returns `<byte-count>;<text>` for a positional chunk whose end is adjusted to
44	# a complete UTF-8 boundary. The byte count advances the next positional read.
45	def read_utf8_chunk(path: String, offset: Nat, max_bytes: Nat) -> IO(Result<&1, &1, U32 & String, String>):
46	  import "./effs/read_utf8_chunk.c"
47	  import "./effs/read_utf8_chunk.js"
48	
49	# Pure accumulator step (leaf: matches structurally, never recurses).
50	# Past-end fetches answer "" (SNil{}), which is skipped.
51	
52	def grab_name(nm: String, acc: List<String>) -> List<String>:
53	  match nm:
54	    case SNil{}:
55	      acc
56	    case SCon{_, _}:
57	      Con{nm, acc}
58	
59	# Fuel-bounded sweep 0..count-1. Startup-only use (spec §10 below): the
60	# directory is stable during recovery, so count-then-fetch is exact.
61	
62	def read_go(fuel: Nat, +path: String, +idx: Nat, acc: List<String>) -> IO(List<String>):
63	  match fuel:
64	    case 0n:
65	      IO.pure(List<String>, List.reverse(&1, String, acc))
66	    case 1n+f:
67	      do IO<List<String>>:
68	        nm : String <- IO.try(String, read_dir_at(path, idx))
69	        read_go(f, path, Nat.add(idx, 1n), grab_name(nm, acc))
70	
71	def read_dir(+path: String) -> IO(Result<&1, &1, U32 & String, List<String>>):
72	  do IO<Result<&1, &1, U32 & String, List<String>>>:
73	    n : Nat <- IO.try(Nat, read_dir_count(path))
74	    names : List<String> <- read_go(Nat.add(n, 1n), path, 0n, Nil{})
75	    return Done{names}