metadata verification

This commit is contained in:
AF 2022-09-11 16:26:58 +03:00
parent 6ea5be228c
commit 20434aa835
8 changed files with 41 additions and 9 deletions

View File

@ -46,7 +46,7 @@ class ActiveBinaryTree(
protocol,
NullableReference(
Null(),
BinaryTreeFactory(KeyMetadataFactory(factory, protocol.empty_metadata().factory))
BinaryTreeFactory(KeyMetadataFactory(factory, protocol.empty_metadata.factory))
)
)

View File

@ -1,6 +1,7 @@
from typing import Generic, Optional, TypeVar
from rainbowadn.atomic import *
from rainbowadn.collection.comparison import *
from rainbowadn.core import *
from .actions import *
from .core import *
@ -12,8 +13,8 @@ TreeType = TypeVar('TreeType')
class AVL(BinaryBalancing[ActiveKeyType, Integer, TreeType]):
def empty_metadata(self) -> HashPoint[Integer]:
return HashPoint.of(Integer(0))
def __init__(self, comparator_: Comparator[ActiveKeyType]):
super().__init__(comparator_, HashPoint.of(Integer(0)))
async def metadata(
self,

View File

@ -45,3 +45,9 @@ class BalancedCreation(
)
)
)
async def verify_metadata(
self, treel: TreeType, treer: TreeType, key: HashPoint[ActiveKeyType], metadata: HashPoint[MetaDataType]
) -> bool:
assert_true(await self.protocol.verify_metadata(treel, treer, key, metadata, self))
return True

View File

@ -13,22 +13,32 @@ MetaDataType = TypeVar('MetaDataType')
class BinaryBalancing(Generic[ActiveKeyType, MetaDataType, TreeType]):
def __init__(self, comparator_: Comparator[ActiveKeyType]):
def __init__(self, comparator_: Comparator[ActiveKeyType], empty_metadata: HashPoint[MetaDataType]):
assert isinstance(comparator_, Comparator)
assert isinstance(empty_metadata, HashPoint)
self.comparator = comparator_
def empty_metadata(self) -> HashPoint[MetaDataType]:
raise NotImplementedError
self.empty_metadata = empty_metadata
async def metadata(
self,
treel: TreeType,
treer: TreeType,
key: HashPoint[ActiveKeyType],
creation: BinaryCreation[ActiveKeyType, MetaDataType, TreeType]
creation: BinaryCreation[ActiveKeyType, MetaDataType, TreeType],
) -> HashPoint[MetaDataType]:
raise NotImplementedError
async def verify_metadata(
self,
treel: TreeType,
treer: TreeType,
key: HashPoint[ActiveKeyType],
metadata: HashPoint[MetaDataType],
creation: BinaryCreation[ActiveKeyType, MetaDataType, TreeType],
) -> bool:
assert_eq(await self.metadata(treel, treer, key, creation), metadata)
return True
async def balance(
self,
protocolized: BinaryProtocolized[ActiveKeyType, MetaDataType, TreeType],

View File

@ -24,3 +24,8 @@ class BinaryCreation(Generic[ActiveKeyType, MetaDataType, TreeType]):
async def tree(self, treel: TreeType, treer: TreeType, key: HashPoint[ActiveKeyType]) -> TreeType:
raise NotImplementedError
async def verify_metadata(
self, treel: TreeType, treer: TreeType, key: HashPoint[ActiveKeyType], metadata: HashPoint[MetaDataType]
) -> bool:
raise NotImplementedError

View File

@ -1,5 +1,6 @@
from typing import Generic, Optional, TypeVar
from rainbowadn.core import *
from .binarycreation import *
from .binaryprotocolized import *
from .binarysplit import *
@ -50,3 +51,11 @@ class ProtocolizedBinarySplit(
return None
else:
return ProtocolizedBinarySplit(protocolized.creation, split, protocolized.tree)
async def verify_metadata(self) -> bool:
assert_true(
await self.protocol.verify_metadata(
self.split.treel, self.split.treer, self.split.key, self.split.metadata
)
)
return True

View File

@ -176,6 +176,7 @@ class VerifySubsetAction(
assert_trues(
await gather(
self.on(case.protocolizedl()),
case.verify_metadata(),
self.on(case.protocolizedr()),
)
)

View File

@ -167,7 +167,7 @@ if __name__ == '__main__':
try:
asyncio.run(
trace(
preset_short
preset_long
)
)
except KeyboardInterrupt: