Research.hs (12741B)
1 {-# LANGUAGE PatternSynonyms #-} 2 3 module Research where 4 5 import Crypto.Hash (hash, SHA256, Digest) 6 import Data.ByteArray (convert) 7 import Data.ByteString.Base16 (decode, encode) 8 import Data.List (intercalate) 9 import Data.Map () 10 import Data.Text (Text, replace) 11 import Data.Text.Encoding (decodeUtf8, encodeUtf8) 12 import Data.Word (Word8) 13 import qualified Data.ByteString as BS 14 import qualified Data.Map as Map 15 import qualified Data.Set as Set 16 import qualified Data.Text as T 17 18 -- Tree Calculus Types 19 data T = Leaf | Stem T | Fork T T 20 deriving (Show, Eq, Ord) 21 22 -- Contract source annotations for @ and =@ syntax. ViewExpr carries the 23 -- surface syntax of a contract until Frontend.ContractDesugar turns it into a 24 -- runtime contract application. 25 data ViewExpr 26 = VEName String 27 | VEVar String 28 | VEVarId Integer 29 | VEInt Integer 30 | VEString String 31 | VEList [ViewExpr] 32 | VEApp ViewExpr ViewExpr 33 | VEForall [Integer] ViewExpr 34 | VEExists [Integer] ViewExpr 35 | VERaw String 36 deriving (Show, Eq, Ord) 37 38 data DefArg 39 = DefBinder String (Maybe ViewExpr) 40 | DefPhantom ViewExpr 41 deriving (Show, Eq, Ord) 42 43 -- Abstract Syntax Tree for tricu 44 data TricuAST 45 = SVar String (Maybe String) 46 | SInt Integer 47 | SStr String 48 | SList [TricuAST] 49 | SDef String [String] TricuAST 50 | SDefAnn String [DefArg] (Maybe ViewExpr) TricuAST 51 | SApp TricuAST TricuAST 52 | TLeaf 53 | TStem TricuAST 54 | TFork TricuAST TricuAST 55 | SLambda [String] TricuAST 56 -- Non-recursive local binding: `name = boundValue` scoped over `body`. 57 -- Produced by let/where desugaring. `boundValue` already folds any binding 58 -- arguments into nested SLambda. Semantically equal to 59 -- SApp (SLambda [name] body) boundValue 60 | SLet String TricuAST TricuAST 61 | SEmpty 62 | SImport String String 63 deriving (Show, Eq, Ord) 64 65 -- Lexer Tokens 66 data LToken 67 = LIdentifier String 68 | LIdentifierWithHash String String 69 | LKeywordT 70 | LNamespace String 71 | LImport String String 72 | LAssign 73 | LAssignAt 74 | LAt 75 | LColon 76 | LDot 77 | LOpenParen 78 | LCloseParen 79 | LOpenBracket 80 | LCloseBracket 81 | LStringLiteral String 82 | LIntegerLiteral Int 83 | LArrowLeft 84 | LArrowRight 85 | LBindArrow 86 | LNewline 87 | LIndent Int 88 deriving (Eq, Show, Ord) 89 90 -- Output formats 91 data EvaluatedForm = Tree | FSL | AST | Ternary | Ascii | Decode | Number | StringLit 92 deriving (Show) 93 94 -- Environment containing previously evaluated TC terms 95 type Env = Map.Map String T 96 97 -- Merkle DAG Node types 98 -- Each Tree Calculus node becomes a content-addressed object. 99 type MerkleHash = Text 100 101 data Node 102 = NLeaf 103 | NStem MerkleHash 104 | NFork MerkleHash MerkleHash 105 deriving (Show, Eq, Ord) 106 107 -- | Canonical serialization of a Node for hashing. 108 -- Leaf: 0x00 109 -- Stem: 0x01 || child_hash (32 bytes) 110 -- Fork: 0x02 || left_hash (32 bytes) || right_hash (32 bytes) 111 serializeNode :: Node -> BS.ByteString 112 serializeNode NLeaf = BS.pack [0x00] 113 serializeNode (NStem h) = BS.pack [0x01] <> go (decode (encodeUtf8 h)) 114 where go (Left _) = error "Research.serializeNode: invalid hex hash" 115 go (Right bs) = bs 116 serializeNode (NFork l r) = BS.pack [0x02] <> go (decode (encodeUtf8 l)) <> go (decode (encodeUtf8 r)) 117 where go (Left _) = error "Research.serializeNode: invalid hex hash" 118 go (Right bs) = bs 119 120 -- | Hash a node per the Merkle content-addressing spec. 121 -- hash = SHA256( "arboricx.merkle.node.v1" <> 0x00 <> node_payload ) 122 nodeHash :: Node -> MerkleHash 123 nodeHash node = decodeUtf8 (encode (sha256WithPrefix (serializeNode node))) 124 where sha256WithPrefix payload = 125 convert . (hash :: BS.ByteString -> Digest SHA256) $ utf8Tag <> BS.pack [0x00] <> payload 126 utf8Tag = BS.pack $ map fromIntegral $ BS.unpack "arboricx.merkle.node.v1" 127 128 -- | Deserialize a Node from canonical bytes. 129 deserializeNode :: BS.ByteString -> Node 130 deserializeNode bs = 131 case BS.uncons bs of 132 Just (0x00, rest) 133 | BS.null rest -> NLeaf 134 135 Just (0x01, rest) 136 | BS.length rest == 32 -> 137 NStem $ decodeUtf8 (encode rest) 138 139 Just (0x02, rest) 140 | BS.length rest == 64 -> 141 let (l, r) = BS.splitAt 32 rest 142 in NFork (decodeUtf8 (encode l)) (decodeUtf8 (encode r)) 143 144 _ -> errorWithoutStackTrace "invalid merkle node payload" 145 146 -- --------------------------------------------------------------------------- 147 -- ByteString / bytestream marshalling via existing Tree Calculus conventions 148 -- --------------------------------------------------------------------------- 149 150 -- | Encode a single byte (Word8) as a Tree Calculus number (0..255). 151 ofByte :: Word8 -> T 152 ofByte = ofNumber . fromIntegral 153 154 -- | Decode a Tree Calculus number as a single byte (Word8). 155 -- Rejects values outside the range 0..255. 156 toByte :: T -> Either String Word8 157 toByte t = case toNumber t of 158 Left err -> Left err 159 Right n 160 | n >= 0 && n <= 255 -> Right (fromIntegral n) 161 | otherwise -> Left ("Byte value out of range: " ++ show n) 162 163 -- | Encode a ByteString as a Tree Calculus list of Byte trees. 164 ofBytes :: BS.ByteString -> T 165 ofBytes = ofList . map ofByte . BS.unpack 166 167 -- | Decode a Tree Calculus list of Byte trees as a ByteString. 168 -- Rejects non-list trees and elements that are not valid byte values (0..255). 169 toBytes :: T -> Either String BS.ByteString 170 toBytes t = case toList t of 171 Left err -> Left err 172 Right bs -> BS.pack <$> mapM toByte bs 173 174 -- | Convert a canonical Arboricx node payload (ByteString) to a Tree 175 -- representation (a list of Byte trees). 176 nodePayloadToTreeBytes :: BS.ByteString -> T 177 nodePayloadToTreeBytes = ofBytes 178 179 -- | Convert a Tree representation of a node payload back to ByteString. 180 treeBytesToNodePayload :: T -> Either String BS.ByteString 181 treeBytesToNodePayload = toBytes 182 183 -- | Convert a MerkleHash (hex-encoded) to a Tree of its 32 raw bytes. 184 hashToTreeBytes :: MerkleHash -> Either String T 185 hashToTreeBytes h = case decode (encodeUtf8 h) of 186 Left _ -> Left "Invalid hex MerkleHash" 187 Right raw 188 | BS.length raw == 32 -> Right (ofBytes raw) 189 | otherwise -> Left "Hash raw bytes must be 32 bytes" 190 191 -- | Convert a Tree of 32 Byte trees back to a MerkleHash (hex string). 192 treeBytesToHash :: T -> Either String MerkleHash 193 treeBytesToHash t = case toList t of 194 Left err -> Left err 195 Right bytes 196 | length bytes == 32 -> do 197 raw <- BS.pack <$> mapM toByte bytes 198 Right $ decodeUtf8 (encode raw) 199 | otherwise -> Left "Expected exactly 32 byte elements for hash" 200 201 -- | Build a Merkle DAG from a Tree Calculus term. 202 buildMerkle :: T -> Node 203 buildMerkle Leaf = NLeaf 204 buildMerkle (Stem t) = NStem (nodeHash child) 205 where child = buildMerkle t 206 buildMerkle (Fork l r) = NFork (nodeHash left) (nodeHash right) 207 where 208 left = buildMerkle l 209 right = buildMerkle r 210 211 -- Tree Calculus Reduction Rules 212 {- 213 The t operator is left associative. 214 1. t t a b -> a 215 2. t (t a) b c -> a c (b c) 216 3a. t (t a b) c t -> a 217 3b. t (t a b) c (t u) -> b u 218 3c. t (t a b) c (t u v) -> c u v 219 -} 220 apply :: T -> T -> T 221 apply (Fork Leaf a) _ = a 222 apply (Fork (Stem a) b) c = apply (apply a c) (apply b c) 223 apply (Fork (Fork _a _b) _c) Leaf = _a 224 apply (Fork (Fork _a _b) _c) (Stem u) = apply _b u 225 apply (Fork (Fork _a _b) _c) (Fork u v) = apply (apply _c u) v 226 -- Left associative `t` 227 apply Leaf b = Stem b 228 apply (Stem a) b = Fork a b 229 230 -- Booleans 231 _false :: T 232 _false = Leaf 233 234 _true :: T 235 _true = Stem Leaf 236 237 _not :: T 238 _not = Fork (Fork _true (Fork Leaf _false)) Leaf 239 240 -- Marshalling 241 ofString :: String -> T 242 ofString str = ofList $ map (ofNumber . toInteger . fromEnum) str 243 244 ofNumber :: Integer -> T 245 ofNumber 0 = Leaf 246 ofNumber n = 247 Fork 248 (if odd n then Stem Leaf else Leaf) 249 (ofNumber (n `div` 2)) 250 251 ofList :: [T] -> T 252 ofList = foldr Fork Leaf 253 254 toNumber :: T -> Either String Integer 255 toNumber Leaf = Right 0 256 toNumber (Fork Leaf rest) = case toNumber rest of 257 Right n -> Right (2 * n) 258 Left err -> Left err 259 toNumber (Fork (Stem Leaf) rest) = case toNumber rest of 260 Right n -> Right (1 + 2 * n) 261 Left err -> Left err 262 toNumber _ = Left "Invalid Tree Calculus number" 263 264 toChar :: Integer -> Either String Char 265 toChar n 266 | n < 0 = Left "Negative character code" 267 | n > 0x10FFFF = Left "Character code out of Unicode range" 268 | n >= 0xD800 && n <= 0xDFFF = Left "Surrogate character code not allowed" 269 | otherwise = Right (toEnum (fromInteger n)) 270 271 toString :: T -> Either String String 272 toString tc = do 273 list <- toList tc 274 nums <- mapM toNumber list 275 mapM toChar nums 276 277 toList :: T -> Either String [T] 278 toList Leaf = Right [] 279 toList (Fork x rest) = case toList rest of 280 Right xs -> Right (x : xs) 281 Left err -> Left err 282 toList _ = Left "Invalid Tree Calculus list" 283 284 -- Outputs 285 formatT :: EvaluatedForm -> T -> String 286 formatT Tree = toSimpleT . show 287 formatT FSL = show 288 formatT AST = show . toAST 289 formatT Ternary = toTernaryString 290 formatT Ascii = toAscii 291 formatT Decode = decodeResult 292 formatT Number = either (\e -> "<not-number: " ++ e ++ ">") show . toNumber 293 formatT StringLit = either (\e -> "<not-string: " ++ e ++ ">") show . toString 294 295 toSimpleT :: String -> String 296 toSimpleT s = T.unpack 297 $ replace "Fork" "t" 298 $ replace "Stem" "t" 299 $ replace "Leaf" "t" 300 $ T.pack s 301 302 toTernaryString :: T -> String 303 toTernaryString Leaf = "0" 304 toTernaryString (Stem t) = "1" ++ toTernaryString t 305 toTernaryString (Fork t1 t2) = "2" ++ toTernaryString t1 ++ toTernaryString t2 306 307 toAST :: T -> TricuAST 308 toAST Leaf = TLeaf 309 toAST (Stem a) = TStem (toAST a) 310 toAST (Fork a b) = TFork (toAST a) (toAST b) 311 312 toAscii :: T -> String 313 toAscii tree = go tree "" True 314 where 315 go :: T -> String -> Bool -> String 316 go Leaf prefix isLast = 317 prefix ++ (if isLast then "`-- " else "|-- ") ++ "Leaf\n" 318 go (Stem t) prefix isLast = 319 prefix ++ (if isLast then "`-- " else "|-- ") ++ "Stem\n" 320 ++ go t (prefix ++ (if isLast then " " else "| ")) True 321 go (Fork left right) prefix isLast = 322 prefix ++ (if isLast then "`-- " else "|-- ") ++ "Fork\n" 323 ++ go left (prefix ++ (if isLast then " " else "| ")) False 324 ++ go right (prefix ++ (if isLast then " " else "| ")) True 325 326 decodeResult :: T -> String 327 decodeResult Leaf = "t" 328 decodeResult tc = 329 case (toString tc, toList tc, toNumber tc) of 330 (Right s, _, _) | all isCommonChar s -> "\"" ++ s ++ "\"" 331 (_, _, Right n) -> show n 332 (_, Right xs@(_:_), _) -> "[" ++ intercalate ", " (map decodeResult xs) ++ "]" 333 (_, Right [], _) -> "[]" 334 _ -> formatT Tree tc 335 where 336 isCommonChar c = 337 let n = fromEnum c 338 in (n >= 32 && n <= 126) 339 || n == 9 340 || n == 10 341 || n == 13 342 343 -- --------------------------------------------------------------------------- 344 -- DAG node-table export (for host-language kernel embedding) 345 -- --------------------------------------------------------------------------- 346 347 -- | Export a term's Merkle DAG as a topologically-sorted node table. 348 -- Children appear before parents so all index references are forward. 349 -- Returns (root index, list of (tag, [child_indices])). 350 exportDag :: T -> (Int, [(String, [Int])]) 351 exportDag term = 352 let (root, acc, _) = collectDag term [] Set.empty 353 -- acc is in reverse post-order (children first, root last) 354 ordered = reverse acc 355 idxMap = Map.fromList [(h, i) | (i, (h, _)) <- zip [0..] ordered] 356 rootIdx = idxMap Map.! root 357 lines_ = map (formatNode idxMap . snd) ordered 358 in (rootIdx, lines_) 359 where 360 collectDag :: T -> [(MerkleHash, Node)] -> Set.Set MerkleHash -> (MerkleHash, [(MerkleHash, Node)], Set.Set MerkleHash) 361 collectDag Leaf acc seen = 362 let h = nodeHash NLeaf 363 in if Set.member h seen then (h, acc, seen) else (h, (h, NLeaf) : acc, Set.insert h seen) 364 collectDag (Stem t) acc seen = 365 let (ch, acc', seen') = collectDag t acc seen 366 node = NStem ch 367 h = nodeHash node 368 in if Set.member h seen' then (h, acc', seen') else (h, (h, node) : acc', Set.insert h seen') 369 collectDag (Fork l r) acc seen = 370 let (lh, acc', seen') = collectDag l acc seen 371 (rh, acc'', seen'') = collectDag r acc' seen' 372 node = NFork lh rh 373 h = nodeHash node 374 in if Set.member h seen'' then (h, acc'', seen'') else (h, (h, node) : acc'', Set.insert h seen'') 375 376 formatNode :: Map.Map MerkleHash Int -> Node -> (String, [Int]) 377 formatNode _ NLeaf = ("leaf", []) 378 formatNode idxMap (NStem ch) = ("stem", [idxMap Map.! ch]) 379 formatNode idxMap (NFork l r) = ("fork", [idxMap Map.! l, idxMap Map.! r])