tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

64e2248dbd4a05fc78b9d92cd775bb111951af95e384b91000e7f7aa32410013.tri (6402B)

      1 !import base as B
      2 !import native_math as N
      3 !import io_v2 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 split 0 rest = [[] rest]
     20 split _ [] = [[] []]
     21 split count [c | rest] = case split (N.predecessor count) rest of
     22   [prefix after] = [(B.pair c prefix) after]
     23   _ = []
     24 split     _ _    = []
     25 flatten   chunks = B.foldr (suffix chunk : B.append chunk suffix) [] (B.reverse chunks)
     26 readCount 0      = 1
     27 readCount remaining = case N.lte remaining 4096 of
     28   (t t) = remaining
     29   _ = 4096
     30 readLoop reader remaining chunks = do IO.onOk
     31   received <- IO.readSome reader (readCount remaining)
     32   case received of
     33     ("eof", t) = IO.pure (B.ok (flatten chunks) t)
     34     ("data", bytes) = case N.lte (B.length bytes) remaining of
     35       (t t) = readLoop reader (N.subtract remaining (B.length bytes)) (B.pair bytes chunks)
     36       _ = IO.pure (B.err ["invalid-bound" "storage/read" "file exceeds byte limit" "unknown"] t)
     37     _ = IO.fail "Invalid storage read reply"
     38 -- May consume one excess byte in the EOF probe at the budget boundary.
     39 readBytes path limit = checkedLimit limit (count : IO.scope (owner : do IO.onOk
     40   reader <- IO.openReader owner path
     41   readLoop reader count []))
     42 
     43 hashLoop digest remaining bytes = case split 4096 bytes of
     44   [[] []] = IO.finishDigest digest
     45   [part rest] = case N.lte (B.length part) remaining of
     46     (t t) = do IO.onOk
     47       IO.updateDigest digest part
     48       hashLoop digest (N.subtract remaining (B.length part)) rest
     49     _ = IO.pure (B.err ["invalid-bound" "storage/hash" "bytes exceed limit" "none"] t)
     50   _ = IO.pure (B.err ["invalid-argument" "storage/hash" "improper byte list" "none"] t)
     51 hashBytes limit bytes = checkedLimit limit (count : IO.scope (owner : do IO.onOk
     52   digest <- IO.openDigest owner "sha256"
     53   hashLoop digest count bytes))
     54 writeLoop writer bytes = case split 4096 bytes of
     55   [[] []] = IO.pure (B.ok t t)
     56   [part rest] = do IO.onOk
     57     IO.writeAll writer part
     58     writeLoop writer rest
     59   _ = IO.fail "Invalid preflighted byte list"
     60 
     61 verifyBytes reader remaining = do IO.onOk
     62   received <- IO.readSome reader 4096
     63   case received of
     64     ("eof", t) = case remaining of
     65       [] = IO.pure (B.ok t t)
     66       _ = IO.pure (B.err (problem "storage/verify" "different bytes") t)
     67     ("data", bytes) = case split (B.length bytes) remaining of
     68       [expected rest] = case B.equal? bytes expected of
     69         (t t) = verifyBytes reader rest
     70         _ = IO.pure (B.err (problem "storage/verify" "different bytes") t)
     71       _ = IO.fail "Invalid preflighted byte list"
     72     _ = IO.fail "Invalid verification read reply"
     73 verified owner directory destination verify created = do IO.onOk
     74   reader <- IO.openReader owner destination
     75   verify reader
     76   IO.syncFile reader
     77   IO.syncDirectory directory
     78   IO.pure (B.ok created t)
     79 -- Immutable names verify every winner, through EOF, before syncing its opened
     80 -- inode and directory. Mismatches remain intact for diagnosis. Mutable
     81 -- replacement acknowledges its own stage publication; a concurrent writer can
     82 -- legitimately replace the alias immediately afterward.
     83 publishBytes directory destination replace limit bytes = case replace of
     84   0 = do IO.onOk
     85     hashBytes limit bytes
     86     IO.scope (owner : do IO.onOk
     87       stage <- IO.openStage owner directory
     88       writeLoop stage bytes
     89       IO.sealStage stage
     90       status <- IO.publishNew stage destination
     91       case status of
     92         "published" = verified owner directory destination (reader : verifyBytes reader bytes) (t t)
     93         "exists" = verified owner directory destination (reader : verifyBytes reader bytes) t
     94         _ = IO.fail "Invalid publication reply")
     95   1 = do IO.onOk
     96     hashBytes limit bytes
     97     IO.scope (owner : do IO.onOk
     98       stage <- IO.openStage owner directory
     99       writeLoop stage bytes
    100       IO.sealStage stage
    101       IO.publishReplace stage destination
    102       IO.pure (B.ok (t t) t))
    103   _ = IO.pure (B.err ["invalid-argument" "storage/publish" "invalid replacement flag" "none"] t)
    104 
    105 verifyTree reader limit tree = do IO.onOk
    106   IO.verifyIndexedTree reader limit tree
    107   end <- IO.readSome reader 1
    108   case end of
    109     ("eof", t) = IO.pure (B.ok t t)
    110     _ = IO.pure (B.err (problem "storage/verify" "trailing bytes") t)
    111 publishTree directory destination limit expected tree = do IO.onOk
    112   info <- IO.hashIndexedTree limit tree
    113   case info of
    114     [_ actual] = case B.equal? actual expected of
    115       (t t) = IO.scope (owner : do IO.onOk
    116         stage <- IO.openStage owner directory
    117         IO.writeIndexedTree stage limit expected tree
    118         IO.sealStage stage
    119         status <- IO.publishNew stage destination
    120         case status of
    121           "published" = verified owner directory destination (reader : verifyTree reader limit tree) (t t)
    122           "exists" = verified owner directory destination (reader : verifyTree reader limit tree) t
    123           _ = IO.fail "Invalid publication reply")
    124       _ = IO.pure (B.err ["integrity-failed" "storage/publish" "digest mismatch" "none"] t)
    125     _ = IO.fail "Invalid indexed hash reply"
    126 readTree directory path limit expected = IO.scope (owner : do IO.onOk
    127   reader <- IO.openReader owner path
    128   size <- IO.fileSize reader
    129   IO.readIndexedTree reader directory limit size expected)
    130 
    131 -- POSIX lexical parent, retaining separators and literal '..' components.
    132 -- Callers pass complete paths to the native path validators for OS resolution.
    133 slashes []          = t t
    134 slashes [47 | rest] = slashes rest
    135 slashes _           = t
    136 trimSeparators [47 | rest] = trimSeparators rest
    137 trimSeparators rest        = rest
    138 parentReverse [] = "."
    139 parentReverse [47 | rest] = case slashes rest of
    140   (t t) = B.pair 47 (B.reverse rest)
    141   _ = B.reverse rest
    142 parentReverse [_ | rest] = parentReverse rest
    143 parentReverse _ = "."
    144 parentPath [] = "."
    145 parentPath path = case trimSeparators (B.reverse path) of
    146   [] = path
    147   rest = parentReverse rest