f389a5949bce196d183e11389c9bd46f3e97cb990b6f9368300e6df79ee6e1a1.tri (7705B)
1 !import base as B 2 !import native_math as N 3 !import io as IO 4 !export readBytes 5 !export hashBytes 6 !export publishBytes 7 !export readTree 8 !export publishTree 9 !export parentPath 10 11 -- Caller-selected limits and directories. Whole byte lists are resident source 12 -- values; transport chunks have a fixed bound. Paths follow OS authority. 13 problem op detail = ["invalid-data" op detail "unknown"] 14 checkedLimit limit next = case B.isNat? limit of 15 (t t) = case N.lte limit 9223372036854775807 of 16 (t t) = next limit 17 _ = IO.pure (B.err ["invalid-bound" "storage/limit" "invalid byte limit" "none"] t) 18 _ = IO.pure (B.err ["invalid-bound" "storage/limit" "invalid byte limit" "none"] t) 19 -- A fixed composition supplies 4096 structural steps without a per-byte 20 -- numeric countdown. Each step preserves the proper-list failure sentinel; 21 -- reaching the bound leaves the suffix for the next chunk to validate. 22 chunkEnd rest = [[] rest] 23 chunkStep next [] = [[] []] 24 chunkStep next [c | rest] = case next rest of 25 [prefix after] = [(B.pair c prefix) after] 26 _ = [] 27 chunkStep _ _ = [] 28 doubleStep step next = step (step next) 29 chunkSteps = chunkStep 30 |> doubleStep |> doubleStep |> doubleStep |> doubleStep 31 |> doubleStep |> doubleStep |> doubleStep |> doubleStep 32 |> doubleStep |> doubleStep |> doubleStep |> doubleStep 33 chunk bytes = chunkSteps chunkEnd bytes 34 -- Only host-produced proper chunks, or prefixes checked by chunk, reach here. 35 -- Count their cells directly, preserving the public base.length contract. 36 chunkLength [] = 0 37 chunkLength [_ | rest] = N.successor (chunkLength rest) 38 chunkLength _ = 0 39 flatten chunks = B.foldr (suffix chunk : B.append chunk suffix) [] (B.reverse chunks) 40 readCount 0 = 1 41 readCount remaining = case N.lte remaining 4096 of 42 (t t) = remaining 43 _ = 4096 44 readLoop reader remaining chunks = do IO.onOk 45 received <- IO.readSome reader (readCount remaining) 46 case received of 47 ("eof", t) = IO.pure (B.ok (flatten chunks) t) 48 ("data", bytes) = let count = chunkLength bytes in case N.lte count remaining of 49 (t t) = readLoop reader (N.subtract remaining count) (B.pair bytes chunks) 50 _ = IO.pure (B.err ["invalid-bound" "storage/read" "file exceeds byte limit" "unknown"] t) 51 _ = IO.fail "Invalid storage read reply" 52 -- May consume one excess byte in the EOF probe at the budget boundary. 53 readBytes path limit = checkedLimit limit (count : IO.scope (owner : do IO.onOk 54 reader <- IO.openReader owner path 55 readLoop reader count [])) 56 57 hashLoop digest remaining bytes = case chunk bytes of 58 [[] []] = IO.finishDigest digest 59 [part rest] = case N.lte 4096 remaining of 60 -- A short final chunk may leave unused budget; its empty suffix completes 61 -- the digest. Every non-final chunk consumes exactly 4096 bytes. 62 (t t) = do IO.onOk 63 IO.updateDigest digest part 64 hashLoop digest (N.subtract remaining 4096) rest 65 _ = let count = chunkLength part in case N.lte count remaining of 66 (t t) = do IO.onOk 67 IO.updateDigest digest part 68 hashLoop digest (N.subtract remaining count) rest 69 _ = IO.pure (B.err ["invalid-bound" "storage/hash" "bytes exceed limit" "none"] t) 70 _ = IO.pure (B.err ["invalid-argument" "storage/hash" "improper byte list" "none"] t) 71 hashBytes limit bytes = checkedLimit limit (count : IO.scope (owner : do IO.onOk 72 digest <- IO.openDigest owner "sha256" 73 hashLoop digest count bytes)) 74 writeLoop writer bytes = case chunk bytes of 75 [[] []] = IO.pure (B.ok t t) 76 [part rest] = do IO.onOk 77 IO.writeAll writer part 78 writeLoop writer rest 79 _ = IO.fail "Invalid preflighted byte list" 80 81 -- Compare only the received prefix, returning the unconsumed expected suffix. 82 -- Both inputs have already passed their byte/proper-list validation boundary. 83 verifyPrefix [] remaining = [remaining] 84 verifyPrefix [byte | bytes] [expected | rest] = case B.equal? byte expected of 85 (t t) = verifyPrefix bytes rest 86 _ = [] 87 verifyPrefix _ _ = [] 88 verifyBytes reader remaining = do IO.onOk 89 received <- IO.readSome reader 4096 90 case received of 91 ("eof", t) = case remaining of 92 [] = IO.pure (B.ok t t) 93 _ = IO.pure (B.err (problem "storage/verify" "different bytes") t) 94 ("data", bytes) = case verifyPrefix bytes remaining of 95 [rest] = verifyBytes reader rest 96 _ = IO.pure (B.err (problem "storage/verify" "different bytes") t) 97 _ = IO.fail "Invalid verification read reply" 98 verified owner directory destination verify created = do IO.onOk 99 reader <- IO.openReader owner destination 100 verify reader 101 IO.syncFile reader 102 IO.syncDirectory directory 103 IO.pure (B.ok created t) 104 -- Immutable names verify every winner, through EOF, before syncing its opened 105 -- inode and directory. Mismatches remain intact for diagnosis. Mutable 106 -- replacement acknowledges its own stage publication; a concurrent writer can 107 -- legitimately replace the alias immediately afterward. 108 publishBytes directory destination replace limit bytes = case replace of 109 0 = do IO.onOk 110 hashBytes limit bytes 111 IO.scope (owner : do IO.onOk 112 stage <- IO.openStage owner directory 113 writeLoop stage bytes 114 IO.sealStage stage 115 status <- IO.publishNew stage destination 116 case status of 117 "published" = verified owner directory destination (reader : verifyBytes reader bytes) (t t) 118 "exists" = verified owner directory destination (reader : verifyBytes reader bytes) t 119 _ = IO.fail "Invalid publication reply") 120 1 = do IO.onOk 121 hashBytes limit bytes 122 IO.scope (owner : do IO.onOk 123 stage <- IO.openStage owner directory 124 writeLoop stage bytes 125 IO.sealStage stage 126 IO.publishReplace stage destination 127 IO.pure (B.ok (t t) t)) 128 _ = IO.pure (B.err ["invalid-argument" "storage/publish" "invalid replacement flag" "none"] t) 129 130 verifyTree reader limit tree = do IO.onOk 131 IO.verifyIndexedTree reader limit tree 132 end <- IO.readSome reader 1 133 case end of 134 ("eof", t) = IO.pure (B.ok t t) 135 _ = IO.pure (B.err (problem "storage/verify" "trailing bytes") t) 136 publishTree directory destination limit expected tree = do IO.onOk 137 info <- IO.hashIndexedTree limit tree 138 case info of 139 [_ actual] = case B.equal? actual expected of 140 (t t) = IO.scope (owner : do IO.onOk 141 stage <- IO.openStage owner directory 142 IO.writeIndexedTree stage limit expected tree 143 IO.sealStage stage 144 status <- IO.publishNew stage destination 145 case status of 146 "published" = verified owner directory destination (reader : verifyTree reader limit tree) (t t) 147 "exists" = verified owner directory destination (reader : verifyTree reader limit tree) t 148 _ = IO.fail "Invalid publication reply") 149 _ = IO.pure (B.err ["integrity-failed" "storage/publish" "digest mismatch" "none"] t) 150 _ = IO.fail "Invalid indexed hash reply" 151 readTree directory path limit expected = IO.scope (owner : do IO.onOk 152 reader <- IO.openReader owner path 153 size <- IO.fileSize reader 154 IO.readIndexedTree reader directory limit size expected) 155 156 -- POSIX lexical parent, retaining separators and literal '..' components. 157 -- Callers pass complete paths to the native path validators for OS resolution. 158 slashes [] = t t 159 slashes [47 | rest] = slashes rest 160 slashes _ = t 161 trimSeparators [47 | rest] = trimSeparators rest 162 trimSeparators rest = rest 163 parentReverse [] = "." 164 parentReverse [47 | rest] = case slashes rest of 165 (t t) = B.pair 47 (B.reverse rest) 166 _ = B.reverse rest 167 parentReverse [_ | rest] = parentReverse rest 168 parentReverse _ = "." 169 parentPath [] = "." 170 parentPath path = case trimSeparators (B.reverse path) of 171 [] = path 172 rest = parentReverse rest