ms2k/lazaret
SHA256
Watch
0
Code Releases 3 Activity

Bootstrap verified Rust implementation workspace

Browse source
This commit is contained in:
ms2k 2026-07-13 02:22:37 +09:00
commit b438dd5201
4 changed files with 1646 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

128
support/external-tools.toml Normal file
View file

@ -0,0 +1,128 @@
schema = 1
levels = ["V1", "V2", "V3", "V4", "V5"]
[[command]]
id = "python"
program = "python3"
args = ["--version"]
version_pattern = '^Python 3\.(1[1-9]|[2-9][0-9])\.'
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Python 3.11 or newer is required for repository verification."
[[command]]
id = "rustc"
program = "rustc"
args = ["--version"]
version_pattern = '^rustc 1\.90\.0 '
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install the pinned Rust toolchain from rust-toolchain.toml."
[[command]]
id = "cargo"
program = "cargo"
args = ["--version"]
version_pattern = '^cargo 1\.90\.0 '
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install the pinned Rust toolchain from rust-toolchain.toml."
[[command]]
id = "cargo-deny"
program = "cargo-deny"
args = ["--version"]
version_pattern = '^cargo-deny 0\.20\.2$'
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install cargo-deny 0.20.2 with its locked dependency graph."
[[command]]
id = "git"
program = "git"
args = ["--version"]
version_pattern = '^git version 2\.'
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Git 2.x is required for generated-file drift checks."
[[command]]
id = "tlc"
program = "tlc"
args = ["-h"]
version_pattern = 'Version 2\.19 '
accepted_exit_codes = [0, 1]
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install the TLC 2.19 launcher on PATH."
[[command]]
id = "runsc"
program = "runsc"
args = ["--version"]
version_pattern = '^runsc version release-20260622\.0\nspec: 1\.2\.1$'
policy = "skip"
levels = ["V3", "V4", "V5"]
diagnostic = "The selected composition is qualified on runsc release-20260622.0."
[[command]]
id = "fuse-overlayfs"
program = "fuse-overlayfs"
args = ["--version"]
version_pattern = '^fusermount3 version: 3\.18\.2\nfuse-overlayfs: version 1\.16\nFUSE library version 3\.18\.2\nusing FUSE kernel interface version 7\.45$'
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Install the qualified fuse-overlayfs 1.16 and FUSE 3.18.2 stack."
[[command]]
id = "slirp4netns"
program = "slirp4netns"
args = ["--version"]
version_pattern = '^slirp4netns version 1\.3\.1\ncommit: .+\nlibslirp: 4\.9\.1\nSLIRP_CONFIG_VERSION_MAX: 6\nlibseccomp: 2\.6\.0$'
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Install the qualified slirp4netns 1.3.1 and libslirp 4.9.1 stack."
[[feature]]
id = "linux-x86_64"
probe = "linux-x86_64"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Physical and composition suites currently support Linux x86_64."
[[feature]]
id = "kernel"
probe = "kernel-at-least"
minimum = "6.8"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Linux 6.8 or newer supplies the qualified namespace and pidfd baseline."
[[feature]]
id = "user-namespaces"
probe = "user-namespace"
program = "unshare"
sysctl_path = "/proc/sys/user/max_user_namespaces"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Enable functional unprivileged user namespace creation for physical runtime tests."
[[feature]]
id = "subordinate-ids"
probe = "subordinate-ids"
minimum_count = 65536
uidmap_program = "newuidmap"
gidmap_program = "newgidmap"
unshare_program = "unshare"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Configure usable 65,536-ID subordinate UID/GID ranges and mapping helpers for the current user."
[[feature]]
id = "fuse-device"
probe = "open-character-device"
path = "/dev/fuse"
access = "read-write"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Expose an openable read-write /dev/fuse device to run physical filesystem suites."

3
support/integration-tests.toml Normal file
View file

@ -0,0 +1,3 @@
schema = 1
levels = ["V2", "V3", "V4", "V5"]
scenarios = []

165
support/model-refinements.toml Normal file
View file

@ -0,0 +1,165 @@
schema = 1
[[model]]
name = "Lazaret"
module = "docs/protocol/Lazaret.tla"
config = "docs/protocol/Lazaret.cfg"
action_aggregates = ["Next", "DomainServiceProgress", "RuntimePhysicalInterleaving", "RequestProgress"]
[[model]]
name = "PreparedLower"
module = "docs/protocol/PreparedLower.tla"
config = "docs/protocol/PreparedLower.cfg"
action_aggregates = ["Next"]
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["StartNewDomain", "StartReadySession", "WaitForDomain", "RestartWaitingDomain", "AdvanceWaitingSession", "RejectConfigurationMismatch", "RegisterSession", "DisconnectSession"]
owners = ["IP-30", "IP-31"]
levels = ["V1", "V3"]
verifier = "Deterministic lifecycle adapters and the IP-40 cold-start slice"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["CreateTrustAnchor"]
owners = ["IP-23", "IP-30"]
levels = ["V2", "V3"]
verifier = "Credential/control physical tests and generation publication"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["StartRuntimeSupervisor", "LeasePreparedLower", "MountStateAnchor", "StartSidecar", "StartConnectivityHelper", "MarkNetworkReady", "ArmRuntimeCausalEdge", "StartSandbox", "PublishDomain"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-14", "IP-15", "IP-16", "IP-21", "IP-22", "IP-23", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Component tests, the IP-21 composition harness, and IP-40"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["BeginTeardown", "StopSandbox", "StopSidecar", "UnmountStateAnchor", "ReleasePreparedLowerLease", "GracefulSupervisorExit", "FinishTeardown"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Lifecycle adapters and IP-40 normal teardown"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["FailDomain", "HostCoordinatorTerminateUnresponsiveRuntime", "LeaseTeardownStopSandbox", "LeaseTeardownStopSidecar", "LeaseTeardownUnmountStateAnchor", "LeaseTeardownSupervisorExit", "ExternalReapStoppedSupervisorAfterHcLoss", "BootstrapRecoveryCoordinator", "BeginRecovery", "RecoverSandbox", "RecoverSidecar", "RecoverStateAnchor", "RecoverPreparedLowerLease", "FinishRecovery"]
owners = ["IP-21", "IP-22", "IP-32"]
levels = ["V2", "V4"]
verifier = "Causal-loss tests and the recovery failpoint matrix"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["HardLoseHostCoordinator", "HardLoseRuntimeSupervisor", "HardLoseAttachedRunsc", "HardLoseConnectivityHelper", "StopHostCoordinatorProcess", "ResumeHostCoordinatorProcess", "StopRuntimeSupervisorProcess", "ResumeRuntimeSupervisorProcess", "StopAttachedRunscProcess", "ResumeAttachedRunscProcess", "ObservePathMismatch", "RefusePathMismatchCleanup", "RefusePreparedLowerReclaim"]
owners = ["IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-32"]
levels = ["V2", "V4"]
verifier = "Physical mismatch, stop, loss, and hostile-failure cases"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["ReceiveEscalation", "AutoApprove", "QueuePrompt", "BeginPrompt", "DeveloperApprove", "DeveloperDeny", "StartHostExecution", "CompleteHostExecution", "TimeoutRequest", "CancelRequest", "FailHostExecution", "DeliverResult"]
owners = ["IP-15", "IP-24", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Protocol tests, the IP-43 slice, and hostile-loss cases"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["TypeOK", "DomainGenerationBounds", "RuntimeRoleIdentitySeparation", "GenerationScopedIdentitiesDistinct"]
owners = ["IP-01", "IP-10", "IP-14", "IP-15", "IP-30"]
levels = ["V1"]
verifier = "Type/property tests and lifecycle state assertions"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["ConfigurationConfinement", "SandboxNamespaceIsolation", "OrderedNetworkStartup", "NetworkReadyBeforePublish"]
owners = ["IP-02", "IP-14", "IP-16", "IP-20", "IP-21", "IP-22", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Builders/codecs, physical isolation, and IP-40/IP-41"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["PublishedDomainsReady", "DomainLockLifetime", "RuntimeCausalEdgeArmedBeforeSandbox", "RuntimeCausalEdgeOwnerPresent", "SandboxRunningImpliesCoordinatorPresent", "PublishedRuntimeAuthorityPresent", "SupervisorLeaseConsistency", "RuntimeResourceOwnership", "CoordinatorPhysicalConsistency", "HostCoordinatorRequiresDomainOwnership", "NoVanishPresentRuntime", "StateAnchorOwnership", "HelperUnderSupervisor"]
owners = ["IP-10", "IP-13", "IP-21", "IP-22", "IP-30", "IP-32"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Lifecycle adapters, causal harnesses, and IP-44"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["ExclusiveBootstrapOwnership", "TeardownNotJoinable", "RegisteredSessionsConnected", "AttachedSessionsValid", "TerminalIsolation"]
owners = ["IP-23", "IP-30", "IP-31", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3"]
verifier = "Control/session tests and IP-40/IP-42"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["AuthenticatedRequestsOnly", "RegisteredSessionIdentityUniqueness", "LiveRequestIdentityAuthorized", "DeveloperApprovalAuthenticated", "HostExecutionAuthorized", "AutoApprovalNoShell", "NoOrphanHostProcess", "ResultDeliveryStateConsistent"]
owners = ["IP-15", "IP-23", "IP-24", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Protocol tests, IP-43, and hostile-loss cases"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["OrderedLeaseTeardown", "DurableIntentBeforeSandboxReady", "DurableDecisionPublicationConsistent", "PathMismatchNotAdopted", "FailedDomainIsolation", "OrderedFailureRecovery", "MultiRoleDurableIntent", "PreparedLowerLeaseBeforeMount"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-30", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Transactional and failpoint tests plus IP-44"
[[coverage]]
model = "Lazaret"
kind = "property"
symbols = ["SessionEventuallyResolves", "RequestEventuallyResolves", "PromptEventuallyRestoresTerminal", "EmptyDomainEventuallyStops", "FailedDomainEventuallyRecovers"]
owners = ["IP-24", "IP-30", "IP-31", "IP-32", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Bounded progress tests, integrated slices, and TLC"
[[coverage]]
model = "Lazaret"
kind = "property"
symbols = ["LeaseLossUnmountRetainsPreparedLowerLease"]
owners = ["IP-10", "IP-11", "IP-13", "IP-21", "IP-30", "IP-32"]
levels = ["V2", "V4"]
verifier = "Lease-loss failpoints and TLC"
[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["BeginPrepare", "CreateOwnedStage", "PublishArtifact", "RecoverOwnedStage", "ObserveForeignStage", "RefuseForeignStage"]
owners = ["IP-12", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Preparer publication, ownership, and recovery tests"
[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["AcquireLease", "MountStateAnchor", "UnmountStateAnchor", "ReleaseLease"]
owners = ["IP-11", "IP-13", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Catalog and State Anchor lease lifecycle tests"
[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["RequestGC", "PublishReplacementDuringGC", "ReclaimArtifact"]
owners = ["IP-11", "IP-12", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Concurrent publication and exact-owned reclamation tests"
[[coverage]]
model = "PreparedLower"
kind = "invariant"
symbols = ["TypeOK", "LeaseBindingConsistent", "MountedGenerationLeased", "LeasedArtifactPublished", "GCExcludesLeases", "ReplacementOnlyDuringGC", "ForeignStagePreserved", "OwnedStageRequiresIntent"]
owners = ["IP-11", "IP-12", "IP-13", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Catalog/preparer concurrency and recovery tests plus TLC"

175
support/work-packages.toml Normal file
View file

@ -0,0 +1,175 @@
schema = 1
[[package]]
id = "IP-00"
title = "Repository scaffold and verification"
depends_on = []
levels = ["V1", "V2", "V3", "V4", "V5"]
[[package]]
id = "IP-01"
title = "Typed schema and protocol records"
depends_on = ["IP-00"]
levels = ["V1"]
[[package]]
id = "IP-02"
title = "Trusted-host configuration"
depends_on = ["IP-00", "IP-01"]
levels = ["V1", "V2"]
[[package]]
id = "IP-03"
title = "Linux primitives"
depends_on = ["IP-00", "IP-01"]
levels = ["V1", "V2"]
[[package]]
id = "IP-04"
title = "Ignored-workspace contract"
depends_on = ["IP-00"]
levels = ["V1", "V2", "V5"]
[[package]]
id = "IP-10"
title = "Domain Store"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-11"
title = "Storage Catalog"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-12"
title = "OCI transport and layer preparer"
depends_on = ["IP-02", "IP-03", "IP-11"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-13"
title = "State Anchor"
depends_on = ["IP-02", "IP-03", "IP-10", "IP-11", "IP-12"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-14"
title = "Derived network policy"
depends_on = ["IP-01", "IP-02"]
levels = ["V1"]
[[package]]
id = "IP-15"
title = "Protocol cryptography and codecs"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1", "V2"]
[[package]]
id = "IP-16"
title = "OCI specification and runsc command builder"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1"]
[[package]]
id = "IP-20"
title = "Ignored-workspace router and Git Sentry"
depends_on = ["IP-02", "IP-03", "IP-04", "IP-10"]
levels = ["V1", "V2", "V4", "V5"]
[[package]]
id = "IP-21"
title = "Runtime Supervisor and runsc ownership"
depends_on = ["IP-03", "IP-13", "IP-16"]
levels = ["V2", "V3", "V4"]
[[package]]
id = "IP-22"
title = "Network installation and connectivity helper"
depends_on = ["IP-03", "IP-10", "IP-14", "IP-21"]
levels = ["V2", "V3", "V4"]
[[package]]
id = "IP-23"
title = "Host-private control face"
depends_on = ["IP-02", "IP-10", "IP-15"]
levels = ["V1", "V2"]
[[package]]
id = "IP-24"
title = "Escalation mailbox and execution"
depends_on = ["IP-03", "IP-10", "IP-15", "IP-23"]
levels = ["V1", "V2", "V3", "V4"]
[[package]]
id = "IP-30"
title = "Core Host Coordinator lifecycle"
depends_on = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-14", "IP-15", "IP-16", "IP-21", "IP-22", "IP-23"]
levels = ["V1", "V2", "V3"]
[[package]]
id = "IP-31"
title = "Non-interactive Client CLI"
depends_on = ["IP-02", "IP-16", "IP-23", "IP-30"]
levels = ["V1", "V3"]
[[package]]
id = "IP-32"
title = "Recovery and prepared-artifact GC"
depends_on = ["IP-30", "IP-40"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-33"
title = "Session Terminal engine"
depends_on = ["IP-10", "IP-21", "IP-23", "IP-30", "IP-40"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-34"
title = "Interactive Client CLI"
depends_on = ["IP-31", "IP-33"]
levels = ["V1", "V3"]
[[package]]
id = "IP-35"
title = "State inspection and reset"
depends_on = ["IP-10", "IP-13", "IP-20", "IP-32"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-40"
title = "Minimal non-interactive runtime slice"
depends_on = ["IP-30", "IP-31"]
levels = ["V3"]
[[package]]
id = "IP-41"
title = "Workspace, Git, and persistence slice"
depends_on = ["IP-20", "IP-32", "IP-40"]
levels = ["V3", "V5"]
[[package]]
id = "IP-42"
title = "Interactive and multi-session slice"
depends_on = ["IP-33", "IP-34", "IP-40"]
levels = ["V3"]
[[package]]
id = "IP-43"
title = "Host-escalation slice"
depends_on = ["IP-24", "IP-34", "IP-42"]
levels = ["V3"]
[[package]]
id = "IP-44"
title = "Durability and hostile-failure gate"
depends_on = ["IP-32", "IP-35", "IP-40", "IP-41", "IP-42", "IP-43"]
levels = ["V4"]
[[package]]
id = "IP-45"
title = "Release qualification"
depends_on = ["IP-44"]
levels = ["V5"]