From c884995c90b8eec40461a1a24cfb3353a713265c Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 21:34:48 +0800 Subject: [PATCH 1/7] model: MN-REQ-05.5 session cap evicts least-recently-touched saveable session (proposed, not shipped) --- sysml-models/README.md | 4 +- sysml-models/models/behaviour.sysml | 36 ++++- sysml-models/models/deploy.sysml | 18 +++ sysml-models/models/requirements.sysml | 34 +++++ sysml-models/models/verify.sysml | 188 +++++++++++++++++++++++++ tests/test_sysml_session_evict.py | 130 +++++++++++++++++ 6 files changed, 407 insertions(+), 3 deletions(-) create mode 100644 tests/test_sysml_session_evict.py diff --git a/sysml-models/README.md b/sysml-models/README.md index 445fbe11..d5e1d49f 100644 --- a/sysml-models/README.md +++ b/sysml-models/README.md @@ -21,12 +21,12 @@ Design authority: rebuilt requirements + ADR-001 (GQL agent wire) + `docs/gramma | File | Package | Role | |------|---------|------| | `models/connections.sysml` | `MemNetConnections` | SharedLlmMemory, SessionHandoff (+ CallerId / SessionBind / SessionCapability), WorkingMemorySlice, SessionImportRequest, optional ImportGuardDecision; ServeUsageLook / ImportGuardArmedLook / HumanUsagePage (ops look); application `CompanyAnalyticalSsot` / `HostSearchBridge` / `DeviceMemNetFleet` / `TipMemNetAccess` / `MemNetLanMcpCluster` / `MemNetTwoMovesContrast` | -| `models/requirements.sysml` | `MemNetRequirements` | MN-REQ-00…13 (01.7/01.8, 06.4, **06.5** human usage look, **06.6** device services / one droplet MemNet MCP tip/ops, product face sysmledge, **06.7** SSOT → code allocate, **06.8** tip MemNet access portal, **06.9** ClusterRoute LAN MCP front invent #191, **06.10** SliceHandCarry invent #47 cousin, **06.12** product gateway on memnet-mcp, 12.9–12.13, 13.1 Recall/Commit; 02.9 cousin store-key; 04.8 cue \|Q\|>1; 04.9 empty-q outline) | +| `models/requirements.sysml` | `MemNetRequirements` | MN-REQ-00…13 (01.7/01.8, 06.4, **06.5** human usage look, **06.6** device services / one droplet MemNet MCP tip/ops, product face sysmledge, **06.7** SSOT → code allocate, **06.8** tip MemNet access portal, **06.9** ClusterRoute LAN MCP front invent #191, **06.10** SliceHandCarry invent #47 cousin, **05.5** session cap LRU evict (proposed, not shipped), **06.12** product gateway on memnet-mcp, 12.9–12.13, 13.1 Recall/Commit; 02.9 cousin store-key; 04.8 cue \|Q\|>1; 04.9 empty-q outline) | | `models/cousins.sysml` | `MemNetCousinContrast` | TARGET vs eight cousin pointing/identity designs (not a product switch; SysMLEdge is a distinct pin_map; overlay family `SysMLEdgePrj-*`; this engine repo and `modelbasedPrj-*` are repo-based — MUST NOT use SysMLEdge as model SSOT; `SysMLEdgePrj-*` bound desk is working model SSOT) | | `models/deploy.sysml` | `MemNet` | Nested parts; `RecallCommit` two-operator cut; Multitask spine; `MemNetUsageDashboard` / `MemNetOpsFleet` / `TipMemNetAccessPortal` / `MemNetLanMcpFront` / `MemNetProductGateway` / `MemNetTwoMoves` outside `MemNetSystem` | | `models/implementation.sysml` | `MemNetImplementation` | `SoftwareAllocate` logical → live modules; one Hatch wheel many hosts; sysmledge not in wheel | | `models/behaviour.sysml` | `MemNetBehaviour` | HandoffById, SessionImportReceive, Multitask async, landed-client hydrate/flush | -| `models/verify.sysml` | `MemNetVerification` | MN-VER-12-G00 + S01…S14; MN-VER-04-S01…S05; MN-VER-09-S01; MN-VER-13-S01; MN-VER-06-S01…S10 (S06 storage roles; S07 ClusterRoute LAN MCP front; S08 two named moves; S09 admin usage; S10 product gateway); MN-VER-01-S03 | +| `models/verify.sysml` | `MemNetVerification` | MN-VER-12-G00 + S01…S14; MN-VER-04-S01…S05; MN-VER-09-S01; MN-VER-13-S01; MN-VER-05-S03…S09 (MN-REQ-05.5 session cap LRU evict, proposed); MN-VER-06-S01…S10 (S06 storage roles; S07 ClusterRoute LAN MCP front; S08 two named moves; S09 admin usage; S10 product gateway); MN-VER-01-S03 | | `models/root.sysml` | `ProjectMemNet` | Root imports (load last). MUST NOT import `MemNetArchive` | | `models/archive.sysml` | `MemNetArchive` | ARCHIVE shelf (leftover_* / TierACodec / LegacyPipe* / retired Neo4j). **Off** `config.yaml` load | diff --git a/sysml-models/models/behaviour.sysml b/sysml-models/models/behaviour.sysml index f1b0aa56..5e91ccdf 100644 --- a/sysml-models/models/behaviour.sysml +++ b/sysml-models/models/behaviour.sysml @@ -100,6 +100,14 @@ package MemNetBehaviour { File stays until the user deletes it. Not Neo4j. */ } + attribute def EvEvictForCap { + doc /* + MN-REQ-05.5 (proposed, not shipped): session cap full on open or + load, after purge_expired; this live session is the oldest-touched + saveable victim. Save first, then drop from RAM. Unsaveable victims + are skipped (EvError) and stay live. + */ + } attribute def EvCloseOrExpire { doc /* session_close or TTL purge after optional expire save. */ } @@ -328,7 +336,11 @@ package MemNetBehaviour { then closed; state closed { - doc /* No session id; open or load required. */ + doc /* + No session id; open or load required. An evicted session (MN-REQ-05.5) + returns here; closed_to_loading via EvLoadSnapshot restores it from + its snapshot with the same ACL and lease. + */ } transition closed_to_opening first closed @@ -433,6 +445,28 @@ package MemNetBehaviour { first expireSaving accept EvCloseOrExpire then closed; + + state evictSaving { + doc /* + MN-REQ-05.5 (proposed): cap eviction of the oldest-touched saveable + session. Write its snapshot first (fsync, atomic 0600, @SNAP v2); + save ok drops RAM to closed, save failure keeps the session active. + Never entered for the session being opened or loaded, or for a + session holding an active write lock. + */ + } + transition active_to_evict_saving + first active + accept EvEvictForCap + then evictSaving; + transition evict_saving_to_closed + first evictSaving + accept EvCloseOrExpire + then closed; + transition evict_saving_to_active + first evictSaving + accept EvError + then active; } // --- 2. Goldfish loop (engine side of turn) --- diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index b175ba58..bd3adf67 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -156,6 +156,20 @@ package MemNet { attribute maxLaw : Integer = 100; attribute maxRelations : Integer = 200; attribute maxSessions : Integer = 1024; + // MN-REQ-05.5 session cap LRU evict: proposed design flags, not shipped. + attribute evictOnSessionCap : Boolean = true; + attribute envMaxSessions : String = "MEMNET_MAX_SESSIONS"; + attribute evictPicksOldestTouch : Boolean = true; + attribute evictTouchOnReadOrWrite : Boolean = true; + attribute evictSavesFirstFsync : Boolean = true; + attribute evictSkipsUnsaveable : Boolean = true; + attribute evictRefusesWhenNoneEvictable : Boolean = true; + attribute evictNeverSelf : Boolean = true; + attribute evictNeverWriteLocked : Boolean = true; + attribute evictReportsNameNotId : Boolean = true; + attribute evictLoadRestores : Boolean = true; + attribute evictKeepsAclLease : Boolean = true; + attribute evictShipped : Boolean = false; attribute maxDepth : Integer = 4; attribute defaultQueryMaxRows : Integer = 50; attribute defaultQueryDepth : Integer = 2; @@ -185,6 +199,7 @@ package MemNet { satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_2_QueryFanoutCaps; satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_3_ConsistentValueByteCap; satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_4_ConsistentFieldCap; + satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru; satisfy MN_REQ_00_MissionBridge::MN_REQ_01_SessionLifecycle::MN_REQ_01_10_SessionLifecycleAclWho; satisfy MN_REQ_00_MissionBridge::MN_REQ_10_LlmPropertiesAndLimits::MN_REQ_10_2_PinMapMustFitContext; satisfy MN_REQ_00_MissionBridge::MN_REQ_12_MultitaskMode::MN_REQ_12_7_NoAssumeAclReserveIngest; @@ -3165,11 +3180,14 @@ package MemNet { (save_on_expire, expire_snapshot_dir_set) and the count of sessions held because expire-save failed (expire_snapshot_failed). Path redacted. Look only. + MN-REQ-05.5 (proposed): sessions_evicted counter for cap evictions; + the evicted session is named by name or tag, never a real mn_ id. */ attribute lookOnly : Boolean = true; attribute saveOnExpireFlag : Boolean = true; attribute expireSnapshotDirSetFlag : Boolean = true; attribute expireSnapshotFailedCount : Boolean = true; + attribute sessionsEvictedCounter : Boolean = true; attribute pathRedacted : Boolean = true; } diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index 4edb6a25..31c6b80e 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -34,6 +34,7 @@ MN-REQ-03.4 MATCH WHERE SET/DELETE SHALL honour the predicate or refuse MN-REQ-05.3 One decoded value_bytes cap on pipe mutate, GQL mutate, snapshot load MN-REQ-05.4 One effective-field cap (default 64) on SCHEMA register, mutate, snapshot save/load; save never stricter than write + MN-REQ-05.5 Session cap evicts least-recently-touched saveable session (proposed, not shipped); save victim first; none evictable keeps limit_exceeded|sessions refusal MN-REQ-06.11 Admin-only serve usage report (counts/caps; opaque session alias; not agent MCP) MN-REQ-06.12 Product gateway on memnet-mcp: per-product route to owning serve (not mn_tip_) MN-REQ-06.13 Serve request isolation: each command's stdout, stderr, and exit_code @@ -762,6 +763,29 @@ package MemNetRequirements { */ attribute requirementId : String = "MN-REQ-05.4"; } + + requirement def MN_REQ_05_5_SessionCapEvictLru { + doc /* + Proposed, not shipped. When the session cap (MEMNET_MAX_SESSIONS, + default 1024) is reached on session open or load, after + purge_expired, the engine SHALL evict the live session with the + oldest last-touch time; any read or write counts as a touch. + Before the RAM drop the victim SHALL be saved to its snapshot + first (fsync, atomic 0600 write, @SNAP version 2 with the ACL + and lease digest kept). An unsaveable victim (snapshot_unsaveable, + over cap, or no snapshot dir) SHALL be skipped, stay in RAM, and + the next-oldest SHALL be tried. If no session is evictable the + limit_exceeded|sessions n/cap refusal SHALL stand and nothing + SHALL be dropped. The session being opened or loaded SHALL NOT be + evicted, nor any session holding an active write lock (RSV lease + or in-flight commit). The result SHALL report the evicted session + by name or tag only, never a real mn_ id; serve_status SHALL carry + a sessions_evicted counter. A later session_load SHALL restore the + evicted session from its snapshot with the same ACL and lease. + Verify: MN-VER-05-S03 to MN-VER-05-S09. + */ + attribute requirementId : String = "MN-REQ-05.5"; + } } // ----- Process / transport boundary ----- @@ -2311,6 +2335,8 @@ package MemNetRequirements { : MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_3_ConsistentValueByteCap; requirement consistentFieldCapReq : MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_4_ConsistentFieldCap; + requirement sessionCapEvictLruReq + : MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru; requirement processBoundaryReq : MN_REQ_00_MissionBridge::MN_REQ_06_ProcessBoundary; @@ -2569,6 +2595,14 @@ package MemNetRequirements { end #derive ::> queryFanoutCapsReq; end #derive ::> consistentValueByteCapReq; end #derive ::> consistentFieldCapReq; + end #derive ::> sessionCapEvictLruReq; + } + + #derivation connection deriveSessionCapEvictFromCapsAndSnapshot { + end #original ::> sessionTtlAndCapsReq; + end #original ::> snapshotLosslessRoundTripReq; + end #original ::> snapshotAclReq; + end #derive ::> sessionCapEvictLruReq; } #derivation connection deriveProcessBoundaryLeaves { diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index 4dcc39f5..b78a0b28 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -54,6 +54,11 @@ TcpServeBridge; admin drain; manifest; startup restore; retire after a clean restore; no client retry; no silent session loss; no SemVer bump. + Session cap LRU evict (MN-VER-05-S03..S09, proposed, not shipped): + MN-REQ-05.5 — oldest-touch pick; save first then drop; skip + unsaveable; none evictable refuses limit_exceeded|sessions; self and + write-locked exempt; name not mn_ id plus serve_status counter; + later load restores with ACL and lease (@SNAP v2). Serve checkpoint (MN-VER-06-S13): ServeCheckpoint on TcpServeBridge; admin credential; per-session lock; lossless atomic snaps; skip unsaveable; no drain; no live load; no @@ -2315,6 +2320,175 @@ package MemNetVerification { } } + verification def MN_VER_05_S03_SessionCapEvictOldestTouch { + doc /* + MN-REQ-05.5 R1 (proposed, not shipped) — at MEMNET_MAX_SESSIONS + (default 1024) on open or load, after purge_expired, evict the live + session with the oldest last-touch time; any read or write is a + touch. Knob MEMNET_MAX_SESSIONS. + */ + attribute verificationId : String = "MN-VER-05-S03"; + + subject system : MemNetSystem; + + objective sessionCapEvictOldestTouch { + verify sessionCapEvictLruReq; + verify sessionTtlAndCapsReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictOnSessionCap == true + and system.core.transport.inProcess.memory.sessions.caps + .envMaxSessions == "MEMNET_MAX_SESSIONS" + and system.core.transport.inProcess.memory.sessions.caps + .evictPicksOldestTouch == true + and system.core.transport.inProcess.memory.sessions.caps + .evictTouchOnReadOrWrite == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + + verification def MN_VER_05_S04_SessionCapEvictSaveFirst { + doc /* + MN-REQ-05.5 R2 (proposed) — the victim is saved to its snapshot first + (fsync, atomic 0600, @SNAP v2 with ACL and lease digest kept), then + dropped from RAM. A failed save never drops RAM. + */ + attribute verificationId : String = "MN-VER-05-S04"; + + subject system : MemNetSystem; + + objective sessionCapEvictSaveFirst { + verify sessionCapEvictLruReq; + verify saveSessionSnapshotReq; + verify snapshotLosslessRoundTripReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictSavesFirstFsync == true + and system.core.transport.inProcess.memory.sessions.caps + .evictKeepsAclLease == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + + verification def MN_VER_05_S05_SessionCapEvictSkipUnsaveable { + doc /* + MN-REQ-05.5 R3 (proposed) — an unsaveable victim (snapshot_unsaveable, + over cap, or no snapshot dir) is skipped, stays in RAM, and the + next-oldest session is tried. + */ + attribute verificationId : String = "MN-VER-05-S05"; + + subject system : MemNetSystem; + + objective sessionCapEvictSkipUnsaveable { + verify sessionCapEvictLruReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictSkipsUnsaveable == true + and system.core.transport.inProcess.memory.sessions.caps + .evictPicksOldestTouch == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + + verification def MN_VER_05_S06_SessionCapEvictNoneEvictable { + doc /* + MN-REQ-05.5 R4 (proposed) — cap full and every candidate unsaveable, + so refuse with limit_exceeded|sessions n/cap as today; nothing is + dropped. + */ + attribute verificationId : String = "MN-VER-05-S06"; + + subject system : MemNetSystem; + + objective sessionCapEvictNoneEvictable { + verify sessionCapEvictLruReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictRefusesWhenNoneEvictable == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + + verification def MN_VER_05_S07_SessionCapEvictExemptSelfAndLocked { + doc /* + MN-REQ-05.5 R5 (proposed) — the session being opened or loaded is + never evicted, nor is a session holding an active write lock (RSV + lease or in-flight commit). + */ + attribute verificationId : String = "MN-VER-05-S07"; + + subject system : MemNetSystem; + + objective sessionCapEvictExemptSelfAndLocked { + verify sessionCapEvictLruReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictNeverSelf == true + and system.core.transport.inProcess.memory.sessions.caps + .evictNeverWriteLocked == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + + verification def MN_VER_05_S08_SessionCapEvictReportNameNotId { + doc /* + MN-REQ-05.5 R6 (proposed) — the eviction result reports the evicted + session by name or tag only, never a real mn_ id. serve_status carries + the sessions_evicted counter (ServeStatusLook.sessionsEvictedCounter + on MemNetUsageDashboard, outside MemNetSystem; a verification has one + subject, so the counter is checked by its deploy attribute, not here). + */ + attribute verificationId : String = "MN-VER-05-S08"; + + subject system : MemNetSystem; + + objective sessionCapEvictReportNameNotId { + verify sessionCapEvictLruReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictReportsNameNotId == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + + verification def MN_VER_05_S09_SessionCapEvictLoadRestores { + doc /* + MN-REQ-05.5 R7 (proposed) — a later session_load restores the evicted + session from its snapshot with the same ACL and lease (@SNAP v2, digest + only; MN-REQ-06.16). + */ + attribute verificationId : String = "MN-VER-05-S09"; + + subject system : MemNetSystem; + + objective sessionCapEvictLoadRestores { + verify sessionCapEvictLruReq; + verify loadSessionSnapshotReq; + verify snapshotAclReq; + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .evictLoadRestores == true + and system.core.transport.inProcess.memory.sessions.caps + .evictKeepsAclLease == true + and system.core.transport.inProcess.memory.sessions.caps + .evictShipped == false + } + } + } + verification def MN_VER_06_S06_StorageRoles { doc /* storageRole only where bytes outlive the call: working_memory, @@ -2414,6 +2588,20 @@ package MemNetVerification { : MN_VER_05_S01_ConsistentValueByteCap; verification consistentFieldCapVerify : MN_VER_05_S02_ConsistentFieldCap; + verification sessionCapEvictOldestTouchVerify + : MN_VER_05_S03_SessionCapEvictOldestTouch; + verification sessionCapEvictSaveFirstVerify + : MN_VER_05_S04_SessionCapEvictSaveFirst; + verification sessionCapEvictSkipUnsaveableVerify + : MN_VER_05_S05_SessionCapEvictSkipUnsaveable; + verification sessionCapEvictNoneEvictableVerify + : MN_VER_05_S06_SessionCapEvictNoneEvictable; + verification sessionCapEvictExemptSelfAndLockedVerify + : MN_VER_05_S07_SessionCapEvictExemptSelfAndLocked; + verification sessionCapEvictReportNameNotIdVerify + : MN_VER_05_S08_SessionCapEvictReportNameNotId; + verification sessionCapEvictLoadRestoresVerify + : MN_VER_05_S09_SessionCapEvictLoadRestores; verification storageRolesVerify : MN_VER_06_S06_StorageRoles; verification lanMcpFrontSeveralServesVerify : MN_VER_06_S07_LanMcpFrontSeveralServes; diff --git a/tests/test_sysml_session_evict.py b/tests/test_sysml_session_evict.py new file mode 100644 index 00000000..075d7670 --- /dev/null +++ b/tests/test_sysml_session_evict.py @@ -0,0 +1,130 @@ +"""MN-REQ-05.5 session cap LRU evict: SysML text checks (proposed, not shipped).""" + +from __future__ import annotations + +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +MODELS = ROOT / "sysml-models" / "models" +README = ROOT / "sysml-models" / "README.md" +DEPLOY = MODELS / "deploy.sysml" +REQ = MODELS / "requirements.sysml" +VERIFY = MODELS / "verify.sysml" +BEHAVIOUR = MODELS / "behaviour.sysml" + + +def _read(path: Path) -> str: + return path.read_text(encoding="utf-8") + + +def test_mn_req_05_5_requirement_def_and_usage(): + text = _read(REQ) + assert "MN-REQ-05.5 Session cap evicts least-recently-touched" in text + assert "requirement def MN_REQ_05_5_SessionCapEvictLru {" in text + assert 'attribute requirementId : String = "MN-REQ-05.5";' in text + assert "requirement sessionCapEvictLruReq" in text + assert "MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru;" in text + assert "end #derive ::> sessionCapEvictLruReq;" in text + + +def test_mn_req_05_5_rules_in_doc(): + text = _read(REQ) + start = text.index("requirement def MN_REQ_05_5_SessionCapEvictLru {") + body = text[start : text.index('attribute requirementId : String = "MN-REQ-05.5";', start)] + assert "MEMNET_MAX_SESSIONS" in body + assert "oldest last-touch time" in body + assert "fsync" in body + assert "@SNAP version 2" in body + assert "snapshot_unsaveable" in body + assert "limit_exceeded|sessions n/cap" in body + assert "active write lock" in body + assert "sessions_evicted" in body + assert "later session_load SHALL restore" in body + assert "MN-VER-05-S03 to MN-VER-05-S09" in body + + +def test_mn_req_05_5_derivation_links(): + text = _read(REQ) + assert "end #original ::> sessionTtlAndCapsReq;" in text + assert "end #original ::> snapshotLosslessRoundTripReq;" in text + assert "end #original ::> snapshotAclReq;" in text + assert "#derivation connection deriveSessionCapEvictFromCapsAndSnapshot" in text + + +def test_deploy_caps_evict_flags(): + text = _read(DEPLOY) + assert "attribute maxSessions : Integer = 1024;" in text + assert "attribute evictOnSessionCap : Boolean = true;" in text + assert 'attribute envMaxSessions : String = "MEMNET_MAX_SESSIONS";' in text + assert "attribute evictPicksOldestTouch : Boolean = true;" in text + assert "attribute evictTouchOnReadOrWrite : Boolean = true;" in text + assert "attribute evictSavesFirstFsync : Boolean = true;" in text + assert "attribute evictSkipsUnsaveable : Boolean = true;" in text + assert "attribute evictRefusesWhenNoneEvictable : Boolean = true;" in text + assert "attribute evictNeverSelf : Boolean = true;" in text + assert "attribute evictNeverWriteLocked : Boolean = true;" in text + assert "attribute evictReportsNameNotId : Boolean = true;" in text + assert "attribute evictLoadRestores : Boolean = true;" in text + assert "attribute evictKeepsAclLease : Boolean = true;" in text + assert "attribute evictShipped : Boolean = false;" in text + assert "satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru;" in text + + +def test_serve_status_sessions_evicted_counter(): + text = _read(DEPLOY) + start = text.index("part def ServeStatusLook {") + body = text[start : text.index("part def SessionCensusLook {", start)] + assert "attribute sessionsEvictedCounter : Boolean = true;" in body + + +def test_behaviour_evict_saving_state(): + text = _read(BEHAVIOUR) + assert "attribute def EvEvictForCap" in text + assert "state evictSaving" in text + assert "accept EvEvictForCap" in text + assert "then evictSaving;" in text + assert "transition evict_saving_to_closed" in text + assert "transition evict_saving_to_active" in text + assert "An evicted session (MN-REQ-05.5)" in text + assert "closed_to_loading via EvLoadSnapshot restores it" in text + + +def test_verify_mn_ver_05_s03_to_s09_defs_and_usages(): + text = _read(VERIFY) + defs = [ + ("MN_VER_05_S03_SessionCapEvictOldestTouch", "MN-VER-05-S03", "sessionCapEvictOldestTouchVerify"), + ("MN_VER_05_S04_SessionCapEvictSaveFirst", "MN-VER-05-S04", "sessionCapEvictSaveFirstVerify"), + ("MN_VER_05_S05_SessionCapEvictSkipUnsaveable", "MN-VER-05-S05", "sessionCapEvictSkipUnsaveableVerify"), + ("MN_VER_05_S06_SessionCapEvictNoneEvictable", "MN-VER-05-S06", "sessionCapEvictNoneEvictableVerify"), + ( + "MN_VER_05_S07_SessionCapEvictExemptSelfAndLocked", + "MN-VER-05-S07", + "sessionCapEvictExemptSelfAndLockedVerify", + ), + ("MN_VER_05_S08_SessionCapEvictReportNameNotId", "MN-VER-05-S08", "sessionCapEvictReportNameNotIdVerify"), + ("MN_VER_05_S09_SessionCapEvictLoadRestores", "MN-VER-05-S09", "sessionCapEvictLoadRestoresVerify"), + ] + for def_name, ver_id, usage in defs: + assert f"verification def {def_name} {{" in text + assert f'attribute verificationId : String = "{ver_id}";' in text + assert f"verification {usage}" in text + assert f" : {def_name};" in text + assert "verify sessionCapEvictLruReq;" in text + assert "verify snapshotAclReq;" in text + assert "verify loadSessionSnapshotReq;" in text + + +def test_verify_05_5_constraints_use_caps_paths(): + text = _read(VERIFY) + start = text.index("verification def MN_VER_05_S03_SessionCapEvictOldestTouch {") + end = text.index("verification def MN_VER_06_S06_StorageRoles {", start) + block = text[start:end] + assert block.count("system.core.transport.inProcess.memory.sessions.caps") >= 7 + assert ".envMaxSessions == \"MEMNET_MAX_SESSIONS\"" in block + assert block.count(".evictShipped == false") == 7 + + +def test_readme_lists_05_5(): + text = _read(README) + assert "**05.5** session cap LRU evict (proposed, not shipped)" in text + assert "MN-VER-05-S03…S09 (MN-REQ-05.5 session cap LRU evict, proposed)" in text From 38ba83ac367a44c5294cb7f355968c33cdb8d996 Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 21:54:46 +0800 Subject: [PATCH 2/7] model: MN-REQ-05.5 review fixes B1-B5, settled answers, runtime xfail tests --- sysml-models/README.md | 4 +- sysml-models/models/behaviour.sysml | 20 +- sysml-models/models/deploy.sysml | 47 ++- sysml-models/models/requirements.sysml | 94 ++++- sysml-models/models/verify.sysml | 140 ++++--- tests/test_session_evict.py | 505 +++++++++++++++++++++++++ tests/test_sysml_session_evict.py | 181 +++++---- 7 files changed, 802 insertions(+), 189 deletions(-) create mode 100644 tests/test_session_evict.py diff --git a/sysml-models/README.md b/sysml-models/README.md index d5e1d49f..06a9cc09 100644 --- a/sysml-models/README.md +++ b/sysml-models/README.md @@ -21,12 +21,12 @@ Design authority: rebuilt requirements + ADR-001 (GQL agent wire) + `docs/gramma | File | Package | Role | |------|---------|------| | `models/connections.sysml` | `MemNetConnections` | SharedLlmMemory, SessionHandoff (+ CallerId / SessionBind / SessionCapability), WorkingMemorySlice, SessionImportRequest, optional ImportGuardDecision; ServeUsageLook / ImportGuardArmedLook / HumanUsagePage (ops look); application `CompanyAnalyticalSsot` / `HostSearchBridge` / `DeviceMemNetFleet` / `TipMemNetAccess` / `MemNetLanMcpCluster` / `MemNetTwoMovesContrast` | -| `models/requirements.sysml` | `MemNetRequirements` | MN-REQ-00…13 (01.7/01.8, 06.4, **06.5** human usage look, **06.6** device services / one droplet MemNet MCP tip/ops, product face sysmledge, **06.7** SSOT → code allocate, **06.8** tip MemNet access portal, **06.9** ClusterRoute LAN MCP front invent #191, **06.10** SliceHandCarry invent #47 cousin, **05.5** session cap LRU evict (proposed, not shipped), **06.12** product gateway on memnet-mcp, 12.9–12.13, 13.1 Recall/Commit; 02.9 cousin store-key; 04.8 cue \|Q\|>1; 04.9 empty-q outline) | +| `models/requirements.sysml` | `MemNetRequirements` | MN-REQ-00…13 (01.7/01.8, 06.4, **06.5** human usage look, **06.6** device services / one droplet MemNet MCP tip/ops, product face sysmledge, **06.7** SSOT → code allocate, **06.8** tip MemNet access portal, **06.9** ClusterRoute LAN MCP front invent #191, **06.10** SliceHandCarry invent #47 cousin, **05.5** session cap LRU evict (proposed, not shipped; restore: same ACL, no lease carried over), **06.12** product gateway on memnet-mcp, 12.9–12.13, 13.1 Recall/Commit; 02.9 cousin store-key; 04.8 cue \|Q\|>1; 04.9 empty-q outline) | | `models/cousins.sysml` | `MemNetCousinContrast` | TARGET vs eight cousin pointing/identity designs (not a product switch; SysMLEdge is a distinct pin_map; overlay family `SysMLEdgePrj-*`; this engine repo and `modelbasedPrj-*` are repo-based — MUST NOT use SysMLEdge as model SSOT; `SysMLEdgePrj-*` bound desk is working model SSOT) | | `models/deploy.sysml` | `MemNet` | Nested parts; `RecallCommit` two-operator cut; Multitask spine; `MemNetUsageDashboard` / `MemNetOpsFleet` / `TipMemNetAccessPortal` / `MemNetLanMcpFront` / `MemNetProductGateway` / `MemNetTwoMoves` outside `MemNetSystem` | | `models/implementation.sysml` | `MemNetImplementation` | `SoftwareAllocate` logical → live modules; one Hatch wheel many hosts; sysmledge not in wheel | | `models/behaviour.sysml` | `MemNetBehaviour` | HandoffById, SessionImportReceive, Multitask async, landed-client hydrate/flush | -| `models/verify.sysml` | `MemNetVerification` | MN-VER-12-G00 + S01…S14; MN-VER-04-S01…S05; MN-VER-09-S01; MN-VER-13-S01; MN-VER-05-S03…S09 (MN-REQ-05.5 session cap LRU evict, proposed); MN-VER-06-S01…S10 (S06 storage roles; S07 ClusterRoute LAN MCP front; S08 two named moves; S09 admin usage; S10 product gateway); MN-VER-01-S03 | +| `models/verify.sysml` | `MemNetVerification` | MN-VER-12-G00 + S01…S14; MN-VER-04-S01…S05; MN-VER-09-S01; MN-VER-13-S01; MN-VER-05-S03…S09 (MN-REQ-05.5 session cap LRU evict, proposed; runtime checks in `tests/test_session_evict.py`, xfail until shipped); MN-VER-06-S01…S10 (S06 storage roles; S07 ClusterRoute LAN MCP front; S08 two named moves; S09 admin usage; S10 product gateway); MN-VER-01-S03 | | `models/root.sysml` | `ProjectMemNet` | Root imports (load last). MUST NOT import `MemNetArchive` | | `models/archive.sysml` | `MemNetArchive` | ARCHIVE shelf (leftover_* / TierACodec / LegacyPipe* / retired Neo4j). **Off** `config.yaml` load | diff --git a/sysml-models/models/behaviour.sysml b/sysml-models/models/behaviour.sysml index 5e91ccdf..d0cd81a8 100644 --- a/sysml-models/models/behaviour.sysml +++ b/sysml-models/models/behaviour.sysml @@ -104,8 +104,15 @@ package MemNetBehaviour { doc /* MN-REQ-05.5 (proposed, not shipped): session cap full on open or load, after purge_expired; this live session is the oldest-touched - saveable victim. Save first, then drop from RAM. Unsaveable victims - are skipped (EvError) and stay live. + evictable victim. The victim lock is taken at pick and held through + save, drop and registry removal. Save first, then drop from RAM. + */ + } + attribute def EvEvictSaved { + doc /* + MN-REQ-05.5 (proposed, not shipped): the victim's snapshot is complete + (temp file, fsync, rename, fsync dir). Only this event drops the victim + from RAM. Runtime check: tests/test_session_evict.py. */ } attribute def EvCloseOrExpire { @@ -339,7 +346,7 @@ package MemNetBehaviour { doc /* No session id; open or load required. An evicted session (MN-REQ-05.5) returns here; closed_to_loading via EvLoadSnapshot restores it from - its snapshot with the same ACL and lease. + its snapshot: same ACL, no lease carried over. */ } transition closed_to_opening @@ -452,7 +459,10 @@ package MemNetBehaviour { session. Write its snapshot first (fsync, atomic 0600, @SNAP v2); save ok drops RAM to closed, save failure keeps the session active. Never entered for the session being opened or loaded, or for a - session holding an active write lock. + session holding an active write lock or an open bind. The victim is + marked evicting under the cap lock; its victim lock is held from pick + through save, drop and registry removal. Save runs outside the cap lock. + Atomic write: temp file in the same dir, fsync file, rename, fsync dir. */ } transition active_to_evict_saving @@ -461,7 +471,7 @@ package MemNetBehaviour { then evictSaving; transition evict_saving_to_closed first evictSaving - accept EvCloseOrExpire + accept EvEvictSaved then closed; transition evict_saving_to_active first evictSaving diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index bd3adf67..3a2ffad0 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -156,20 +156,32 @@ package MemNet { attribute maxLaw : Integer = 100; attribute maxRelations : Integer = 200; attribute maxSessions : Integer = 1024; - // MN-REQ-05.5 session cap LRU evict: proposed design flags, not shipped. - attribute evictOnSessionCap : Boolean = true; - attribute envMaxSessions : String = "MEMNET_MAX_SESSIONS"; - attribute evictPicksOldestTouch : Boolean = true; - attribute evictTouchOnReadOrWrite : Boolean = true; - attribute evictSavesFirstFsync : Boolean = true; - attribute evictSkipsUnsaveable : Boolean = true; - attribute evictRefusesWhenNoneEvictable : Boolean = true; - attribute evictNeverSelf : Boolean = true; - attribute evictNeverWriteLocked : Boolean = true; - attribute evictReportsNameNotId : Boolean = true; - attribute evictLoadRestores : Boolean = true; - attribute evictKeepsAclLease : Boolean = true; + // MN-REQ-05.5 session cap LRU evict: proposed, not shipped (engine pending). + // Each flag is a spec record; its runtime check is the pytest on the same + // line in tests/test_session_evict.py (xfail until the engine ships). attribute evictShipped : Boolean = false; + attribute evictOnSessionCap : Boolean = true; // test_evicts_oldest_touched_first + attribute envMaxSessions : String = "MEMNET_MAX_SESSIONS"; + attribute envSnapshotDir : String = "MEMNET_EVICT_SNAPSHOT_DIR"; + attribute evictSnapshotDirDefault : String = "unset"; // test_no_snapshot_dir_refuses_without_eviction + attribute evictPicksOldestTouch : Boolean = true; // test_evicts_oldest_touched_first + attribute evictTouchOnReadOrWrite : Boolean = true; // test_reads_and_writes_are_touches + attribute evictAdminReadsNotTouch : Boolean = true; // test_admin_and_serve_status_reads_are_not_touches + attribute evictSavesFirstFsync : Boolean = true; // test_victim_saved_before_drop_atomic_fsync + attribute evictVictimLockHeld : Boolean = true; // test_victim_lock_held_from_pick_through_drop + attribute evictOneCapLock : Boolean = true; // test_cap_two_concurrent_opens_one_victim_per_slot + attribute evictSkipsUnsaveable : Boolean = true; // test_unsaveable_victim_skipped_next_oldest_tried + attribute evictUnsaveableNotAutoDropped : Boolean = true; // test_unsaveable_held_counted_on_serve_status + attribute evictRefusesWhenNoneEvictable : Boolean = true; // test_all_in_use_refusal_drops_nothing + attribute evictNeverSelf : Boolean = true; // test_session_being_loaded_is_not_evicted + attribute evictNeverWriteLocked : Boolean = true; // test_write_locked_session_exempt + attribute evictNeverOpenBind : Boolean = true; // test_open_bind_exempt + attribute evictCallerNoEvictionField : Boolean = true; // test_caller_result_has_no_eviction_field + attribute evictReportAdminOnlyNameNotId : Boolean = true; // test_admin_report_names_victim_never_mn_id + attribute evictLoadRestores : Boolean = true; // test_restore_keeps_rows_edges_and_acl + attribute evictReopenRestoredTrue : Boolean = true; // test_reopen_restored_true_no_alerts + attribute evictLoadFreshTtl : Boolean = true; // test_load_is_touch_with_fresh_ttl + attribute evictKeepsAclNoLease : Boolean = true; // test_restore_carries_no_lease attribute maxDepth : Integer = 4; attribute defaultQueryMaxRows : Integer = 50; attribute defaultQueryDepth : Integer = 2; @@ -199,7 +211,7 @@ package MemNet { satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_2_QueryFanoutCaps; satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_3_ConsistentValueByteCap; satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_4_ConsistentFieldCap; - satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru; + // MN-REQ-05.5 satisfy is not linked: the satisfy lands with the engine (evictShipped=false). satisfy MN_REQ_00_MissionBridge::MN_REQ_01_SessionLifecycle::MN_REQ_01_10_SessionLifecycleAclWho; satisfy MN_REQ_00_MissionBridge::MN_REQ_10_LlmPropertiesAndLimits::MN_REQ_10_2_PinMapMustFitContext; satisfy MN_REQ_00_MissionBridge::MN_REQ_12_MultitaskMode::MN_REQ_12_7_NoAssumeAclReserveIngest; @@ -3180,14 +3192,17 @@ package MemNet { (save_on_expire, expire_snapshot_dir_set) and the count of sessions held because expire-save failed (expire_snapshot_failed). Path redacted. Look only. - MN-REQ-05.5 (proposed): sessions_evicted counter for cap evictions; - the evicted session is named by name or tag, never a real mn_ id. + MN-REQ-05.5 (proposed, not shipped): sessions_evicted and + sessions_unsaveable_held for cap evictions. Admin only: the evicted + session's name or tag, never a real mn_ id. Caller results carry no + eviction field. Runtime: tests/test_session_evict.py. */ attribute lookOnly : Boolean = true; attribute saveOnExpireFlag : Boolean = true; attribute expireSnapshotDirSetFlag : Boolean = true; attribute expireSnapshotFailedCount : Boolean = true; attribute sessionsEvictedCounter : Boolean = true; + attribute sessionsUnsaveableHeld : Boolean = true; attribute pathRedacted : Boolean = true; } diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index 31c6b80e..819d3514 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -34,7 +34,7 @@ MN-REQ-03.4 MATCH WHERE SET/DELETE SHALL honour the predicate or refuse MN-REQ-05.3 One decoded value_bytes cap on pipe mutate, GQL mutate, snapshot load MN-REQ-05.4 One effective-field cap (default 64) on SCHEMA register, mutate, snapshot save/load; save never stricter than write - MN-REQ-05.5 Session cap evicts least-recently-touched saveable session (proposed, not shipped); save victim first; none evictable keeps limit_exceeded|sessions refusal + MN-REQ-05.5 Session cap evicts least-recently-touched saveable session (proposed, not shipped); save victim first; none evictable refuses limit_exceeded ("all sessions are in use"); restore: same ACL, no lease carried over MN-REQ-06.11 Admin-only serve usage report (counts/caps; opaque session alias; not agent MCP) MN-REQ-06.12 Product gateway on memnet-mcp: per-product route to owning serve (not mn_tip_) MN-REQ-06.13 Serve request isolation: each command's stdout, stderr, and exit_code @@ -766,23 +766,81 @@ package MemNetRequirements { requirement def MN_REQ_05_5_SessionCapEvictLru { doc /* - Proposed, not shipped. When the session cap (MEMNET_MAX_SESSIONS, - default 1024) is reached on session open or load, after - purge_expired, the engine SHALL evict the live session with the - oldest last-touch time; any read or write counts as a touch. - Before the RAM drop the victim SHALL be saved to its snapshot - first (fsync, atomic 0600 write, @SNAP version 2 with the ACL - and lease digest kept). An unsaveable victim (snapshot_unsaveable, - over cap, or no snapshot dir) SHALL be skipped, stay in RAM, and - the next-oldest SHALL be tried. If no session is evictable the - limit_exceeded|sessions n/cap refusal SHALL stand and nothing - SHALL be dropped. The session being opened or loaded SHALL NOT be - evicted, nor any session holding an active write lock (RSV lease - or in-flight commit). The result SHALL report the evicted session - by name or tag only, never a real mn_ id; serve_status SHALL carry - a sessions_evicted counter. A later session_load SHALL restore the - evicted session from its snapshot with the same ACL and lease. - Verify: MN-VER-05-S03 to MN-VER-05-S09. + Proposed, not shipped (engine pending). Runtime checks: + tests/test_session_evict.py (xfail until the engine ships). + + Cap. At session open or load, after purge_expired, when the count + reaches MEMNET_MAX_SESSIONS (default 1024) the engine SHALL pick at + most one victim. One cap lock SHALL cover the count, the victim pick + and the slot reservation; the victim is marked evicting under that + lock. The save then runs outside the cap lock, under the victim's + session lock. + + Victim. The live, non-evicting session with the oldest last touch. + A touch is any read or write through the session (get_session, + mutate, read, load). Admin and serve_status reads are NOT touches. + The session being opened or loaded is excluded separately; only an + open bind or live writes (its session lock held by an in-flight + mutate or commit) exempt any other session. A reserve (RSV) lease + alone does NOT exempt its session. Exempt sessions are never + auto-dropped. + + Save first. The victim's session lock SHALL be held from pick + through save, RAM drop and registry removal, then released. Under + that lock the victim SHALL be written to MEMNET_EVICT_SNAPSHOT_DIR as + an atomic write: temp file in the same directory, fsync the file, + rename over the final name, fsync the directory; mode 0600; @SNAP + version 2 with the ACL. Only after a complete save SHALL the engine + drop the victim from RAM, then remove its registry entry. A failed + save keeps the victim live (EvError: evictSaving to active) and the + next-oldest candidate is tried. + + Crash safety. A crash after the fsync and before the drop SHALL + leave a complete snapshot. On restart the session is restored from + that snapshot or is absent; never torn. + + No snapshot dir. MEMNET_EVICT_SNAPSHOT_DIR has no default. Without + it the cap refuses and nothing is evicted. + + Unsaveable. An unsaveable candidate (snapshot_unsaveable, over cap, + or write error) SHALL stay live and the engine SHALL try the + next-oldest candidate. No auto-drop of unsaveable sessions. The + count of sessions held unsaveable SHALL be reported as + sessions_unsaveable_held on serve_status and surfaced to admin. + + Refusal. If no session is evictable, the engine SHALL refuse with + code limit_exceeded and the plain message "all sessions are in use". + Nothing SHALL be dropped and no snapshot written. + + Restore. session_load of an evicted id from its snapshot SHALL give + the same ACL, no lease carried over: reserve leases do not survive + and the restored session has no bind. A load is a touch and starts + a fresh TTL. The reopened session returns restored=true and emits + no alerts. + + Caller. The caller result carries no cap and no eviction field: the + caller is not told that a cap or an eviction exists. The evicted + session's name or tag (never an mn_ id) and the sessions_evicted + counter are reported on admin serve_status only. + + Settled (not open): a lease does not survive eviction; a load is a + touch with a fresh TTL; admin and serve_status reads are not + touches; no default snapshot dir (no dir means the cap refuses); + one cap lock for count, pick and slot reservation; save outside + the cap lock, under the victim lock; no auto-drop of unsaveable + sessions, counted and surfaced. + + LATER (not dropped, not modelled): a "touched within the last N + minutes" exemption. Do not add it until a measured run shows + reload-thrash at cap=3: cycle opens over 4 or more live sessions and + count evict-then-reload inside a short interval. + + Open items (doc only, not rules yet): (a) a distinct session_evicted + refusal for a caller who holds an evicted id; (b) whether + session_load of an evicted id returns the same id. + + Verify: runtime tests in tests/test_session_evict.py, cited by + MN-VER-05-S03 to MN-VER-05-S09. */ attribute requirementId : String = "MN-REQ-05.5"; } diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index b78a0b28..ec9ad00b 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -56,9 +56,10 @@ session loss; no SemVer bump. Session cap LRU evict (MN-VER-05-S03..S09, proposed, not shipped): MN-REQ-05.5 — oldest-touch pick; save first then drop; skip - unsaveable; none evictable refuses limit_exceeded|sessions; self and - write-locked exempt; name not mn_ id plus serve_status counter; - later load restores with ACL and lease (@SNAP v2). + unsaveable; none evictable refuses limit_exceeded (all sessions are in + use); self, write-locked and open-bind exempt; name not mn_ id on admin + serve_status only; later load restores: same ACL, no lease carried over + (@SNAP v2). Runtime: tests/test_session_evict.py (xfail until shipped). Serve checkpoint (MN-VER-06-S13): ServeCheckpoint on TcpServeBridge; admin credential; per-session lock; lossless atomic snaps; skip unsaveable; no drain; no live load; no @@ -2322,28 +2323,27 @@ package MemNetVerification { verification def MN_VER_05_S03_SessionCapEvictOldestTouch { doc /* - MN-REQ-05.5 R1 (proposed, not shipped) — at MEMNET_MAX_SESSIONS - (default 1024) on open or load, after purge_expired, evict the live - session with the oldest last-touch time; any read or write is a - touch. Knob MEMNET_MAX_SESSIONS. + MN-REQ-05.5 R1 (proposed, not shipped) — at MEMNET_MAX_SESSIONS on open + or load, after purge_expired, evict the live session with the oldest + last touch. Any read or write is a touch; admin and serve_status reads + are not. Runtime checks (xfail until shipped): + tests/test_session_evict.py::test_evicts_oldest_touched_first, + ::test_reads_and_writes_are_touches, + ::test_admin_and_serve_status_reads_are_not_touches. */ attribute verificationId : String = "MN-VER-05-S03"; subject system : MemNetSystem; objective sessionCapEvictOldestTouch { + doc /* + Runtime: tests/test_session_evict.py (oldest-touch order, touch + semantics, admin reads not touches). Status guard only below. + */ verify sessionCapEvictLruReq; verify sessionTtlAndCapsReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictOnSessionCap == true - and system.core.transport.inProcess.memory.sessions.caps - .envMaxSessions == "MEMNET_MAX_SESSIONS" - and system.core.transport.inProcess.memory.sessions.caps - .evictPicksOldestTouch == true - and system.core.transport.inProcess.memory.sessions.caps - .evictTouchOnReadOrWrite == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } @@ -2352,23 +2352,30 @@ package MemNetVerification { verification def MN_VER_05_S04_SessionCapEvictSaveFirst { doc /* MN-REQ-05.5 R2 (proposed) — the victim is saved to its snapshot first - (fsync, atomic 0600, @SNAP v2 with ACL and lease digest kept), then - dropped from RAM. A failed save never drops RAM. + (temp file, fsync, rename, fsync dir; 0600; @SNAP v2 with the ACL), + then dropped from RAM. The victim lock is held from pick through + save, drop and registry removal. A crash after fsync and before drop + leaves a complete snapshot. A failed save never drops RAM. Runtime checks + (xfail until shipped): tests/test_session_evict.py:: + test_victim_saved_before_drop_atomic_fsync, + ::test_victim_lock_held_from_pick_through_drop, + ::test_crash_after_fsync_before_drop_is_restorable, + ::test_failed_save_never_drops_ram. */ attribute verificationId : String = "MN-VER-05-S04"; subject system : MemNetSystem; objective sessionCapEvictSaveFirst { + doc /* + Runtime: tests/test_session_evict.py (save before drop, victim lock, + crash safety, failed save keeps RAM). Status guard only below. + */ verify sessionCapEvictLruReq; verify saveSessionSnapshotReq; verify snapshotLosslessRoundTripReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictSavesFirstFsync == true - and system.core.transport.inProcess.memory.sessions.caps - .evictKeepsAclLease == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } @@ -2376,22 +2383,25 @@ package MemNetVerification { verification def MN_VER_05_S05_SessionCapEvictSkipUnsaveable { doc /* - MN-REQ-05.5 R3 (proposed) — an unsaveable victim (snapshot_unsaveable, - over cap, or no snapshot dir) is skipped, stays in RAM, and the - next-oldest session is tried. + MN-REQ-05.5 R3 (proposed) — an unsaveable candidate (snapshot_unsaveable, + over cap, write error) stays live and the next-oldest is tried. No + auto-drop; the count is reported as sessions_unsaveable_held on + serve_status and surfaced to admin. Runtime checks (xfail until shipped): + tests/test_session_evict.py::test_unsaveable_victim_skipped_next_oldest_tried, + ::test_unsaveable_held_counted_on_serve_status. */ attribute verificationId : String = "MN-VER-05-S05"; subject system : MemNetSystem; objective sessionCapEvictSkipUnsaveable { + doc /* + Runtime: tests/test_session_evict.py (skip and count). Status guard + only below. + */ verify sessionCapEvictLruReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictSkipsUnsaveable == true - and system.core.transport.inProcess.memory.sessions.caps - .evictPicksOldestTouch == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } @@ -2399,20 +2409,27 @@ package MemNetVerification { verification def MN_VER_05_S06_SessionCapEvictNoneEvictable { doc /* - MN-REQ-05.5 R4 (proposed) — cap full and every candidate unsaveable, - so refuse with limit_exceeded|sessions n/cap as today; nothing is - dropped. + MN-REQ-05.5 R4 (proposed) — cap full and no evictable candidate: refuse + with code limit_exceeded and the message "all sessions are in use"; + nothing is dropped. No snapshot dir means refuse, no eviction. Concurrent + opens at cap=2 keep count <= cap with one victim per slot. + Runtime checks (xfail until shipped): tests/test_session_evict.py:: + test_all_in_use_refusal_drops_nothing, + ::test_no_snapshot_dir_refuses_without_eviction, + ::test_cap_two_concurrent_opens_one_victim_per_slot. */ attribute verificationId : String = "MN-VER-05-S06"; subject system : MemNetSystem; objective sessionCapEvictNoneEvictable { + doc /* + Runtime: tests/test_session_evict.py (refusal, no snapshot dir, + concurrent opens). Status guard only below. + */ verify sessionCapEvictLruReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictRefusesWhenNoneEvictable == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } @@ -2420,22 +2437,27 @@ package MemNetVerification { verification def MN_VER_05_S07_SessionCapEvictExemptSelfAndLocked { doc /* - MN-REQ-05.5 R5 (proposed) — the session being opened or loaded is - never evicted, nor is a session holding an active write lock (RSV - lease or in-flight commit). + MN-REQ-05.5 R5 (proposed) — exempt from eviction: the session being + opened or loaded; a session with an open bind; a session with live + writes (session lock held by an in-flight mutate or commit). A reserve + (RSV) lease alone does not exempt. No touch window (LATER, not modelled). + Runtime checks (xfail until shipped): tests/test_session_evict.py:: + test_session_being_loaded_is_not_evicted, + ::test_write_locked_session_exempt, ::test_open_bind_exempt, + ::test_reserve_lease_is_not_an_exemption. */ attribute verificationId : String = "MN-VER-05-S07"; subject system : MemNetSystem; objective sessionCapEvictExemptSelfAndLocked { + doc /* + Runtime: tests/test_session_evict.py (exemption set). Status guard + only below. + */ verify sessionCapEvictLruReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictNeverSelf == true - and system.core.transport.inProcess.memory.sessions.caps - .evictNeverWriteLocked == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } @@ -2443,22 +2465,27 @@ package MemNetVerification { verification def MN_VER_05_S08_SessionCapEvictReportNameNotId { doc /* - MN-REQ-05.5 R6 (proposed) — the eviction result reports the evicted - session by name or tag only, never a real mn_ id. serve_status carries - the sessions_evicted counter (ServeStatusLook.sessionsEvictedCounter - on MemNetUsageDashboard, outside MemNetSystem; a verification has one - subject, so the counter is checked by its deploy attribute, not here). + MN-REQ-05.5 R6 (proposed) — the caller result carries no cap and no + eviction field. Admin serve_status reports the evicted session by name + or tag only, never a real mn_ id, plus the sessions_evicted counter + (ServeStatusLook on MemNetUsageDashboard, outside MemNetSystem; the + counter is checked by its deploy attribute, not here). Runtime checks + (xfail until shipped): tests/test_session_evict.py:: + test_caller_result_has_no_eviction_field, + ::test_admin_report_names_victim_never_mn_id. */ attribute verificationId : String = "MN-VER-05-S08"; subject system : MemNetSystem; objective sessionCapEvictReportNameNotId { + doc /* + Runtime: tests/test_session_evict.py (caller silence, admin naming). + Status guard only below. + */ verify sessionCapEvictLruReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictReportsNameNotId == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } @@ -2467,23 +2494,30 @@ package MemNetVerification { verification def MN_VER_05_S09_SessionCapEvictLoadRestores { doc /* MN-REQ-05.5 R7 (proposed) — a later session_load restores the evicted - session from its snapshot with the same ACL and lease (@SNAP v2, digest - only; MN-REQ-06.16). + session from its snapshot: same ACL, no lease carried over (reserve + leases dropped; the restored session has no bind). The load is a + touch with a fresh TTL; the reopened session returns restored=true and + emits no alerts. Rows and edges survive. Runtime checks (xfail until + shipped): tests/test_session_evict.py:: + test_restore_keeps_rows_edges_and_acl, + ::test_restore_carries_no_lease, + ::test_reopen_restored_true_no_alerts, + ::test_load_is_touch_with_fresh_ttl. */ attribute verificationId : String = "MN-VER-05-S09"; subject system : MemNetSystem; objective sessionCapEvictLoadRestores { + doc /* + Runtime: tests/test_session_evict.py (restore fidelity, ACL, no lease, + restored flag, fresh TTL). Status guard only below. + */ verify sessionCapEvictLruReq; verify loadSessionSnapshotReq; verify snapshotAclReq; require constraint { system.core.transport.inProcess.memory.sessions.caps - .evictLoadRestores == true - and system.core.transport.inProcess.memory.sessions.caps - .evictKeepsAclLease == true - and system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } } diff --git a/tests/test_session_evict.py b/tests/test_session_evict.py new file mode 100644 index 00000000..4611c15c --- /dev/null +++ b/tests/test_session_evict.py @@ -0,0 +1,505 @@ +"""MN-REQ-05.5 session cap LRU evict — runtime checks on the in-process engine. + +Proposed, not shipped. Every test here is xfail until the engine ships the +eviction path (module-level mark below). Test names are cited by the +MN-VER-05-S03..S09 verify defs in sysml-models/models/verify.sysml; the +presence check in tests/test_sysml_session_evict.py keeps the two in sync. + +Never print session ids here: assertion messages name the rule, not the id. +""" + +from __future__ import annotations + +import asyncio +import json +import os +import re +import stat +import threading +from datetime import UTC, datetime, timedelta +from unittest.mock import patch + +import pytest +from typer.testing import CliRunner + +import memnet.registry as registry_mod +import memnet.session as session_mod +import memnet.snapshot as snapshot_mod +from memnet.acl import acl_to_dict +from memnet.admin_usage import build_report # noqa: F401 (admin read surface) +from memnet.cli import app +from memnet.exceptions import MemNetError +from memnet.mutate_gate import MutateGate +from memnet.neighbourhood_reserve import reserve +from memnet.registry import contains, count, get_entry +from memnet.session import ( + SessionStore, + get_session, + list_sessions, + open_session, + reset_registry, + set_now_override, +) +from memnet.snapshot import load_snapshot + +pytestmark = pytest.mark.xfail(reason="MN-REQ-05.5 not shipped; engine pending", strict=False) + +runner = CliRunner() + +ENV_MAX = "MEMNET_MAX_SESSIONS" +ENV_DIR = "MEMNET_EVICT_SNAPSHOT_DIR" +ENV_ADMIN = "MEMNET_ADMIN_TOKEN" +ADMIN_TOKEN = "test-admin-token" # dummy value for the in-process admin read +BASE = datetime(2026, 10, 20, 12, 0, tzinfo=UTC) +_MN_ID = re.compile(r"mn_[0-9a-fA-F]+") +_PLR = ( + "CREATE (:PLR {id: 'PLR01', identity: 'Hero', wealth: 1, cashflow: 0, " + "monopoly: 0, reputation: 0, inventory: 'bag'})" +) + + +def _at(minute: float) -> datetime: + return BASE + timedelta(minutes=minute) + + +@pytest.fixture +def evict(memnet_temp, monkeypatch, tmp_path): + """Cap 3, snapshot dir set, no touch window (LATER). Clock fixed to BASE.""" + snap_dir = tmp_path / "evict-snaps" + snap_dir.mkdir() + monkeypatch.setenv(ENV_MAX, "3") + monkeypatch.setenv(ENV_DIR, str(snap_dir)) + set_now_override(BASE) + return snap_dir + + +def _open(schema, minute: float, ttl: int = 600) -> SessionStore: + set_now_override(_at(minute)) + return open_session(map_file=str(schema), ttl_minutes=ttl) + + +def _touch(sid: str, minute: float) -> SessionStore: + set_now_override(_at(minute)) + return get_session(sid) + + +def _seed(sid: str, workflow) -> None: + """Write rows and edges through the CLI add path (a real write).""" + r = runner.invoke(app, ["add", "--file", str(workflow), "--session", sid]) + assert r.exit_code == 0, "seed write failed" + + +def _snapshot_of(snap_dir, sid: str): + hits = [p for p in snap_dir.iterdir() if p.is_file() and sid in p.read_text(encoding="utf-8")] + assert len(hits) == 1, "expected exactly one snapshot for the evicted session" + return hits[0] + + +def _make_unsaveable(ss: SessionStore) -> None: + MutateGate(ss).apply([_PLR], mode="add") + ss.store.get("PLR01").fields["identity"] = "x" * 9000 + + +def _serve_status_payload() -> dict: + from memnet_mcp.server import serve_status + + return json.loads(asyncio.run(serve_status())) + + +# --- S03: oldest-touch order and touch semantics ---------------------------- + + +def test_evicts_oldest_touched_first(evict, schema_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + c = _open(schema_file, 2) + _touch(a.session_id, 3) # a is now the newest touch + d = _open(schema_file, 4) + assert not contains(b.session_id), "oldest-touched session must be the victim" + assert contains(a.session_id) and contains(c.session_id) and contains(d.session_id) + + +def test_reads_and_writes_are_touches(evict, schema_file, workflow_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + c = _open(schema_file, 2) + set_now_override(_at(3)) + _seed(a.session_id, workflow_file) # write touches a + _touch(b.session_id, 4) # read touches b + _open(schema_file, 5) + assert not contains(c.session_id), "untouched session must be the victim" + assert contains(a.session_id) and contains(b.session_id) + + +def test_admin_and_serve_status_reads_are_not_touches(evict, schema_file, monkeypatch): + monkeypatch.setenv(ENV_ADMIN, ADMIN_TOKEN) + a = _open(schema_file, 0) + b = _open(schema_file, 1) + c = _open(schema_file, 2) + set_now_override(_at(3)) + list_sessions() + build_report(ADMIN_TOKEN) + _serve_status_payload() + d = _open(schema_file, 4) + assert not contains(a.session_id), "admin/serve_status reads must not refresh the touch" + assert contains(b.session_id) and contains(c.session_id) and contains(d.session_id) + + +# --- S04: save first, atomic write, victim lock, crash safety --------------- + + +def test_victim_saved_before_drop_atomic_fsync(evict, schema_file, workflow_file, monkeypatch): + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + _open(schema_file, 1) + _open(schema_file, 2) + victim = a.session_id + fsynced: list[int] = [] + real_fsync = os.fsync + + def counting_fsync(fd): + fsynced.append(fd) + return real_fsync(fd) + + monkeypatch.setattr(os, "fsync", counting_fsync) + _open(schema_file, 4) + assert not contains(victim) + assert len(fsynced) >= 2, "file and directory must both be fsynced" + snap = _snapshot_of(evict, victim) + assert stat.S_IMODE(snap.stat().st_mode) == 0o600 + leftovers = [p.name for p in evict.iterdir() if p != snap] + assert not leftovers, "no temp files may be left in the snapshot dir" + + +def test_victim_lock_held_from_pick_through_drop(evict, schema_file, monkeypatch): + a = _open(schema_file, 0) + _open(schema_file, 1) + _open(schema_file, 2) + victim = a.session_id + real_write = snapshot_mod.write_snapshot + writing = threading.Event() + release = threading.Event() + + def slow_write(ss, path, **kwargs): + if ss.session_id == victim: + writing.set() + release.wait(5) + return real_write(ss, path, **kwargs) + + monkeypatch.setattr(snapshot_mod, "write_snapshot", slow_write) + opener = threading.Thread(target=lambda: _open(schema_file, 4)) + opener.start() + try: + assert writing.wait(5), "eviction never reached the save" + entry = get_entry(victim) + assert entry is not None + acquired = entry.lock.acquire(timeout=0.2) + if acquired: + entry.lock.release() + assert not acquired, "victim lock must be held during save" + finally: + release.set() + opener.join(5) + assert not opener.is_alive() + assert not contains(victim) + + +def test_crash_after_fsync_before_drop_is_restorable(evict, schema_file, workflow_file): + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + _open(schema_file, 1) + _open(schema_file, 2) + victim = a.session_id + crash = RuntimeError("simulated crash") + with ( + patch.object(registry_mod, "remove_entry", side_effect=crash) as reg_drop, + patch.object(session_mod, "remove_entry", side_effect=crash) as ses_drop, + ): + try: + _open(schema_file, 4) + except RuntimeError: + pass + assert reg_drop.called or ses_drop.called, "crash hook never ran" + snap = _snapshot_of(evict, victim) # complete snapshot exists + reset_registry() # restart: RAM is lost + assert not contains(victim) + restored = load_snapshot(snap) # restorable after restart, never torn + assert restored.store.get("PLR01") is not None, "rows from before the crash must be intact" + + +def test_failed_save_never_drops_ram(evict, schema_file, monkeypatch): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + _open(schema_file, 2) + victim = a.session_id + real_write = snapshot_mod.write_snapshot + + def failing_write(ss, path, **kwargs): + if ss.session_id == victim: + raise OSError("simulated disk full") + return real_write(ss, path, **kwargs) + + monkeypatch.setattr(snapshot_mod, "write_snapshot", failing_write) + _open(schema_file, 4) + assert contains(victim), "a failed save must keep the victim live" + assert not contains(b.session_id), "the next-oldest candidate must be tried" + + +# --- S05: skip unsaveable, count them ----------------------------------------- + + +def test_unsaveable_victim_skipped_next_oldest_tried(evict, schema_file): + a = _open(schema_file, 0) + _make_unsaveable(a) + b = _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) + assert contains(a.session_id), "unsaveable session stays live" + assert not contains(b.session_id), "next-oldest saveable session is the victim" + + +def test_unsaveable_held_counted_on_serve_status(evict, schema_file): + a = _open(schema_file, 0) + _make_unsaveable(a) + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) + payload = _serve_status_payload() + assert payload.get("sessions_unsaveable_held") == 1, "held unsaveable sessions must be counted" + + +# --- S06: refusal, no snapshot dir, concurrency ------------------------------- + + +def test_all_in_use_refusal_drops_nothing(evict, schema_file): + ids = [_open(schema_file, m).session_id for m in (0, 1, 2)] + for sid in ids: # every session is in use: open bind, so none is evictable + SessionStore(sid).set_bind(f"mission-{sid[:4]}", "lease-x") + with pytest.raises(MemNetError) as exc: + _open(schema_file, 1) + assert exc.value.code == "limit_exceeded" + assert "all sessions are in use" in exc.value.message + assert all(contains(sid) for sid in ids), "nothing may be dropped on refusal" + assert not any(evict.iterdir()), "no snapshot may be written on refusal" + + +def test_no_snapshot_dir_refuses_without_eviction(evict, schema_file, monkeypatch): + monkeypatch.delenv(ENV_DIR, raising=False) + ids = [_open(schema_file, m).session_id for m in (0, 1, 2)] + with pytest.raises(MemNetError) as exc: + _open(schema_file, 4) + assert exc.value.code == "limit_exceeded" + assert all(contains(sid) for sid in ids), "no eviction without a snapshot dir" + + +def test_cap_two_concurrent_opens_one_victim_per_slot(evict, schema_file, monkeypatch): + monkeypatch.setenv(ENV_MAX, "2") + a = _open(schema_file, 0) + b = _open(schema_file, 1) + seeded = {a.session_id, b.session_id} + set_now_override(_at(30)) + barrier = threading.Barrier(4) + opened: list[SessionStore] = [] + refused: list[MemNetError] = [] + errors: list[Exception] = [] + samples: list[int] = [] + stop = threading.Event() + + def worker(): + barrier.wait(5) + try: + opened.append(open_session(map_file=str(schema_file), ttl_minutes=600)) + except MemNetError as exc: + refused.append(exc) + except Exception as exc: # any other error is a failure + errors.append(exc) + + def sampler(): + while not stop.is_set(): + samples.append(count()) + + mon = threading.Thread(target=sampler) + threads = [threading.Thread(target=worker) for _ in range(4)] + mon.start() + for t in threads: + t.start() + for t in threads: + t.join(10) + stop.set() + mon.join(5) + + assert not errors, "only limit_exceeded refusals are allowed" + assert len(opened) + len(refused) == 4 + # Two victims exist and the cap lock serialises picks, so the first two opens always + # succeed. Later opens may be refused while both victims are mid-save (race-dependent). + assert len(opened) >= 2, "the first two opens each free one slot" + assert all(e.code == "limit_exceeded" for e in refused) + assert samples and max(samples) <= 2, "count must never exceed the cap" + assert count() == 2 + created = seeded | {s.session_id for s in opened} + evicted = {sid for sid in created if not contains(sid)} + assert len(evicted) == len(opened), "each successful open consumes exactly one victim" + assert len(list(evict.iterdir())) == len(evicted), "one snapshot per victim" + + +# --- S07: exemptions ---------------------------------------------------------- + + +def test_session_being_loaded_is_not_evicted(evict, schema_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + c = _open(schema_file, 2) + d = _open(schema_file, 4) # evicts a + snap = _snapshot_of(evict, a.session_id) + set_now_override(_at(5)) + loaded = load_snapshot(snap) # cap full: victim is oldest of b, c, d + assert contains(loaded.session_id), "the session being loaded is never its own victim" + assert not contains(b.session_id) + assert contains(c.session_id) and contains(d.session_id) + + +def test_write_locked_session_exempt(evict, schema_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + _open(schema_file, 2) + held = threading.Event() + release = threading.Event() + holder_ss = SessionStore(a.session_id) + + def hold(): + with holder_ss.lock(exclusive=True): + held.set() + release.wait(5) + + t = threading.Thread(target=hold) + t.start() + try: + assert held.wait(5) + _open(schema_file, 4) + finally: + release.set() + t.join(5) + assert contains(a.session_id), "write-locked session is exempt" + assert not contains(b.session_id), "next-oldest candidate is the victim" + + +def test_open_bind_exempt(evict, schema_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + _open(schema_file, 2) + SessionStore(a.session_id).set_bind("mission-x", "lease-x") + _open(schema_file, 4) + assert contains(a.session_id), "session with an open bind is exempt" + assert not contains(b.session_id) + + +def test_reserve_lease_is_not_an_exemption(evict, schema_file, workflow_file): + # Only open bind and live writes are exempt. A reserve lease does not protect + # its session, and the lease does not survive the eviction. + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + b = _open(schema_file, 1) + _open(schema_file, 2) + holder = SessionStore(a.session_id) + reserve(holder.reserves, holder.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(3)) + _open(schema_file, 4) + assert not contains(a.session_id), "a reserve lease alone does not exempt a session" + assert contains(b.session_id) + loaded = load_snapshot(_snapshot_of(evict, a.session_id)) + assert loaded.reserves.leases == {}, "reserve leases do not survive eviction" + + +# --- S08: caller silence, admin naming --------------------------------------- + + +def test_caller_result_has_no_eviction_field(evict, schema_file): + for minute in (0, 1, 2): + set_now_override(_at(minute)) + runner.invoke(app, ["session", "open", "--map-file", str(schema_file)]) + set_now_override(_at(4)) + res = runner.invoke(app, ["session", "open", "--map-file", str(schema_file)]) + assert res.exit_code == 0 + text = (res.stdout + res.stderr).lower() + assert "evict" not in text, "caller output must not mention eviction" + + +def test_admin_report_names_victim_never_mn_id(evict, schema_file): + a = _open(schema_file, 0) + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a + payload = _serve_status_payload() + dumped = json.dumps(payload, default=str) + assert payload.get("sessions_evicted") == 1, "admin status counts the eviction" + assert not _MN_ID.search(dumped), "admin status must not carry a real session id" + assert not contains(a.session_id) + + +# --- S09: restore fidelity, no lease, restored flag, fresh TTL --------------- + + +def test_restore_keeps_rows_edges_and_acl(evict, schema_file, workflow_file): + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + victim = a.session_id + ss = SessionStore(victim) + ss.enable_acl() + ss.grant_caller("worker-1", can_mutate=False) + rows_before = ss.store.row_count_non_law() + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a + snap = _snapshot_of(evict, victim) + set_now_override(_at(5)) + loaded = load_snapshot(snap) + assert loaded.store.row_count_non_law() == rows_before, "row count must survive" + assert loaded.store.get("PLR01") is not None, "node rows must survive" + assert loaded.store.get("E02") is not None, "edges must survive" + assert loaded.acl.enabled and "worker-1" in loaded.acl.callers + assert loaded.acl.callers["worker-1"].can_mutate is False + + +def test_restore_carries_no_lease(evict, schema_file, workflow_file): + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + victim = a.session_id + SessionStore(victim).grant_caller("worker-1") + holder = SessionStore(victim) + reserve(holder.reserves, holder.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(0.5)) + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a; a reserve lease alone does not exempt it + snap = _snapshot_of(evict, victim) + set_now_override(_at(5)) + loaded = load_snapshot(snap) + assert loaded.reserves.leases == {}, "restored session must carry no reserve leases" + assert not (acl_to_dict(loaded.acl) or {}).get("bind"), "no bind may survive the restore" + assert "worker-1" in loaded.acl.callers, "the ACL itself is kept" + + +def test_reopen_restored_true_no_alerts(evict, schema_file, capsys): + a = _open(schema_file, 0) + victim = a.session_id + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a + snap = _snapshot_of(evict, victim) + set_now_override(_at(5)) + capsys.readouterr() + loaded = load_snapshot(snap) + err = capsys.readouterr().err + assert getattr(loaded, "restored", None) is True, "reopen must report restored=true" + assert "WRN" not in err, "reopen of an evicted session emits no alerts" + + +def test_load_is_touch_with_fresh_ttl(evict, schema_file): + a = _open(schema_file, 0, ttl=60) + victim = a.session_id + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a + snap = _snapshot_of(evict, victim) + set_now_override(_at(30)) + loaded = load_snapshot(snap) + expires = datetime.fromisoformat(loaded.meta.expires_at.replace("Z", "+00:00")) + assert expires == _at(30 + 60), "a load starts a fresh TTL from load time" diff --git a/tests/test_sysml_session_evict.py b/tests/test_sysml_session_evict.py index 075d7670..a6b4be05 100644 --- a/tests/test_sysml_session_evict.py +++ b/tests/test_sysml_session_evict.py @@ -1,7 +1,15 @@ -"""MN-REQ-05.5 session cap LRU evict: SysML text checks (proposed, not shipped).""" +"""MN-REQ-05.5 model presence: the SysML cites runtime tests (proposed, not shipped). + +Runtime behaviour lives in tests/test_session_evict.py. This file only checks +that the model points at those tests, that every cited test exists, and that +the runtime module stays xfail until the engine ships. It makes no claim that a +flag is true. +""" from __future__ import annotations +import ast +import re from pathlib import Path ROOT = Path(__file__).resolve().parents[1] @@ -11,120 +19,103 @@ REQ = MODELS / "requirements.sysml" VERIFY = MODELS / "verify.sysml" BEHAVIOUR = MODELS / "behaviour.sysml" +RUNTIME = ROOT / "tests" / "test_session_evict.py" +VER_IDS = [f"MN-VER-05-S0{n}" for n in range(3, 10)] def _read(path: Path) -> str: return path.read_text(encoding="utf-8") -def test_mn_req_05_5_requirement_def_and_usage(): +def _verify_docs(text: str) -> dict[str, str]: + """Map MN-VER-05-S0x id to its verification def doc, one def block at a time.""" + docs: dict[str, str] = {} + for block in re.split(r"(?=verification def )", text): + ver = re.search(r'attribute verificationId : String = "(MN-VER-05-S0\d)";', block) + doc = re.search(r"doc /\*(.*?)\*/", block, re.S) + if ver and doc: + docs[ver.group(1)] = doc.group(1) + return docs + + +def _cited_tests(doc: str) -> set[str]: + """Test names cited in a doc, ignoring the runtime file path itself.""" + return set(re.findall(r"\btest_\w+", doc.replace("tests/test_session_evict.py", ""))) + + +def _runtime_test_names() -> set[str]: + tree = ast.parse(_read(RUNTIME)) + return { + n.name for n in tree.body if isinstance(n, ast.FunctionDef) and n.name.startswith("test_") + } + + +def test_requirement_def_and_derivation_present(): text = _read(REQ) - assert "MN-REQ-05.5 Session cap evicts least-recently-touched" in text assert "requirement def MN_REQ_05_5_SessionCapEvictLru {" in text assert 'attribute requirementId : String = "MN-REQ-05.5";' in text assert "requirement sessionCapEvictLruReq" in text - assert "MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru;" in text assert "end #derive ::> sessionCapEvictLruReq;" in text -def test_mn_req_05_5_rules_in_doc(): - text = _read(REQ) - start = text.index("requirement def MN_REQ_05_5_SessionCapEvictLru {") - body = text[start : text.index('attribute requirementId : String = "MN-REQ-05.5";', start)] - assert "MEMNET_MAX_SESSIONS" in body - assert "oldest last-touch time" in body - assert "fsync" in body - assert "@SNAP version 2" in body - assert "snapshot_unsaveable" in body - assert "limit_exceeded|sessions n/cap" in body - assert "active write lock" in body - assert "sessions_evicted" in body - assert "later session_load SHALL restore" in body - assert "MN-VER-05-S03 to MN-VER-05-S09" in body - - -def test_mn_req_05_5_derivation_links(): - text = _read(REQ) - assert "end #original ::> sessionTtlAndCapsReq;" in text - assert "end #original ::> snapshotLosslessRoundTripReq;" in text - assert "end #original ::> snapshotAclReq;" in text - assert "#derivation connection deriveSessionCapEvictFromCapsAndSnapshot" in text +def test_verify_defs_s03_to_s09_present(): + text = _read(VERIFY) + docs = _verify_docs(text) + assert set(VER_IDS) <= set(docs) + for n in range(3, 10): + assert f"verification def MN_VER_05_S0{n}_" in text -def test_deploy_caps_evict_flags(): - text = _read(DEPLOY) - assert "attribute maxSessions : Integer = 1024;" in text - assert "attribute evictOnSessionCap : Boolean = true;" in text - assert 'attribute envMaxSessions : String = "MEMNET_MAX_SESSIONS";' in text - assert "attribute evictPicksOldestTouch : Boolean = true;" in text - assert "attribute evictTouchOnReadOrWrite : Boolean = true;" in text - assert "attribute evictSavesFirstFsync : Boolean = true;" in text - assert "attribute evictSkipsUnsaveable : Boolean = true;" in text - assert "attribute evictRefusesWhenNoneEvictable : Boolean = true;" in text - assert "attribute evictNeverSelf : Boolean = true;" in text - assert "attribute evictNeverWriteLocked : Boolean = true;" in text - assert "attribute evictReportsNameNotId : Boolean = true;" in text - assert "attribute evictLoadRestores : Boolean = true;" in text - assert "attribute evictKeepsAclLease : Boolean = true;" in text - assert "attribute evictShipped : Boolean = false;" in text - assert "satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru;" in text +def test_each_verify_doc_names_runtime_pytests_that_exist(): + docs = _verify_docs(_read(VERIFY)) + names = _runtime_test_names() + for ver_id in VER_IDS: + doc = docs[ver_id] + assert "tests/test_session_evict.py" in doc, f"{ver_id} must name its runtime file" + cited = _cited_tests(doc) + assert cited, f"{ver_id} must cite at least one runtime test" + assert cited <= names, f"{ver_id} cites a test that does not exist" + + +def test_every_runtime_test_is_cited_by_a_verify_doc(): + docs = _verify_docs(_read(VERIFY)) + cited = set() + for ver_id in VER_IDS: + doc = docs[ver_id] + cited |= _cited_tests(doc) + assert _runtime_test_names() == cited + + +def test_runtime_module_is_xfail_until_shipped(): + text = _read(RUNTIME) + assert "pytestmark = pytest.mark.xfail(" in text + assert 'reason="MN-REQ-05.5 not shipped; engine pending"' in text + assert "strict=False" in text -def test_serve_status_sessions_evicted_counter(): +def test_deploy_satisfy_not_linked_while_not_shipped(): text = _read(DEPLOY) - start = text.index("part def ServeStatusLook {") - body = text[start : text.index("part def SessionCensusLook {", start)] - assert "attribute sessionsEvictedCounter : Boolean = true;" in body + satisfy = "satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru" + assert satisfy not in text + assert "attribute evictShipped : Boolean = false;" in text -def test_behaviour_evict_saving_state(): +def test_evict_saving_closes_only_on_evict_saved(): text = _read(BEHAVIOUR) - assert "attribute def EvEvictForCap" in text - assert "state evictSaving" in text - assert "accept EvEvictForCap" in text - assert "then evictSaving;" in text - assert "transition evict_saving_to_closed" in text - assert "transition evict_saving_to_active" in text - assert "An evicted session (MN-REQ-05.5)" in text - assert "closed_to_loading via EvLoadSnapshot restores it" in text + assert "attribute def EvEvictSaved" in text + closed = r"transition evict_saving_to_closed\s+first evictSaving\s+accept EvEvictSaved\s" + assert re.search(closed + r"+then closed;", text) + active = ( + r"transition evict_saving_to_active\s+first evictSaving\s+accept EvError\s+then active;" + ) + assert re.search(active, text) -def test_verify_mn_ver_05_s03_to_s09_defs_and_usages(): - text = _read(VERIFY) - defs = [ - ("MN_VER_05_S03_SessionCapEvictOldestTouch", "MN-VER-05-S03", "sessionCapEvictOldestTouchVerify"), - ("MN_VER_05_S04_SessionCapEvictSaveFirst", "MN-VER-05-S04", "sessionCapEvictSaveFirstVerify"), - ("MN_VER_05_S05_SessionCapEvictSkipUnsaveable", "MN-VER-05-S05", "sessionCapEvictSkipUnsaveableVerify"), - ("MN_VER_05_S06_SessionCapEvictNoneEvictable", "MN-VER-05-S06", "sessionCapEvictNoneEvictableVerify"), - ( - "MN_VER_05_S07_SessionCapEvictExemptSelfAndLocked", - "MN-VER-05-S07", - "sessionCapEvictExemptSelfAndLockedVerify", - ), - ("MN_VER_05_S08_SessionCapEvictReportNameNotId", "MN-VER-05-S08", "sessionCapEvictReportNameNotIdVerify"), - ("MN_VER_05_S09_SessionCapEvictLoadRestores", "MN-VER-05-S09", "sessionCapEvictLoadRestoresVerify"), - ] - for def_name, ver_id, usage in defs: - assert f"verification def {def_name} {{" in text - assert f'attribute verificationId : String = "{ver_id}";' in text - assert f"verification {usage}" in text - assert f" : {def_name};" in text - assert "verify sessionCapEvictLruReq;" in text - assert "verify snapshotAclReq;" in text - assert "verify loadSessionSnapshotReq;" in text - - -def test_verify_05_5_constraints_use_caps_paths(): - text = _read(VERIFY) - start = text.index("verification def MN_VER_05_S03_SessionCapEvictOldestTouch {") - end = text.index("verification def MN_VER_06_S06_StorageRoles {", start) - block = text[start:end] - assert block.count("system.core.transport.inProcess.memory.sessions.caps") >= 7 - assert ".envMaxSessions == \"MEMNET_MAX_SESSIONS\"" in block - assert block.count(".evictShipped == false") == 7 - - -def test_readme_lists_05_5(): - text = _read(README) - assert "**05.5** session cap LRU evict (proposed, not shipped)" in text - assert "MN-VER-05-S03…S09 (MN-REQ-05.5 session cap LRU evict, proposed)" in text +def test_readme_points_at_runtime_file(): + assert "tests/test_session_evict.py" in _read(README) + + +def test_no_lease_carried_wording_anywhere_in_models(): + everything = "\n".join(_read(p) for p in MODELS.glob("*.sysml")) + _read(README) + assert "evictKeepsAclLease" not in everything + assert "same ACL and lease" not in everything From ba87659f97e493f89b64b9b7f4b042eebbbbacd9 Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:11:52 +0800 Subject: [PATCH 3/7] model: MN-REQ-05.5 re-review R1-R5, snapshot dir reuse, slot-until-drop, ship sync test --- sysml-models/models/behaviour.sysml | 4 +- sysml-models/models/deploy.sysml | 8 +- sysml-models/models/requirements.sysml | 64 +++++-- sysml-models/models/verify.sysml | 11 +- tests/test_session_evict.py | 252 ++++++++++++++++++++++--- tests/test_sysml_session_evict.py | 64 ++++++- 6 files changed, 340 insertions(+), 63 deletions(-) diff --git a/sysml-models/models/behaviour.sysml b/sysml-models/models/behaviour.sysml index d0cd81a8..101b377a 100644 --- a/sysml-models/models/behaviour.sysml +++ b/sysml-models/models/behaviour.sysml @@ -461,7 +461,9 @@ package MemNetBehaviour { Never entered for the session being opened or loaded, or for a session holding an active write lock or an open bind. The victim is marked evicting under the cap lock; its victim lock is held from pick - through save, drop and registry removal. Save runs outside the cap lock. + through save, drop and registry removal. Save runs outside the cap lock; + the victim keeps its slot until dropped, and the open that picked it + waits for this save. Atomic write: temp file in the same dir, fsync file, rename, fsync dir. */ } diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index 3a2ffad0..424839ae 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -162,14 +162,18 @@ package MemNet { attribute evictShipped : Boolean = false; attribute evictOnSessionCap : Boolean = true; // test_evicts_oldest_touched_first attribute envMaxSessions : String = "MEMNET_MAX_SESSIONS"; - attribute envSnapshotDir : String = "MEMNET_EVICT_SNAPSHOT_DIR"; + attribute envSnapshotDir : String = "MEMNET_EXPIRE_SNAPSHOT_DIR"; // reused; no second eviction knob + attribute envSnapshotDirAlias : String = "MEMNET_SNAPSHOT_DIR"; // optional neutral alias; same path or refuse start + attribute evictSnapshotDirAliasConflictRefuses : Boolean = true; // test_snapshot_dir_alias_conflict_refuses attribute evictSnapshotDirDefault : String = "unset"; // test_no_snapshot_dir_refuses_without_eviction + attribute evictCapFullWithDirEvicts : Boolean = true; // test_cap_full_with_snapshot_dir_evicts_oldest attribute evictPicksOldestTouch : Boolean = true; // test_evicts_oldest_touched_first attribute evictTouchOnReadOrWrite : Boolean = true; // test_reads_and_writes_are_touches attribute evictAdminReadsNotTouch : Boolean = true; // test_admin_and_serve_status_reads_are_not_touches attribute evictSavesFirstFsync : Boolean = true; // test_victim_saved_before_drop_atomic_fsync attribute evictVictimLockHeld : Boolean = true; // test_victim_lock_held_from_pick_through_drop attribute evictOneCapLock : Boolean = true; // test_cap_two_concurrent_opens_one_victim_per_slot + attribute evictVictimKeepsSlot : Boolean = true; // test_cap_two_concurrent_opens_one_victim_per_slot attribute evictSkipsUnsaveable : Boolean = true; // test_unsaveable_victim_skipped_next_oldest_tried attribute evictUnsaveableNotAutoDropped : Boolean = true; // test_unsaveable_held_counted_on_serve_status attribute evictRefusesWhenNoneEvictable : Boolean = true; // test_all_in_use_refusal_drops_nothing @@ -177,11 +181,13 @@ package MemNet { attribute evictNeverWriteLocked : Boolean = true; // test_write_locked_session_exempt attribute evictNeverOpenBind : Boolean = true; // test_open_bind_exempt attribute evictCallerNoEvictionField : Boolean = true; // test_caller_result_has_no_eviction_field + attribute evictResultNoCapFields : Boolean = true; // test_open_and_load_results_carry_no_cap_fields attribute evictReportAdminOnlyNameNotId : Boolean = true; // test_admin_report_names_victim_never_mn_id attribute evictLoadRestores : Boolean = true; // test_restore_keeps_rows_edges_and_acl attribute evictReopenRestoredTrue : Boolean = true; // test_reopen_restored_true_no_alerts attribute evictLoadFreshTtl : Boolean = true; // test_load_is_touch_with_fresh_ttl attribute evictKeepsAclNoLease : Boolean = true; // test_restore_carries_no_lease + attribute evictRestoreLeaseCommitFails : Boolean = true; // test_restore_lease_commit_fails_cleanly attribute maxDepth : Integer = 4; attribute defaultQueryMaxRows : Integer = 50; attribute defaultQueryDepth : Integer = 2; diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index 819d3514..8287bc6d 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -779,28 +779,39 @@ package MemNetRequirements { Victim. The live, non-evicting session with the oldest last touch. A touch is any read or write through the session (get_session, mutate, read, load). Admin and serve_status reads are NOT touches. - The session being opened or loaded is excluded separately; only an - open bind or live writes (its session lock held by an in-flight - mutate or commit) exempt any other session. A reserve (RSV) lease - alone does NOT exempt its session. Exempt sessions are never - auto-dropped. + A fresh open cannot be its own victim: its session is not in the + registry until its slot is reserved under the cap lock, so the pick + never sees it. A load of an evicted id is excluded from its own pick + the same way. Only an open bind or live writes (its session lock held + by an in-flight mutate or commit) exempt any other session. A reserve + (RSV) lease alone does NOT exempt its session. Exempt sessions are + never auto-dropped. Save first. The victim's session lock SHALL be held from pick - through save, RAM drop and registry removal, then released. Under - that lock the victim SHALL be written to MEMNET_EVICT_SNAPSHOT_DIR as - an atomic write: temp file in the same directory, fsync the file, + through save, RAM drop and registry removal, then released. The + victim keeps its slot until it is dropped: the open that picked it + waits for that save and takes the slot only after the drop. Under + that lock the victim SHALL be written to MEMNET_EXPIRE_SNAPSHOT_DIR + (reused; written whether or not MEMNET_SAVE_ON_EXPIRE is on) as an + atomic write: temp file in the same directory, fsync the file, rename over the final name, fsync the directory; mode 0600; @SNAP version 2 with the ACL. Only after a complete save SHALL the engine drop the victim from RAM, then remove its registry entry. A failed - save keeps the victim live (EvError: evictSaving to active) and the - next-oldest candidate is tried. + save keeps the victim live (EvError: evictSaving to active); the + engine then tries the next-oldest candidate, or refuses with + limit_exceeded if none is left. Crash safety. A crash after the fsync and before the drop SHALL leave a complete snapshot. On restart the session is restored from that snapshot or is absent; never torn. - No snapshot dir. MEMNET_EVICT_SNAPSHOT_DIR has no default. Without - it the cap refuses and nothing is evicted. + No snapshot dir. MEMNET_EXPIRE_SNAPSHOT_DIR has no default. Without + it the cap refuses and nothing is evicted. With it set, a full cap + evicts. An optional neutral alias MEMNET_SNAPSHOT_DIR MAY name the + same directory. If both are set to different paths, serve SHALL + refuse to start: Caps construction fails with config_conflict and + neither path is printed. The same path under both names is accepted. + Dropping a separate eviction knob is deliberate: one dir, one meaning. Unsaveable. An unsaveable candidate (snapshot_unsaveable, over cap, or write error) SHALL stay live and the engine SHALL try the @@ -819,16 +830,31 @@ package MemNetRequirements { no alerts. Caller. The caller result carries no cap and no eviction field: the - caller is not told that a cap or an eviction exists. The evicted - session's name or tag (never an mn_ id) and the sessions_evicted - counter are reported on admin serve_status only. + caller is not told that a cap or an eviction exists. The open and + load success results (CLI and MCP) carry no key matching cap, limit, + max_sessions, sessions_count or evict. The evicted session's name or + tag (never an mn_ id) and the sessions_evicted counter are reported + on admin serve_status only. Accepted: the limit_exceeded refusal + itself reveals that a cap exists. That refusal is the one + caller-visible signal and is not hidden. Settled (not open): a lease does not survive eviction; a load is a touch with a fresh TTL; admin and serve_status reads are not - touches; no default snapshot dir (no dir means the cap refuses); - one cap lock for count, pick and slot reservation; save outside - the cap lock, under the victim lock; no auto-drop of unsaveable - sessions, counted and surfaced. + touches; no default snapshot dir (no dir means the cap refuses; + MEMNET_EXPIRE_SNAPSHOT_DIR is reused, with MEMNET_SNAPSHOT_DIR as an + alias that must agree); one cap lock for count, pick and slot + reservation; save outside the cap lock, under the victim lock; the + victim keeps its slot until dropped and the picking open waits for + its save; no auto-drop of unsaveable sessions, counted and surfaced. + + Ship (one commit, PR-facing). The commit that ships the engine SHALL + in one change: (1) flip the module pytestmark in + tests/test_session_evict.py to strict=True or drop the xfail; (2) set + deploy CapsPolicy evictShipped=true; (3) add the deploy satisfy link + MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru; + (4) flip the status guards caps.evictShipped == true in + MN-VER-05-S03..S09. tests/test_sysml_session_evict.py::test_ship_flags_flip_together + fails until (1) to (3) agree; (4) is a manual step at the same commit. LATER (not dropped, not modelled): a "touched within the last N minutes" exemption. Do not add it until a measured run shows diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index ec9ad00b..60e45ad5 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -2411,11 +2411,16 @@ package MemNetVerification { doc /* MN-REQ-05.5 R4 (proposed) — cap full and no evictable candidate: refuse with code limit_exceeded and the message "all sessions are in use"; - nothing is dropped. No snapshot dir means refuse, no eviction. Concurrent - opens at cap=2 keep count <= cap with one victim per slot. + nothing is dropped. No snapshot dir means refuse, no eviction; with the + dir set the same full cap evicts (positive control). The snapshot dir + and its alias must agree or start refuses (config_conflict). Concurrent + opens at cap=2: the two opens that pick a victim each succeed, late + opens are refused while the victims are mid-save, count <= cap throughout. Runtime checks (xfail until shipped): tests/test_session_evict.py:: test_all_in_use_refusal_drops_nothing, + ::test_cap_full_with_snapshot_dir_evicts_oldest, ::test_no_snapshot_dir_refuses_without_eviction, + ::test_snapshot_dir_alias_conflict_refuses, ::test_cap_two_concurrent_opens_one_victim_per_slot. */ attribute verificationId : String = "MN-VER-05-S06"; @@ -2472,6 +2477,7 @@ package MemNetVerification { counter is checked by its deploy attribute, not here). Runtime checks (xfail until shipped): tests/test_session_evict.py:: test_caller_result_has_no_eviction_field, + ::test_open_and_load_results_carry_no_cap_fields, ::test_admin_report_names_victim_never_mn_id. */ attribute verificationId : String = "MN-VER-05-S08"; @@ -2501,6 +2507,7 @@ package MemNetVerification { shipped): tests/test_session_evict.py:: test_restore_keeps_rows_edges_and_acl, ::test_restore_carries_no_lease, + ::test_restore_lease_commit_fails_cleanly, ::test_reopen_restored_true_no_alerts, ::test_load_is_touch_with_fresh_ttl. */ diff --git a/tests/test_session_evict.py b/tests/test_session_evict.py index 4611c15c..a90b2fdb 100644 --- a/tests/test_session_evict.py +++ b/tests/test_session_evict.py @@ -28,9 +28,10 @@ from memnet.acl import acl_to_dict from memnet.admin_usage import build_report # noqa: F401 (admin read surface) from memnet.cli import app +from memnet.config import Caps from memnet.exceptions import MemNetError from memnet.mutate_gate import MutateGate -from memnet.neighbourhood_reserve import reserve +from memnet.neighbourhood_reserve import extend, reserve from memnet.registry import contains, count, get_entry from memnet.session import ( SessionStore, @@ -47,7 +48,8 @@ runner = CliRunner() ENV_MAX = "MEMNET_MAX_SESSIONS" -ENV_DIR = "MEMNET_EVICT_SNAPSHOT_DIR" +ENV_DIR = "MEMNET_EXPIRE_SNAPSHOT_DIR" # reused; no second eviction knob +ENV_ALIAS = "MEMNET_SNAPSHOT_DIR" # optional neutral alias; conflicting paths refuse start ENV_ADMIN = "MEMNET_ADMIN_TOKEN" ADMIN_TOKEN = "test-admin-token" # dummy value for the in-process admin read BASE = datetime(2026, 10, 20, 12, 0, tzinfo=UTC) @@ -69,6 +71,7 @@ def evict(memnet_temp, monkeypatch, tmp_path): snap_dir.mkdir() monkeypatch.setenv(ENV_MAX, "3") monkeypatch.setenv(ENV_DIR, str(snap_dir)) + monkeypatch.delenv(ENV_ALIAS, raising=False) set_now_override(BASE) return snap_dir @@ -106,6 +109,36 @@ def _serve_status_payload() -> dict: return json.loads(asyncio.run(serve_status())) +# Keys match by word or prefix: a segment starting with one of these names. +_CAP_KEY = re.compile(r"(^|_)(cap|limit|max_sessions|sessions_count|evict)") +# Raw text matches only these exact tokens, so ordinary words like "capacity" pass. +_CAP_TOKEN = re.compile(r"\b(max_sessions|sessions_count|evicted)\b") + + +def _keys_of(node) -> set[str]: + if isinstance(node, dict): + keys = set(node) + for value in node.values(): + keys |= _keys_of(value) + return keys + if isinstance(node, list): + keys: set[str] = set() + for item in node: + keys |= _keys_of(item) + return keys + return set() + + +def _assert_no_cap_text(text: str) -> None: + assert not _CAP_TOKEN.search(text.lower()), "open/load output must not name a cap or eviction" + + +def _assert_no_cap_fields(payload: dict) -> None: + bad = sorted(k for k in _keys_of(payload) if _CAP_KEY.search(k.lower())) + assert not bad, f"open/load result carries cap-like keys: {bad}" + _assert_no_cap_text(json.dumps(payload)) + + # --- S03: oldest-touch order and touch semantics ---------------------------- @@ -154,17 +187,53 @@ def test_victim_saved_before_drop_atomic_fsync(evict, schema_file, workflow_file _open(schema_file, 1) _open(schema_file, 2) victim = a.session_id - fsynced: list[int] = [] - real_fsync = os.fsync - - def counting_fsync(fd): - fsynced.append(fd) + snap_dir_stat = os.stat(evict) + snap_dir_real = os.path.realpath(evict) + events: list[str] = [] # kinds only; never a session id or path + real_fsync, real_replace, real_rename = os.fsync, os.replace, os.rename + real_drop, real_session_drop = registry_mod.remove_entry, session_mod.remove_entry + + def recording_fsync(fd): + st = os.fstat(fd) + if stat.S_ISDIR(st.st_mode): + same = st.st_ino == snap_dir_stat.st_ino and st.st_dev == snap_dir_stat.st_dev + events.append("dir_fsync_snap" if same else "dir_fsync_other") + elif stat.S_ISREG(st.st_mode): + events.append("file_fsync") return real_fsync(fd) - monkeypatch.setattr(os, "fsync", counting_fsync) + def wrap_rename(real): + def rename(src, dst, *args, **kwargs): + if os.path.realpath(os.path.dirname(os.fspath(dst))) == snap_dir_real: + events.append("rename_snap") + return real(src, dst, *args, **kwargs) + + return rename + + def wrap_drop(real): + def drop(*args, **kwargs): + events.append("drop") + return real(*args, **kwargs) + + return drop + + monkeypatch.setattr(os, "fsync", recording_fsync) + monkeypatch.setattr(os, "replace", wrap_rename(real_replace)) + monkeypatch.setattr(os, "rename", wrap_rename(real_rename)) + monkeypatch.setattr(registry_mod, "remove_entry", wrap_drop(real_drop)) + monkeypatch.setattr(session_mod, "remove_entry", wrap_drop(real_session_drop)) _open(schema_file, 4) assert not contains(victim) - assert len(fsynced) >= 2, "file and directory must both be fsynced" + + def step(kind: str, after: int) -> int: + idx = next((i for i in range(after, len(events)) if events[i] == kind), None) + assert idx is not None, f"no {kind} after step {after}: {events}" + return idx + + file_sync = step("file_fsync", 0) + renamed = step("rename_snap", file_sync) + dir_sync = step("dir_fsync_snap", renamed) + step("drop", dir_sync) # RAM drop only after the snapshot dir is fsynced snap = _snapshot_of(evict, victim) assert stat.S_IMODE(snap.stat().st_mode) == 0o600 leftovers = [p.name for p in evict.iterdir() if p != snap] @@ -283,22 +352,70 @@ def test_all_in_use_refusal_drops_nothing(evict, schema_file): assert not any(evict.iterdir()), "no snapshot may be written on refusal" +def test_cap_full_with_snapshot_dir_evicts_oldest(evict, schema_file): + # Positive control for the refusal test below: with the dir set, the same full cap evicts. + a = _open(schema_file, 0) + _open(schema_file, 1) + _open(schema_file, 2) + fresh = _open(schema_file, 4) + assert not contains(a.session_id), "oldest session must be evicted when the dir is set" + assert contains(fresh.session_id), "the fresh open must be live" + _snapshot_of(evict, a.session_id) # the victim's complete snapshot exists + + def test_no_snapshot_dir_refuses_without_eviction(evict, schema_file, monkeypatch): monkeypatch.delenv(ENV_DIR, raising=False) + monkeypatch.delenv(ENV_ALIAS, raising=False) ids = [_open(schema_file, m).session_id for m in (0, 1, 2)] with pytest.raises(MemNetError) as exc: _open(schema_file, 4) assert exc.value.code == "limit_exceeded" + assert "all sessions are in use" in exc.value.message assert all(contains(sid) for sid in ids), "no eviction without a snapshot dir" + for sid in ids: + assert get_session(sid).session_id == sid, "every existing session must stay live" + assert not any(evict.iterdir()), "no snapshot may be written without a dir" + + +def test_snapshot_dir_alias_conflict_refuses(tmp_path, monkeypatch): + same = tmp_path / "snaps" + same.mkdir() + other = tmp_path / "other" + monkeypatch.setenv(ENV_DIR, str(same)) + monkeypatch.setenv(ENV_ALIAS, str(same)) + Caps() # the same path under both names is accepted + monkeypatch.setenv(ENV_ALIAS, str(other)) + with pytest.raises(MemNetError) as exc: + Caps() + assert exc.value.code == "config_conflict", "two different snapshot dirs must refuse start" + assert str(same) not in exc.value.message and str(other) not in exc.value.message, ( + "the refusal must not name either path" + ) def test_cap_two_concurrent_opens_one_victim_per_slot(evict, schema_file, monkeypatch): monkeypatch.setenv(ENV_MAX, "2") a = _open(schema_file, 0) b = _open(schema_file, 1) - seeded = {a.session_id, b.session_id} + victims = {a.session_id, b.session_id} set_now_override(_at(30)) - barrier = threading.Barrier(4) + real_write = snapshot_mod.write_snapshot + picked: set[str] = set() + picked_lock = threading.Lock() + both_picked = threading.Event() + release = threading.Event() + + def held_write(ss, path, **kwargs): + # Each victim stays mid-save (slot still held) until the late opens have run. + if ss.session_id in victims: + with picked_lock: + picked.add(ss.session_id) + if len(picked) == len(victims): + both_picked.set() + release.wait(5) + return real_write(ss, path, **kwargs) + + monkeypatch.setattr(snapshot_mod, "write_snapshot", held_write) opened: list[SessionStore] = [] refused: list[MemNetError] = [] errors: list[Exception] = [] @@ -306,7 +423,6 @@ def test_cap_two_concurrent_opens_one_victim_per_slot(evict, schema_file, monkey stop = threading.Event() def worker(): - barrier.wait(5) try: opened.append(open_session(map_file=str(schema_file), ttl_minutes=600)) except MemNetError as exc: @@ -319,27 +435,43 @@ def sampler(): samples.append(count()) mon = threading.Thread(target=sampler) - threads = [threading.Thread(target=worker) for _ in range(4)] mon.start() - for t in threads: + pickers = [threading.Thread(target=worker) for _ in range(2)] + for t in pickers: t.start() - for t in threads: - t.join(10) - stop.set() - mon.join(5) + try: + assert both_picked.wait(5), "both victims must be picked and mid-save" + # Release window: victims are still live and mid-save, so the picking opens + # must not have returned a session yet, and the cap is still full. + assert count() == 2, "victims stay registered until their save and drop" + assert not opened, "a picking open must not return before its victim is dropped" + late = [threading.Thread(target=worker) for _ in range(2)] + for t in late: + t.start() + for t in late: + t.join(5) + # Late opens see no evictable session (both victims are evicting) and are refused + # at once, without queuing behind the victims' saves. + assert len(refused) == 2, "late opens must be refused while the victims are mid-save" + assert count() == 2 and not opened, "cap stays full and no open returns during the window" + finally: + release.set() + for t in pickers: + t.join(5) + stop.set() + mon.join(5) assert not errors, "only limit_exceeded refusals are allowed" - assert len(opened) + len(refused) == 4 - # Two victims exist and the cap lock serialises picks, so the first two opens always - # succeed. Later opens may be refused while both victims are mid-save (race-dependent). - assert len(opened) >= 2, "the first two opens each free one slot" + assert len(opened) == 2, "exactly the two opens that picked a victim succeed" + assert all(contains(s.session_id) for s in opened), ( + "each successful open is live after its drop" + ) assert all(e.code == "limit_exceeded" for e in refused) + assert all("all sessions are in use" in e.message for e in refused) assert samples and max(samples) <= 2, "count must never exceed the cap" assert count() == 2 - created = seeded | {s.session_id for s in opened} - evicted = {sid for sid in created if not contains(sid)} - assert len(evicted) == len(opened), "each successful open consumes exactly one victim" - assert len(list(evict.iterdir())) == len(evicted), "one snapshot per victim" + assert not any(contains(sid) for sid in victims), "each victim is dropped after its save" + assert len(list(evict.iterdir())) == 2, "one snapshot per victim" # --- S07: exemptions ---------------------------------------------------------- @@ -400,12 +532,16 @@ def test_reserve_lease_is_not_an_exemption(evict, schema_file, workflow_file): _seed(a.session_id, workflow_file) b = _open(schema_file, 1) _open(schema_file, 2) - holder = SessionStore(a.session_id) - reserve(holder.reserves, holder.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(3)) + live = get_session(a.session_id) + lease = reserve( + live.reserves, live.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(3) + ) + assert lease.rid in live.reserves.leases, "the lease must be held before eviction" _open(schema_file, 4) assert not contains(a.session_id), "a reserve lease alone does not exempt a session" assert contains(b.session_id) loaded = load_snapshot(_snapshot_of(evict, a.session_id)) + assert lease.rid not in loaded.reserves.leases, "the lease must be absent after load" assert loaded.reserves.leases == {}, "reserve leases do not survive eviction" @@ -423,6 +559,33 @@ def test_caller_result_has_no_eviction_field(evict, schema_file): assert "evict" not in text, "caller output must not mention eviction" +def test_open_and_load_results_carry_no_cap_fields(evict, schema_file, workflow_file): + from memnet_mcp.server import session_load, session_open + + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + b = _open(schema_file, 1) + _open(schema_file, 2) + set_now_override(_at(3)) + cli_open = runner.invoke(app, ["session", "open", "--map-file", str(schema_file)]) # evicts a + assert cli_open.exit_code == 0 + _assert_no_cap_text(cli_open.stdout + cli_open.stderr) + set_now_override(_at(4)) + mcp_open = json.loads(asyncio.run(session_open(map_file=str(schema_file)))) # evicts b + assert mcp_open["exit_code"] == 0, mcp_open + _assert_no_cap_fields(mcp_open) + set_now_override(_at(5)) + mcp_load = json.loads(asyncio.run(session_load(file=str(_snapshot_of(evict, a.session_id))))) + assert mcp_load["exit_code"] == 0, mcp_load + _assert_no_cap_fields(mcp_load) + set_now_override(_at(6)) + cli_load = runner.invoke( + app, ["session", "load", "--file", str(_snapshot_of(evict, b.session_id)), "--keep-id"] + ) + assert cli_load.exit_code == 0 + _assert_no_cap_text(cli_load.stdout + cli_load.stderr) + + def test_admin_report_names_victim_never_mn_id(evict, schema_file): a = _open(schema_file, 0) _open(schema_file, 1) @@ -464,19 +627,48 @@ def test_restore_carries_no_lease(evict, schema_file, workflow_file): _seed(a.session_id, workflow_file) victim = a.session_id SessionStore(victim).grant_caller("worker-1") - holder = SessionStore(victim) - reserve(holder.reserves, holder.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(0.5)) + live = get_session(victim) + lease = reserve( + live.reserves, live.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(0.5) + ) + assert lease.rid in live.reserves.leases, "the lease must be held before eviction" _open(schema_file, 1) _open(schema_file, 2) _open(schema_file, 4) # evicts a; a reserve lease alone does not exempt it snap = _snapshot_of(evict, victim) set_now_override(_at(5)) loaded = load_snapshot(snap) + assert lease.rid not in loaded.reserves.leases, "the lease must be absent after load" assert loaded.reserves.leases == {}, "restored session must carry no reserve leases" assert not (acl_to_dict(loaded.acl) or {}).get("bind"), "no bind may survive the restore" assert "worker-1" in loaded.acl.callers, "the ACL itself is kept" +def test_restore_lease_commit_fails_cleanly(evict, schema_file, workflow_file): + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + victim = a.session_id + live = get_session(victim) + lease = reserve( + live.reserves, live.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(0.5) + ) + assert lease.rid in live.reserves.leases, "the lease must be held before eviction" + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a while llm-1 holds a lease on PLR01 + set_now_override(_at(5)) + loaded = load_snapshot(_snapshot_of(evict, victim)) + assert lease.rid not in loaded.reserves.leases, "the lease must be absent after load" + rows_before = loaded.store.row_count_non_law() + wealth_before = loaded.store.get("PLR01").fields["wealth"] + # The engine's missing-reserve code: extend/release on a cleared lease raise reserve_expired. + with pytest.raises(MemNetError) as exc: + extend(loaded.reserves, rid=lease.rid, llm_id="llm-1") + assert exc.value.code == "reserve_expired", "a dropped lease must fail with reserve_expired" + assert loaded.store.row_count_non_law() == rows_before, "no partial write" + assert loaded.store.get("PLR01").fields["wealth"] == wealth_before, "PLR01 must be unchanged" + + def test_reopen_restored_true_no_alerts(evict, schema_file, capsys): a = _open(schema_file, 0) victim = a.session_id diff --git a/tests/test_sysml_session_evict.py b/tests/test_sysml_session_evict.py index a6b4be05..2d23c115 100644 --- a/tests/test_sysml_session_evict.py +++ b/tests/test_sysml_session_evict.py @@ -21,6 +21,9 @@ BEHAVIOUR = MODELS / "behaviour.sysml" RUNTIME = ROOT / "tests" / "test_session_evict.py" VER_IDS = [f"MN-VER-05-S0{n}" for n in range(3, 10)] +SATISFY_LINE = ( + r"^\s*satisfy\s+MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru\s*;" +) def _read(path: Path) -> str: @@ -86,18 +89,59 @@ def test_every_runtime_test_is_cited_by_a_verify_doc(): assert _runtime_test_names() == cited -def test_runtime_module_is_xfail_until_shipped(): - text = _read(RUNTIME) - assert "pytestmark = pytest.mark.xfail(" in text - assert 'reason="MN-REQ-05.5 not shipped; engine pending"' in text - assert "strict=False" in text +def _evict_shipped() -> bool: + found = re.findall(r"attribute evictShipped : Boolean = (true|false);", _read(DEPLOY)) + assert len(found) == 1, "deploy.sysml must declare evictShipped exactly once" + return found[0] == "true" -def test_deploy_satisfy_not_linked_while_not_shipped(): - text = _read(DEPLOY) - satisfy = "satisfy MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru" - assert satisfy not in text - assert "attribute evictShipped : Boolean = false;" in text +def _satisfy_linked() -> bool: + return re.search(SATISFY_LINE, _read(DEPLOY), re.M) is not None + + +def _xfail_mark() -> tuple[bool, bool | None]: + """Whether the runtime module carries an xfail pytestmark, and its strict value.""" + for node in ast.parse(_read(RUNTIME)).body: + if not ( + isinstance(node, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == "pytestmark" for t in node.targets) + ): + continue + marks = node.value.elts if isinstance(node.value, ast.List) else [node.value] + for mark in marks: + if isinstance(mark, ast.Call) and ast.unparse(mark.func) == "pytest.mark.xfail": + strict = next( + (ast.literal_eval(kw.value) for kw in mark.keywords if kw.arg == "strict"), + None, + ) + return True, strict + return False, None + + +def _status_guards() -> dict[str, list[bool]]: + """Per MN-VER-05-S03..S09 def, the evictShipped value its status guard requires.""" + guards: dict[str, list[bool]] = {} + for block in re.split(r"(?=verification def )", _read(VERIFY)): + ver = re.search(r'attribute verificationId : String = "(MN-VER-05-S0\d)";', block) + if ver and ver.group(1) in VER_IDS: + found = re.findall(r"\.evictShipped\s*==\s*(true|false)", block) + guards[ver.group(1)] = [v == "true" for v in found] + return guards + + +def test_ship_flags_flip_together(): + shipped = _evict_shipped() + linked = _satisfy_linked() + has_xfail, strict = _xfail_mark() + not_shipped = not shipped and not linked and has_xfail and strict is False + shipped_ok = shipped and linked and (not has_xfail or strict is True) + assert not_shipped or shipped_ok, ( + "evictShipped, the deploy satisfy link and the runtime xfail mark must flip together" + ) + guards = _status_guards() + assert set(guards) == set(VER_IDS), "every MN-VER-05-S03..S09 def must carry a status guard" + for ver_id, values in guards.items(): + assert values == [shipped], f"{ver_id} evictShipped guard must match the deploy value" def test_evict_saving_closes_only_on_evict_saved(): From dd11ba23494853b4c5adfaa4263d1d95f657ec3c Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:19:19 +0800 Subject: [PATCH 4/7] model: MN-REQ-05.5 lease_lost on commit naming a lost lease; CLI key check note; ship doc; operator doc + changelog --- CHANGELOG.md | 3 ++ docs/operations/one-session-per-document.md | 2 + sysml-models/models/deploy.sysml | 6 +++ sysml-models/models/requirements.sysml | 17 +++++++-- sysml-models/models/verify.sysml | 14 +++++-- tests/test_session_evict.py | 41 ++++++++++++++++----- tests/test_sysml_session_evict.py | 26 +++++++++---- 7 files changed, 87 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5110abdc..20dfcf55 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,9 @@ This project uses Semantic Versioning as **interpreted for MemNet**: package `a. - **Invent only — ClusterRoute vs SliceHandCarry (#191 / #47 cousin)** — `MemNetTwoMoves` outside `MemNetSystem` (`MN-REQ-06.9` + `MN-REQ-06.10` / `MN-VER-06-S08`). ClusterRoute = where the session lives (`MemNetLanMcpFront`; one owner; `pin_map` / `find` SHALL NOT span backends). SliceHandCarry = explicit copy into another session (`export_pin_map` or `session_save` → LAN file copy → dest import/`session_load`; `import_slice` same-serve only). Not a live hop. `import_slice(from_url)` not shipped. tip≠face. `inventOnly=true`; `implemented=false`; no engine code; no SemVer bump. Wire: [`docs/operations/cluster-route-vs-slice-hand-carry.md`](docs/operations/cluster-route-vs-slice-hand-carry.md). - **Invent only — LAN MCP front over several serves (#191)** — `MemNetLanMcpFront` outside `MemNetSystem` (`MN-REQ-06.9` / `MN-VER-06-S07`). One MCP catalogue, N LAN `memnet serve` backends; `SessionOwnerRegistry` is owner (explicit pin allowed; silent hash is not sole routing). One owner per session; `pin_map` / `find` SHALL NOT span backends. Cousin of #47 (peer sid handoff), not the same invent. tip≠face. `inventOnly=true`; `implemented=false`; no engine code; no SemVer bump. Wire: [`docs/operations/memnet-lan-mcp-front.md`](docs/operations/memnet-lan-mcp-front.md). +### Proposed (not shipped) +- **Session cap LRU evict (MN-REQ-05.5)** — at `MEMNET_MAX_SESSIONS`, the least-recently-touched saveable session is saved to `MEMNET_EXPIRE_SNAPSHOT_DIR` and then dropped; the dir enables eviction writes even with save-on-expire off. No dir refuses `limit_exceeded`. Restore keeps ACL, drops leases. A commit naming a dropped lease is refused `lease_lost` (new mutate arg `rid=`; nothing written; not a touch). Deploy `evictShipped=false` and `commitRefusesLostLease=false`; the runtime tests in `tests/test_session_evict.py` are xfail until the engine ships. Verify: MN-VER-05-S03..S09. + ## [0.19.25] - 2026-10-14 ### Changed diff --git a/docs/operations/one-session-per-document.md b/docs/operations/one-session-per-document.md index 5b1bbeb7..4c8165c6 100644 --- a/docs/operations/one-session-per-document.md +++ b/docs/operations/one-session-per-document.md @@ -21,6 +21,8 @@ Settings this gate uses: | Concurrent sessions | 1024 (`MEMNET_MAX_SESSIONS`) | | Document size | about 1 800 part nodes plus a few opaque `USR` text nodes | +**Proposed, not shipped (MN-REQ-05.5):** once the session cap eviction ships, setting `MEMNET_EXPIRE_SNAPSHOT_DIR` also enables eviction snapshot writes, even with `MEMNET_SAVE_ON_EXPIRE` off. When the cap is full, the least-recently-touched saveable session is written to `{dir}/{sid}.snap` and then dropped; the dir is the one knob (`MEMNET_SNAPSHOT_DIR` may be set as an alias, and conflicting paths refuse start). With no dir set, a full cap refuses `limit_exceeded` and drops nothing. The table above is the shipped behaviour until then. + Ingest caps (`max_nodes=2000` / `max_edges=2000`) are Path-B ingest, not this mutate path. Session row cap remains 5000 non-LAW rows (**nodes plus edges**). `session load` of a snapshot is **not** bound by ingest budget; it walks leftover `parse_line` + `MemStore.upsert` (`MEMNET_MAX_ROWS`, max sessions, leftover value/line/`FIELD_COUNT` on a malformed pipe line). ## Request envelope (direct serve) diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index 424839ae..5da1434f 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -188,6 +188,12 @@ package MemNet { attribute evictLoadFreshTtl : Boolean = true; // test_load_is_touch_with_fresh_ttl attribute evictKeepsAclNoLease : Boolean = true; // test_restore_carries_no_lease attribute evictRestoreLeaseCommitFails : Boolean = true; // test_restore_lease_commit_fails_cleanly + // MN-REQ-05.5 lost lease: a commit naming a rid the caller no longer holds + // is refused lease_lost, nothing written, not a touch. Proposed, not shipped + // (new mutate wire arg rid=). Flips with evictShipped at the ship commit; + // test_ship_flags_flip_together enforces it. Runtime check is + // tests/test_session_evict.py::test_restore_lease_commit_fails_cleanly. + attribute commitRefusesLostLease : Boolean = false; attribute maxDepth : Integer = 4; attribute defaultQueryMaxRows : Integer = 50; attribute defaultQueryDepth : Integer = 2; diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index 8287bc6d..1f150cc6 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -829,6 +829,14 @@ package MemNetRequirements { a fresh TTL. The reopened session returns restored=true and emits no alerts. + Lost lease. A commit naming a lease the caller no longer holds SHALL + be refused with code lease_lost; nothing is written; the refused + commit is not a touch. The commit names the held reserve with the + new wire arg rid (MCP mutate rid=, CLI mutate --rid), and llm_id + names the holder. lease= is not this arg: it stays the SessionBind + lease (MN-REQ-06.16). The arg is new and not shipped + (deploy commitRefusesLostLease=false). + Caller. The caller result carries no cap and no eviction field: the caller is not told that a cap or an eviction exists. The open and load success results (CLI and MCP) carry no key matching cap, limit, @@ -850,11 +858,14 @@ package MemNetRequirements { Ship (one commit, PR-facing). The commit that ships the engine SHALL in one change: (1) flip the module pytestmark in tests/test_session_evict.py to strict=True or drop the xfail; (2) set - deploy CapsPolicy evictShipped=true; (3) add the deploy satisfy link + deploy CapsPolicy evictShipped=true and commitRefusesLostLease=true; + (3) add the deploy satisfy link MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru; (4) flip the status guards caps.evictShipped == true in - MN-VER-05-S03..S09. tests/test_sysml_session_evict.py::test_ship_flags_flip_together - fails until (1) to (3) agree; (4) is a manual step at the same commit. + MN-VER-05-S03..S09 and caps.commitRefusesLostLease == true in + MN-VER-05-S09. tests/test_sysml_session_evict.py::test_ship_flags_flip_together + enforces (1) to (4): it fails unless evictShipped, commitRefusesLostLease, + the satisfy link and the xfail mark all agree, and every guard matches. LATER (not dropped, not modelled): a "touched within the last N minutes" exemption. Do not add it until a measured run shows diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index 60e45ad5..fd43a4b3 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -2503,8 +2503,12 @@ package MemNetVerification { session from its snapshot: same ACL, no lease carried over (reserve leases dropped; the restored session has no bind). The load is a touch with a fresh TTL; the reopened session returns restored=true and - emits no alerts. Rows and edges survive. Runtime checks (xfail until - shipped): tests/test_session_evict.py:: + emits no alerts. Rows and edges survive. A commit that names the dropped + lease (mutate rid=, llm_id) is refused lease_lost: row, field, row count, + snapshot bytes and mtime, and last touch are all unchanged; the refused + commit is not a touch. Gated by deploy caps.commitRefusesLostLease + (= evictShipped). Runtime checks (xfail until shipped): + tests/test_session_evict.py:: test_restore_keeps_rows_edges_and_acl, ::test_restore_carries_no_lease, ::test_restore_lease_commit_fails_cleanly, @@ -2518,7 +2522,7 @@ package MemNetVerification { objective sessionCapEvictLoadRestores { doc /* Runtime: tests/test_session_evict.py (restore fidelity, ACL, no lease, - restored flag, fresh TTL). Status guard only below. + restored flag, fresh TTL, lost-lease refusal). Status guards only below. */ verify sessionCapEvictLruReq; verify loadSessionSnapshotReq; @@ -2527,6 +2531,10 @@ package MemNetVerification { system.core.transport.inProcess.memory.sessions.caps .evictShipped == false } + require constraint { + system.core.transport.inProcess.memory.sessions.caps + .commitRefusesLostLease == false + } } } diff --git a/tests/test_session_evict.py b/tests/test_session_evict.py index a90b2fdb..71ad77cc 100644 --- a/tests/test_session_evict.py +++ b/tests/test_session_evict.py @@ -31,7 +31,7 @@ from memnet.config import Caps from memnet.exceptions import MemNetError from memnet.mutate_gate import MutateGate -from memnet.neighbourhood_reserve import extend, reserve +from memnet.neighbourhood_reserve import reserve from memnet.registry import contains, count, get_entry from memnet.session import ( SessionStore, @@ -569,6 +569,8 @@ def test_open_and_load_results_carry_no_cap_fields(evict, schema_file, workflow_ set_now_override(_at(3)) cli_open = runner.invoke(app, ["session", "open", "--map-file", str(schema_file)]) # evicts a assert cli_open.exit_code == 0 + # CLI session open/load print wire lines, not JSON (only `version --json` does), + # so the CLI side is checked by text token; the MCP side checks keys. _assert_no_cap_text(cli_open.stdout + cli_open.stderr) set_now_override(_at(4)) mcp_open = json.loads(asyncio.run(session_open(map_file=str(schema_file)))) # evicts b @@ -645,6 +647,10 @@ def test_restore_carries_no_lease(evict, schema_file, workflow_file): def test_restore_lease_commit_fails_cleanly(evict, schema_file, workflow_file): + # Real write path: MCP mutate (in-process), the same call an agent makes. + # The wire names the dropped reserve as rid= and its holder as llm_id=. + from memnet_mcp.server import mutate + a = _open(schema_file, 0) _seed(a.session_id, workflow_file) victim = a.session_id @@ -656,17 +662,34 @@ def test_restore_lease_commit_fails_cleanly(evict, schema_file, workflow_file): _open(schema_file, 1) _open(schema_file, 2) _open(schema_file, 4) # evicts a while llm-1 holds a lease on PLR01 + snap = _snapshot_of(evict, victim) set_now_override(_at(5)) - loaded = load_snapshot(_snapshot_of(evict, victim)) + loaded = load_snapshot(snap, keep_id=True) # same id back, live, no lease assert lease.rid not in loaded.reserves.leases, "the lease must be absent after load" + snap_bytes = snap.read_bytes() + snap_mtime = snap.stat().st_mtime_ns rows_before = loaded.store.row_count_non_law() - wealth_before = loaded.store.get("PLR01").fields["wealth"] - # The engine's missing-reserve code: extend/release on a cleared lease raise reserve_expired. - with pytest.raises(MemNetError) as exc: - extend(loaded.reserves, rid=lease.rid, llm_id="llm-1") - assert exc.value.code == "reserve_expired", "a dropped lease must fail with reserve_expired" - assert loaded.store.row_count_non_law() == rows_before, "no partial write" - assert loaded.store.get("PLR01").fields["wealth"] == wealth_before, "PLR01 must be unchanged" + fields_before = dict(loaded.store.get("PLR01").fields) + touch_before = get_entry(victim).meta.modified_at + + set_now_override(_at(6)) + res = json.loads( + asyncio.run( + mutate( + wire_lines=["MATCH (n {id: 'PLR01'}) SET n.wealth = 999"], + session=victim, + llm_id="llm-1", + rid=lease.rid, + ) + ) + ) + assert res["exit_code"] != 0, "a commit naming a dropped lease must be refused" + assert "@ERR: lease_lost|" in res["stderr"], "the refusal must carry code lease_lost" + assert loaded.store.row_count_non_law() == rows_before, "no row may be added or dropped" + assert dict(loaded.store.get("PLR01").fields) == fields_before, "PLR01 must be unchanged" + assert snap.read_bytes() == snap_bytes, "the snapshot file must not be rewritten" + assert snap.stat().st_mtime_ns == snap_mtime, "the snapshot mtime must not move" + assert get_entry(victim).meta.modified_at == touch_before, "a refused commit is not a touch" def test_reopen_restored_true_no_alerts(evict, schema_file, capsys): diff --git a/tests/test_sysml_session_evict.py b/tests/test_sysml_session_evict.py index 2d23c115..28a160fe 100644 --- a/tests/test_sysml_session_evict.py +++ b/tests/test_sysml_session_evict.py @@ -89,12 +89,16 @@ def test_every_runtime_test_is_cited_by_a_verify_doc(): assert _runtime_test_names() == cited -def _evict_shipped() -> bool: - found = re.findall(r"attribute evictShipped : Boolean = (true|false);", _read(DEPLOY)) - assert len(found) == 1, "deploy.sysml must declare evictShipped exactly once" +def _deploy_flag(name: str) -> bool: + found = re.findall(rf"attribute {name} : Boolean = (true|false);", _read(DEPLOY)) + assert len(found) == 1, f"deploy.sysml must declare {name} exactly once" return found[0] == "true" +def _evict_shipped() -> bool: + return _deploy_flag("evictShipped") + + def _satisfy_linked() -> bool: return re.search(SATISFY_LINE, _read(DEPLOY), re.M) is not None @@ -118,14 +122,15 @@ def _xfail_mark() -> tuple[bool, bool | None]: return False, None -def _status_guards() -> dict[str, list[bool]]: - """Per MN-VER-05-S03..S09 def, the evictShipped value its status guard requires.""" +def _status_guards(flag: str = "evictShipped") -> dict[str, list[bool]]: + """Per MN-VER-05-S03..S09 def, the value of ``flag`` its status guard requires.""" guards: dict[str, list[bool]] = {} for block in re.split(r"(?=verification def )", _read(VERIFY)): ver = re.search(r'attribute verificationId : String = "(MN-VER-05-S0\d)";', block) if ver and ver.group(1) in VER_IDS: - found = re.findall(r"\.evictShipped\s*==\s*(true|false)", block) - guards[ver.group(1)] = [v == "true" for v in found] + found = re.findall(rf"\.{flag}\s*==\s*(true|false)", block) + if found: + guards[ver.group(1)] = [v == "true" for v in found] return guards @@ -138,10 +143,17 @@ def test_ship_flags_flip_together(): assert not_shipped or shipped_ok, ( "evictShipped, the deploy satisfy link and the runtime xfail mark must flip together" ) + assert _deploy_flag("commitRefusesLostLease") == shipped, ( + "commitRefusesLostLease must flip with evictShipped (both false now, both true at ship)" + ) guards = _status_guards() assert set(guards) == set(VER_IDS), "every MN-VER-05-S03..S09 def must carry a status guard" for ver_id, values in guards.items(): assert values == [shipped], f"{ver_id} evictShipped guard must match the deploy value" + lost_lease = _status_guards("commitRefusesLostLease") + assert lost_lease == {"MN-VER-05-S09": [shipped]}, ( + "MN-VER-05-S09 must guard commitRefusesLostLease against the deploy value" + ) def test_evict_saving_closes_only_on_evict_saved(): From 35e70b7b37599436950caf5a01f0485c195c07d2 Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:25:47 +0800 Subject: [PATCH 5/7] model: MN-REQ-05.5 no-rid mutate unchanged + regression test; narrower lost-lease claim; modified_at touch field; reserved on other-llm rid --- CHANGELOG.md | 2 +- sysml-models/models/deploy.sysml | 1 - sysml-models/models/requirements.sysml | 20 ++++++- sysml-models/models/verify.sysml | 12 +++-- tests/test_mutate_no_rid_regression.py | 52 ++++++++++++++++++ tests/test_session_evict.py | 73 +++++++++++++++++++++++++- 6 files changed, 151 insertions(+), 9 deletions(-) create mode 100644 tests/test_mutate_no_rid_regression.py diff --git a/CHANGELOG.md b/CHANGELOG.md index 20dfcf55..0b19dc8a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,7 +12,7 @@ This project uses Semantic Versioning as **interpreted for MemNet**: package `a. - **Invent only — LAN MCP front over several serves (#191)** — `MemNetLanMcpFront` outside `MemNetSystem` (`MN-REQ-06.9` / `MN-VER-06-S07`). One MCP catalogue, N LAN `memnet serve` backends; `SessionOwnerRegistry` is owner (explicit pin allowed; silent hash is not sole routing). One owner per session; `pin_map` / `find` SHALL NOT span backends. Cousin of #47 (peer sid handoff), not the same invent. tip≠face. `inventOnly=true`; `implemented=false`; no engine code; no SemVer bump. Wire: [`docs/operations/memnet-lan-mcp-front.md`](docs/operations/memnet-lan-mcp-front.md). ### Proposed (not shipped) -- **Session cap LRU evict (MN-REQ-05.5)** — at `MEMNET_MAX_SESSIONS`, the least-recently-touched saveable session is saved to `MEMNET_EXPIRE_SNAPSHOT_DIR` and then dropped; the dir enables eviction writes even with save-on-expire off. No dir refuses `limit_exceeded`. Restore keeps ACL, drops leases. A commit naming a dropped lease is refused `lease_lost` (new mutate arg `rid=`; nothing written; not a touch). Deploy `evictShipped=false` and `commitRefusesLostLease=false`; the runtime tests in `tests/test_session_evict.py` are xfail until the engine ships. Verify: MN-VER-05-S03..S09. +- **Session cap LRU evict (MN-REQ-05.5)** — at `MEMNET_MAX_SESSIONS`, the least-recently-touched saveable session is saved to `MEMNET_EXPIRE_SNAPSHOT_DIR` and then dropped; the dir enables eviction writes even with save-on-expire off. No dir refuses `limit_exceeded`. Restore keeps ACL, drops leases. A commit naming a dropped lease is refused `lease_lost` (new mutate arg `rid=`; nothing written; not a touch). A `rid=` naming another llm_id's live lease is refused `reserved` (existing reserve code); a commit with no `rid=` is unchanged. Deploy `evictShipped=false` and `commitRefusesLostLease=false`; the runtime tests in `tests/test_session_evict.py` are xfail until the engine ships. Verify: MN-VER-05-S03..S09. ## [0.19.25] - 2026-10-14 diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index 5da1434f..217217b2 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -187,7 +187,6 @@ package MemNet { attribute evictReopenRestoredTrue : Boolean = true; // test_reopen_restored_true_no_alerts attribute evictLoadFreshTtl : Boolean = true; // test_load_is_touch_with_fresh_ttl attribute evictKeepsAclNoLease : Boolean = true; // test_restore_carries_no_lease - attribute evictRestoreLeaseCommitFails : Boolean = true; // test_restore_lease_commit_fails_cleanly // MN-REQ-05.5 lost lease: a commit naming a rid the caller no longer holds // is refused lease_lost, nothing written, not a touch. Proposed, not shipped // (new mutate wire arg rid=). Flips with evictShipped at the ship commit; diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index 1f150cc6..ebc9b6e1 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -777,6 +777,8 @@ package MemNetRequirements { session lock. Victim. The live, non-evicting session with the oldest last touch. + The last-touch field is SessionMeta.modified_at (set by + SessionStore.touch); the victim pick and the tests read this one field. A touch is any read or write through the session (get_session, mutate, read, load). Admin and serve_status reads are NOT touches. A fresh open cannot be its own victim: its session is not in the @@ -837,6 +839,17 @@ package MemNetRequirements { lease (MN-REQ-06.16). The arg is new and not shipped (deploy commitRefusesLostLease=false). + A rid naming a live lease held by a different llm_id SHALL be refused + with the existing code reserved (MutateGate reserve check, + check_mutate_ids). reserve_conflict is the acquire-side overlap code + and is not used on commit. Not lease_lost: the lease is still live. + + A commit that names no rid SHALL behave exactly as today: the + MN-REQ-12.13 reserve check is unchanged (no_llm_id or reserved on a + leased row). lease_lost fires only when a rid is named, so a no-rid + commit after eviction and reload succeeds and changes the field. + Regression, not xfail: tests/test_mutate_no_rid_regression.py. + Caller. The caller result carries no cap and no eviction field: the caller is not told that a cap or an eviction exists. The open and load success results (CLI and MCP) carry no key matching cap, limit, @@ -872,12 +885,17 @@ package MemNetRequirements { reload-thrash at cap=3: cycle opens over 4 or more live sessions and count evict-then-reload inside a short interval. + LATER (not dropped, not modelled): "require rid on leased rows" (a + no-rid commit on a leased row refused). Not a rule; add only if a + measured run shows a lost-holder write slipping past the reserve check. + Open items (doc only, not rules yet): (a) a distinct session_evicted refusal for a caller who holds an evicted id; (b) whether session_load of an evicted id returns the same id. Verify: runtime tests in tests/test_session_evict.py, cited by - MN-VER-05-S03 to MN-VER-05-S09. + MN-VER-05-S03 to MN-VER-05-S09. Regression for the no-rid rule (not + xfail): tests/test_mutate_no_rid_regression.py. */ attribute requirementId : String = "MN-REQ-05.5"; } diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index fd43a4b3..8d2a51b9 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -2505,13 +2505,17 @@ package MemNetVerification { touch with a fresh TTL; the reopened session returns restored=true and emits no alerts. Rows and edges survive. A commit that names the dropped lease (mutate rid=, llm_id) is refused lease_lost: row, field, row count, - snapshot bytes and mtime, and last touch are all unchanged; the refused - commit is not a touch. Gated by deploy caps.commitRefusesLostLease - (= evictShipped). Runtime checks (xfail until shipped): - tests/test_session_evict.py:: + snapshot bytes and mtime, and last touch (SessionMeta.modified_at) are + all unchanged; the refused commit is not a touch. A rid naming a live + lease held by another llm_id is refused reserved (existing code). A + commit with no rid after eviction and reload succeeds. Gated by deploy + caps.commitRefusesLostLease (= evictShipped). Runtime checks (xfail until + shipped): tests/test_session_evict.py:: test_restore_keeps_rows_edges_and_acl, ::test_restore_carries_no_lease, ::test_restore_lease_commit_fails_cleanly, + ::test_no_rid_commit_after_evict_and_reload_succeeds, + ::test_rid_held_by_other_llm_refused_reserved, ::test_reopen_restored_true_no_alerts, ::test_load_is_touch_with_fresh_ttl. */ diff --git a/tests/test_mutate_no_rid_regression.py b/tests/test_mutate_no_rid_regression.py new file mode 100644 index 00000000..d648e0a3 --- /dev/null +++ b/tests/test_mutate_no_rid_regression.py @@ -0,0 +1,52 @@ +"""Mutate without rid behaves exactly as today (MN-REQ-12.13 reserve check unchanged). + +Regression guard for MN-REQ-05.5 "Lost lease": the new rid= arg is additive. +A commit that names no rid keeps the existing reserve rule. Not xfail: these +pass on the shipped engine and must keep passing after the eviction engine ships. +""" + +from __future__ import annotations + +import asyncio +import json + +from memnet.mutate_gate import MutateGate +from memnet.neighbourhood_reserve import reserve +from memnet.session import open_session +from memnet_mcp.server import mutate + +_PLR = ( + "CREATE (:PLR {id: 'PLR01', identity: 'Hero', wealth: 1, cashflow: 0, " + "monopoly: 0, reputation: 0, inventory: 'bag'})" +) +_PATCH = "MATCH (n {id: 'PLR01'}) SET n.wealth = 999" + + +def _commit(**kwargs) -> dict: + return json.loads(asyncio.run(mutate(wire_lines=[_PATCH], **kwargs))) + + +def test_no_rid_mutate_without_leases_succeeds(memnet_temp, schema_file): + ss = open_session(map_file=str(schema_file)) + MutateGate(ss).apply([_PLR], mode="add") + + res = _commit(session=ss.session_id) + + assert res["exit_code"] == 0, res["stderr"] + assert ss.store.get("PLR01").fields["wealth"] == "999" + + +def test_no_rid_mutate_on_leased_row_follows_reserve_rule(memnet_temp, schema_file): + ss = open_session(map_file=str(schema_file)) + MutateGate(ss).apply([_PLR], mode="add") + reserve(ss.reserves, ss.store, anchor="PLR01", llm_id="llm-1", ttl_s=600) + + other = _commit(session=ss.session_id, llm_id="llm-2") + assert other["exit_code"] != 0 + assert "@ERR: reserved|" in other["stderr"], "another llm_id is refused by the reserve check" + + anonymous = _commit(session=ss.session_id) + assert anonymous["exit_code"] != 0 + assert "@ERR: no_llm_id|" in anonymous["stderr"], "no llm_id on a leased row is refused" + + assert ss.store.get("PLR01").fields["wealth"] == "1", "a refused commit writes nothing" diff --git a/tests/test_session_evict.py b/tests/test_session_evict.py index 71ad77cc..cfb1f222 100644 --- a/tests/test_session_evict.py +++ b/tests/test_session_evict.py @@ -86,6 +86,11 @@ def _touch(sid: str, minute: float) -> SessionStore: return get_session(sid) +def _last_touch(sid: str): + """Last touch is SessionMeta.modified_at, the field SessionStore.touch sets.""" + return get_entry(sid).meta.modified_at + + def _seed(sid: str, workflow) -> None: """Write rows and edges through the CLI add path (a real write).""" r = runner.invoke(app, ["add", "--file", str(workflow), "--session", sid]) @@ -670,7 +675,7 @@ def test_restore_lease_commit_fails_cleanly(evict, schema_file, workflow_file): snap_mtime = snap.stat().st_mtime_ns rows_before = loaded.store.row_count_non_law() fields_before = dict(loaded.store.get("PLR01").fields) - touch_before = get_entry(victim).meta.modified_at + touch_before = _last_touch(victim) set_now_override(_at(6)) res = json.loads( @@ -689,7 +694,71 @@ def test_restore_lease_commit_fails_cleanly(evict, schema_file, workflow_file): assert dict(loaded.store.get("PLR01").fields) == fields_before, "PLR01 must be unchanged" assert snap.read_bytes() == snap_bytes, "the snapshot file must not be rewritten" assert snap.stat().st_mtime_ns == snap_mtime, "the snapshot mtime must not move" - assert get_entry(victim).meta.modified_at == touch_before, "a refused commit is not a touch" + assert _last_touch(victim) == touch_before, "a refused commit is not a touch" + + +def test_no_rid_commit_after_evict_and_reload_succeeds(evict, schema_file, workflow_file): + # lease_lost fires only when a rid is named. The reload drops the lease, so a + # commit with no rid and no live lease is a plain commit and must succeed. + from memnet_mcp.server import mutate + + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + victim = a.session_id + live = get_session(victim) + reserve(live.reserves, live.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(0.5)) + _open(schema_file, 1) + _open(schema_file, 2) + _open(schema_file, 4) # evicts a while llm-1 holds a lease on PLR01 + snap = _snapshot_of(evict, victim) + set_now_override(_at(5)) + loaded = load_snapshot(snap, keep_id=True) + assert loaded.reserves.leases == {}, "the reload must carry no lease" + + set_now_override(_at(6)) + res = json.loads( + asyncio.run( + mutate( + wire_lines=["MATCH (n {id: 'PLR01'}) SET n.wealth = 999"], + session=victim, + llm_id="llm-1", + ) + ) + ) + assert res["exit_code"] == 0, "a commit with no rid must succeed after eviction and reload" + assert get_session(victim).store.get("PLR01").fields["wealth"] == "999", "the field must change" + + +def test_rid_held_by_other_llm_refused_reserved(evict, schema_file, workflow_file): + # A rid naming a live lease held by another llm_id hits the existing reserve + # refusal (code reserved, MutateGate check_mutate_ids), not lease_lost. + from memnet_mcp.server import mutate + + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + victim = a.session_id + live = get_session(victim) + lease = reserve( + live.reserves, live.store, anchor="PLR01", llm_id="llm-1", ttl_s=600, now=_at(0.5) + ) + fields_before = dict(live.store.get("PLR01").fields) + touch_before = _last_touch(victim) + + set_now_override(_at(1)) + res = json.loads( + asyncio.run( + mutate( + wire_lines=["MATCH (n {id: 'PLR01'}) SET n.wealth = 999"], + session=victim, + llm_id="llm-2", + rid=lease.rid, + ) + ) + ) + assert res["exit_code"] != 0, "llm-2 must not commit under llm-1's live lease" + assert "@ERR: reserved|" in res["stderr"], "the refusal must carry code reserved" + assert dict(live.store.get("PLR01").fields) == fields_before, "PLR01 must be unchanged" + assert _last_touch(victim) == touch_before, "a refused commit is not a touch" def test_reopen_restored_true_no_alerts(evict, schema_file, capsys): From 80e259bdeceeb52ed04f536c5c2b4143149b5ff9 Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 22:45:53 +0800 Subject: [PATCH 6/7] model: MN-REQ-05.5 reads are touches (surface lists + sync), touch_seq tie order, regression + xfail tests --- sysml-models/models/deploy.sysml | 6 + sysml-models/models/requirements.sysml | 73 ++++++++- sysml-models/models/verify.sysml | 19 ++- tests/test_read_touch_regression.py | 55 +++++++ tests/test_session_evict.py | 217 ++++++++++++++++++++++++- tests/test_sysml_session_evict.py | 154 +++++++++++++++++- 6 files changed, 504 insertions(+), 20 deletions(-) create mode 100644 tests/test_read_touch_regression.py diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index 217217b2..31e28628 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -170,6 +170,12 @@ package MemNet { attribute evictPicksOldestTouch : Boolean = true; // test_evicts_oldest_touched_first attribute evictTouchOnReadOrWrite : Boolean = true; // test_reads_and_writes_are_touches attribute evictAdminReadsNotTouch : Boolean = true; // test_admin_and_serve_status_reads_are_not_touches + // Tie order (MN-REQ-05.5): pick is (modified_at, touch_seq). touch_seq is a + // process-wide monotonic counter on SessionEntry, not persisted in snapshots + // (a load is a fresh touch). Name-then-id fallback is unused: the counter is held. + // Both tie tests: test_tie_touch_order_a_then_b_evicts_a, test_tie_touch_order_b_then_a_evicts_b + attribute touchSeqMonotonic : Boolean = true; + attribute touchSeqInSnapshot : Boolean = false; // test_touch_seq_not_in_snapshot_fresh_on_load attribute evictSavesFirstFsync : Boolean = true; // test_victim_saved_before_drop_atomic_fsync attribute evictVictimLockHeld : Boolean = true; // test_victim_lock_held_from_pick_through_drop attribute evictOneCapLock : Boolean = true; // test_cap_two_concurrent_opens_one_victim_per_slot diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index ebc9b6e1..ae2c4cb6 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -769,6 +769,17 @@ package MemNetRequirements { Proposed, not shipped (engine pending). Runtime checks: tests/test_session_evict.py (xfail until the engine ships). + State (checked at 0.19.25 source). Session-scoped CLI commands + call _load_session, which calls ss.touch(). So the MCP reads + pin_map, query_warm, find, query_walk, read_list, export_pin_map, + housekeep_stats and session_current already touch today, and so do + the CLI-only reads (session_resume calls ss.touch() itself). The + in-process get_session() only extends the TTL and does NOT touch: + a read through get_session() alone leaves modified_at unchanged + today. That is the gap the touch rule below closes. session_list, + serve_status and the admin commands do not touch. session_save + writes a file and does not touch; it is not a read surface. + Cap. At session open or load, after purge_expired, when the count reaches MEMNET_MAX_SESSIONS (default 1024) the engine SHALL pick at most one victim. One cap lock SHALL cover the count, the victim pick @@ -776,11 +787,63 @@ package MemNetRequirements { lock. The save then runs outside the cap lock, under the victim's session lock. - Victim. The live, non-evicting session with the oldest last touch. - The last-touch field is SessionMeta.modified_at (set by - SessionStore.touch); the victim pick and the tests read this one field. - A touch is any read or write through the session (get_session, - mutate, read, load). Admin and serve_status reads are NOT touches. + Victim. The live, non-evicting session with the oldest last touch, + ordered by (modified_at, touch_seq) and compared as parsed instants, + not as strings. SessionMeta.modified_at is set by SessionStore.touch(); + touch_seq is the tie-break (see Tie order). Every non-admin caller + read SHALL set SessionMeta.modified_at through SessionStore.touch(). + The caller read surfaces are the READ-SURFACES block below; the + reads that are NOT touches are the ADMIN-READS block below. Writes + (mutate, add, update, import_slice, ingest_*) are touches. Load + (session_load) is a touch with a fresh TTL. Open stamps the first + touch (modified_at = created_at) and takes a touch_seq, so a + never-read session has a defined last touch. + + Tie order. touch_seq is a process-wide monotonic counter held on the + registry entry (SessionEntry) and advanced at every touch and open. + Build option: touchSeqMonotonic=true, touchSeqInSnapshot=false. The + counter is not persisted: a session loaded from a snapshot gets a + fresh touch_seq, because the load is a touch. Order by name then id + is the fallback only if a build cannot hold the counter; this build + can, so the fallback is not used. + + The READ-SURFACES and ADMIN-READS lists cover the MCP tools and the + CLI-only surfaces. READ-SURFACES is MCP read tools, CLI-only reads + (session_resume, tagmap_show, relations_list, query_neighbors, + query_path, query_context, housekeep_stale, housekeep_orphans, + housekeep_dangling, housekeep_recyclable) and the in-process + get_session. Every session-scoped CLI command in cli.py is a read, + an admin read, or a non-read; the sync test fails on any other. + + READ-SURFACES-BEGIN + get_session + pin_map + query_warm + find + query_walk + read_list + export_pin_map + housekeep_stats + session_current + session_resume + tagmap_show + relations_list + query_neighbors + query_path + query_context + housekeep_stale + housekeep_orphans + housekeep_dangling + housekeep_recyclable + READ-SURFACES-END + + ADMIN-READS-BEGIN + serve_status + session_list + admin_usage_report + admin_checkpoint + admin_checkpoint_verify + ADMIN-READS-END A fresh open cannot be its own victim: its session is not in the registry until its slot is reserved under the cap lock, so the pick never sees it. A load of an evicted id is excluded from its own pick diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index 8d2a51b9..cb765cf8 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -2325,11 +2325,21 @@ package MemNetVerification { doc /* MN-REQ-05.5 R1 (proposed, not shipped) — at MEMNET_MAX_SESSIONS on open or load, after purge_expired, evict the live session with the oldest - last touch. Any read or write is a touch; admin and serve_status reads - are not. Runtime checks (xfail until shipped): + last touch, ordered by (modified_at, touch_seq). Any caller read in + READ-SURFACES and any write is a touch; reads in ADMIN-READS are not. + Runtime checks (xfail until shipped): tests/test_session_evict.py::test_evicts_oldest_touched_first, ::test_reads_and_writes_are_touches, - ::test_admin_and_serve_status_reads_are_not_touches. + ::test_admin_and_serve_status_reads_are_not_touches (parametrized over + ADMIN_READS), + ::test_caller_read_is_a_touch_and_moves_lru_pick (parametrized over + READ_SURFACES), + ::test_tie_touch_order_a_then_b_evicts_a, + ::test_tie_touch_order_b_then_a_evicts_b, + ::test_open_assigns_touch_seq, + ::test_victim_order_compares_modified_at_as_instant. + Presence and surface-list sync: the sysml session-evict sync module + in tests/ (not an xfail runtime file). */ attribute verificationId : String = "MN-VER-05-S03"; @@ -2517,7 +2527,8 @@ package MemNetVerification { ::test_no_rid_commit_after_evict_and_reload_succeeds, ::test_rid_held_by_other_llm_refused_reserved, ::test_reopen_restored_true_no_alerts, - ::test_load_is_touch_with_fresh_ttl. + ::test_load_is_touch_with_fresh_ttl, + ::test_touch_seq_not_in_snapshot_fresh_on_load. */ attribute verificationId : String = "MN-VER-05-S09"; diff --git a/tests/test_read_touch_regression.py b/tests/test_read_touch_regression.py new file mode 100644 index 00000000..29788573 --- /dev/null +++ b/tests/test_read_touch_regression.py @@ -0,0 +1,55 @@ +"""MN-REQ-05.5 read-touch regression guard. Not xfail: passes on the shipped engine. + +Every caller read in READ_SURFACES moves modified_at today, except get_session. +The session-scoped CLI path (MCP reads and CLI-only reads) calls _load_session, +which touches. The in-process get_session() only extends the TTL, so it is +marked xfail(strict=True): the mark must come off when the touch rule ships, +and it fails loudly if that happens without the mark being removed. +""" + +from __future__ import annotations + +from datetime import datetime, timedelta + +import pytest + +from memnet.cli import app +from memnet.registry import get_entry +from memnet.session import open_session, set_now_override +from test_session_evict import BASE, READ_SURFACES, caller_read, runner + + +def _instant(text: str) -> datetime: + return datetime.fromisoformat(text.replace("Z", "+00:00")) + + +def _seeded_session(schema_file, workflow_file) -> str: + set_now_override(BASE) + sid = open_session(map_file=str(schema_file), ttl_minutes=600).session_id + r = runner.invoke(app, ["add", "--file", str(workflow_file), "--session", sid]) + assert r.exit_code == 0, "seed write failed" + return sid + + +_PARAMS = [ + pytest.param( + surface, + marks=pytest.mark.xfail( + strict=True, + reason="get_session() only extends the TTL; the touch rule is not shipped", + ), + ) + if surface == "get_session" + else surface + for surface in READ_SURFACES +] + + +@pytest.mark.parametrize("surface", _PARAMS) +def test_cli_path_read_moves_modified_at(memnet_temp, schema_file, workflow_file, surface): + sid = _seeded_session(schema_file, workflow_file) + before = get_entry(sid).meta.modified_at + set_now_override(BASE + timedelta(minutes=3)) + assert caller_read(surface, sid) == 0, f"{surface} read must succeed before its touch" + after = get_entry(sid).meta.modified_at + assert _instant(after) > _instant(before), f"{surface} must set modified_at" diff --git a/tests/test_session_evict.py b/tests/test_session_evict.py index cfb1f222..62cfebe7 100644 --- a/tests/test_session_evict.py +++ b/tests/test_session_evict.py @@ -27,6 +27,7 @@ import memnet.snapshot as snapshot_mod from memnet.acl import acl_to_dict from memnet.admin_usage import build_report # noqa: F401 (admin read surface) +from memnet.checkpoint import checkpoint_dir, run_checkpoint, verify_checkpoint from memnet.cli import app from memnet.config import Caps from memnet.exceptions import MemNetError @@ -36,7 +37,6 @@ from memnet.session import ( SessionStore, get_session, - list_sessions, open_session, reset_registry, set_now_override, @@ -60,6 +60,60 @@ ) +# Surface lists. The MN-REQ-05.5 READ-SURFACES and ADMIN-READS blocks in +# sysml-models/models/requirements.sysml name the same entries; +# tests/test_sysml_session_evict.py asserts the two stay equal. READ_SURFACES +# is the MCP read tools plus the CLI-only reads (CLI_READ_ARGV) plus get_session. +READ_SURFACES = ( + "get_session", + "pin_map", + "query_warm", + "find", + "query_walk", + "read_list", + "export_pin_map", + "housekeep_stats", + "session_current", + "session_resume", + "tagmap_show", + "relations_list", + "query_neighbors", + "query_path", + "query_context", + "housekeep_stale", + "housekeep_orphans", + "housekeep_dangling", + "housekeep_recyclable", +) +ADMIN_READS = ( + "serve_status", + "session_list", + "admin_usage_report", + "admin_checkpoint", + "admin_checkpoint_verify", +) +# Arguments beyond the session for the MCP caller reads that need them. +_READ_ARGS = { + "find": {"limit": 5, "kind": "PLR"}, + "query_walk": {"cue": "PLR01"}, + "read_list": {"tag": "PLR"}, +} +# CLI-only caller reads (no MCP tool). "{sid}" is the session id; each argv +# names ids that workflow.example.txt seeds (PLR01, TEC01, E02). +CLI_READ_ARGV = { + "session_resume": ("session", "resume", "{sid}"), + "tagmap_show": ("tagmap", "show", "--session", "{sid}"), + "relations_list": ("relations", "list", "--session", "{sid}"), + "query_neighbors": ("query", "neighbors", "PLR01", "--session", "{sid}"), + "query_path": ("query", "path", "PLR01", "TEC01", "--session", "{sid}"), + "query_context": ("query", "context", "--session", "{sid}"), + "housekeep_stale": ("housekeep", "stale", "--session", "{sid}"), + "housekeep_orphans": ("housekeep", "orphans", "--session", "{sid}"), + "housekeep_dangling": ("housekeep", "dangling", "--session", "{sid}"), + "housekeep_recyclable": ("housekeep", "recyclable", "--session", "{sid}"), +} + + def _at(minute: float) -> datetime: return BASE + timedelta(minutes=minute) @@ -76,6 +130,18 @@ def evict(memnet_temp, monkeypatch, tmp_path): return snap_dir +@pytest.fixture +def evict_pair(memnet_temp, monkeypatch, tmp_path): + """Cap 2, snapshot dir set, clock frozen at BASE: every touch ties on modified_at.""" + snap_dir = tmp_path / "pair-snaps" + snap_dir.mkdir() + monkeypatch.setenv(ENV_MAX, "2") + monkeypatch.setenv(ENV_DIR, str(snap_dir)) + monkeypatch.delenv(ENV_ALIAS, raising=False) + set_now_override(BASE) + return snap_dir + + def _open(schema, minute: float, ttl: int = 600) -> SessionStore: set_now_override(_at(minute)) return open_session(map_file=str(schema), ttl_minutes=ttl) @@ -114,6 +180,59 @@ def _serve_status_payload() -> dict: return json.loads(asyncio.run(serve_status())) +def _instant(text: str) -> datetime: + return datetime.fromisoformat(text.replace("Z", "+00:00")) + + +def _advanced(before: str | None, after: str | None) -> bool: + if after is None: + return False + return before is None or _instant(after) > _instant(before) + + +def caller_read(surface: str, sid: str) -> int: + """One session-scoped caller read through the surface named in READ_SURFACES. + + Returns the exit code. The text of a failure is not returned: it can name ids. + get_session() raises on failure, so its exit code is 0 or the call raises. + """ + if surface == "get_session": + get_session(sid) + return 0 + if surface in CLI_READ_ARGV: + argv = [a.format(sid=sid) for a in CLI_READ_ARGV[surface]] + return runner.invoke(app, argv).exit_code + from memnet_mcp import server as mcp_server + + call = getattr(mcp_server, surface) + resp = json.loads(asyncio.run(call(session=sid, **_READ_ARGS.get(surface, {})))) + return resp["exit_code"] + + +def _admin_read(surface: str, ckpt_dir) -> None: + """One admin or session-less read through the surface named in ADMIN_READS.""" + if surface == "serve_status": + _serve_status_payload() + elif surface == "session_list": + from memnet_mcp import server as mcp_server + + asyncio.run(mcp_server.session_list()) + elif surface == "admin_usage_report": + build_report(ADMIN_TOKEN) + elif surface == "admin_checkpoint": + run_checkpoint(ADMIN_TOKEN, directory=ckpt_dir) + elif surface == "admin_checkpoint_verify": + run_checkpoint(ADMIN_TOKEN, directory=ckpt_dir) + verify_checkpoint(checkpoint_dir(ckpt_dir), ADMIN_TOKEN) + else: + raise AssertionError(f"no admin call for {surface}") + + +def _open_frozen(schema) -> SessionStore: + """Open at the current (frozen) clock; does not move it.""" + return open_session(map_file=str(schema), ttl_minutes=600) + + # Keys match by word or prefix: a segment starting with one of these names. _CAP_KEY = re.compile(r"(^|_)(cap|limit|max_sessions|sessions_count|evict)") # Raw text matches only these exact tokens, so ordinary words like "capacity" pass. @@ -169,18 +288,82 @@ def test_reads_and_writes_are_touches(evict, schema_file, workflow_file): assert contains(a.session_id) and contains(b.session_id) -def test_admin_and_serve_status_reads_are_not_touches(evict, schema_file, monkeypatch): +@pytest.mark.parametrize("surface", READ_SURFACES) +def test_caller_read_is_a_touch_and_moves_lru_pick(evict, schema_file, workflow_file, surface): + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) # valid ids for the reads; the write is at minute 0 + b = _open(schema_file, 1) + c = _open(schema_file, 2) + before = _last_touch(a.session_id) + set_now_override(_at(3)) + assert caller_read(surface, a.session_id) == 0, f"{surface} read must succeed" + assert _advanced(before, _last_touch(a.session_id)), f"{surface} must set modified_at" + _open(schema_file, 4) + assert not contains(b.session_id), f"after {surface} on a, b must be the victim" + assert contains(a.session_id) and contains(c.session_id) + + +@pytest.mark.parametrize("surface", ADMIN_READS) +def test_admin_and_serve_status_reads_are_not_touches( + evict, schema_file, monkeypatch, tmp_path, surface +): monkeypatch.setenv(ENV_ADMIN, ADMIN_TOKEN) a = _open(schema_file, 0) b = _open(schema_file, 1) c = _open(schema_file, 2) + before = _last_touch(a.session_id) set_now_override(_at(3)) - list_sessions() - build_report(ADMIN_TOKEN) - _serve_status_payload() - d = _open(schema_file, 4) - assert not contains(a.session_id), "admin/serve_status reads must not refresh the touch" - assert contains(b.session_id) and contains(c.session_id) and contains(d.session_id) + _admin_read(surface, tmp_path / "ckpt") + assert _last_touch(a.session_id) == before, f"admin read {surface} must not move modified_at" + _open(schema_file, 4) + assert not contains(a.session_id), f"admin read {surface} must not change the victim pick" + assert contains(b.session_id) and contains(c.session_id) + + +def test_tie_touch_order_a_then_b_evicts_a(evict_pair, schema_file): + # Open order is B then A, so opening order alone would evict B. The final + # touches are A, B, A, B: A's last touch is the earlier one, so A is the victim. + b = _open_frozen(schema_file) + a = _open_frozen(schema_file) + for sid in (a.session_id, b.session_id, a.session_id, b.session_id): + get_session(sid) # frozen clock: every modified_at ties; touch_seq decides + _open_frozen(schema_file) + assert not contains(a.session_id), "the session touched first must be the victim" + assert contains(b.session_id) + + +def test_tie_touch_order_b_then_a_evicts_b(evict_pair, schema_file): + # Open order is A then B, so opening order alone would evict A. The final + # touches are B, A, B, A: B's last touch is the earlier one, so B is the victim. + a = _open_frozen(schema_file) + b = _open_frozen(schema_file) + for sid in (b.session_id, a.session_id, b.session_id, a.session_id): + get_session(sid) # frozen clock: every modified_at ties; touch_seq decides + _open_frozen(schema_file) + assert not contains(b.session_id), "the session touched first must be the victim" + assert contains(a.session_id) + + +def test_open_assigns_touch_seq(evict, schema_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + seq_a = get_entry(a.session_id).touch_seq + seq_b = get_entry(b.session_id).touch_seq + assert isinstance(seq_a, int) and isinstance(seq_b, int), "open must take a touch_seq" + assert seq_b > seq_a, "a later open must take a later touch_seq" + + +def test_victim_order_compares_modified_at_as_instant(evict_pair, schema_file): + # Whole-second stamp "...00Z" and fractional stamp "...00.500000Z": as strings + # the fractional one sorts first ('.' < 'Z'), but as instants it is 0.5 s later. + set_now_override(BASE) + whole = open_session(map_file=str(schema_file), ttl_minutes=600) + set_now_override(BASE + timedelta(milliseconds=500)) + fractional = open_session(map_file=str(schema_file), ttl_minutes=600) + set_now_override(_at(1)) + open_session(map_file=str(schema_file), ttl_minutes=600) # cap 2: one victim + assert not contains(whole.session_id), "the oldest instant must be the victim" + assert contains(fractional.session_id) # --- S04: save first, atomic write, victim lock, crash safety --------------- @@ -787,3 +970,21 @@ def test_load_is_touch_with_fresh_ttl(evict, schema_file): loaded = load_snapshot(snap) expires = datetime.fromisoformat(loaded.meta.expires_at.replace("Z", "+00:00")) assert expires == _at(30 + 60), "a load starts a fresh TTL from load time" + + +def test_touch_seq_not_in_snapshot_fresh_on_load(evict, schema_file, workflow_file): + # touchSeqInSnapshot=false: the counter is not persisted; a load is a touch. + a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) + victim = a.session_id + b = _open(schema_file, 1) + c = _open(schema_file, 2) + _open(schema_file, 4) # evicts a + snap = _snapshot_of(evict, victim) + assert "touch_seq" not in snap.read_text(encoding="utf-8"), "snapshot must not carry touch_seq" + set_now_override(_at(5)) + loaded = load_snapshot(snap) + assert loaded.store.get("PLR01") is not None, "round trip must keep the rows" + seq_loaded = get_entry(loaded.session_id).touch_seq + others = [get_entry(s.session_id).touch_seq for s in (b, c)] + assert seq_loaded > max(others), "a loaded session must get a fresh touch_seq above all others" diff --git a/tests/test_sysml_session_evict.py b/tests/test_sysml_session_evict.py index 28a160fe..e3cb51aa 100644 --- a/tests/test_sysml_session_evict.py +++ b/tests/test_sysml_session_evict.py @@ -1,14 +1,17 @@ """MN-REQ-05.5 model presence: the SysML cites runtime tests (proposed, not shipped). Runtime behaviour lives in tests/test_session_evict.py. This file only checks -that the model points at those tests, that every cited test exists, and that -the runtime module stays xfail until the engine ships. It makes no claim that a -flag is true. +that the model points at those tests, that every cited test exists, that the +runtime module stays xfail until the engine ships, and that the READ-SURFACES +and ADMIN-READS blocks match the runtime surface lists and cover every +registered MCP tool and every session-scoped CLI command in cli.py. It makes +no claim that a flag is true. """ from __future__ import annotations import ast +import asyncio import re from pathlib import Path @@ -20,10 +23,61 @@ VERIFY = MODELS / "verify.sysml" BEHAVIOUR = MODELS / "behaviour.sysml" RUNTIME = ROOT / "tests" / "test_session_evict.py" +CLI = ROOT / "parts" / "common" / "memnet" / "memnet" / "cli.py" VER_IDS = [f"MN-VER-05-S0{n}" for n in range(3, 10)] SATISFY_LINE = ( r"^\s*satisfy\s+MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru\s*;" ) +# Registered MCP tools that are not caller reads: writes, lifecycle, lease verbs. +# Every other registered tool must be a READ-SURFACES or ADMIN-READS entry, so a +# new tool fails test_every_caller_mcp_read_tool_is_listed until it is classified. +MCP_NON_READ_TOOLS = frozenset( + { + "add", + "extend", + "import_slice", + "ingest_codebase", + "ingest_pcba", + "ingest_skills", + "ingest_sysml", + "mutate", + "release", + "reserve", + "session_acl_bind", + "session_acl_enable", + "session_acl_grant", + "session_close", + "session_load", + "session_open", + "session_save", + "snap_model", + "update", + } +) +# CLI function name -> surface name, where the CLI function is named differently +# from its MCP tool or classification entry. Other session-scoped commands match by name. +CLI_SURFACE_ALIAS = { + "add_cmd": "add", + "delete_cmd": "delete", + "export_pin_map_cmd": "export_pin_map", + "extend_cmd": "extend", + "import_slice_cmd": "import_slice", + "ingest_codebase_cmd": "ingest_codebase", + "ingest_pcba_cmd": "ingest_pcba", + "ingest_skills_cmd": "ingest_skills", + "ingest_sysml_cmd": "ingest_sysml", + "mutate_cmd": "mutate", + "prune_stale_cmd": "prune_stale", + "query_find": "find", + "query_pin_map": "pin_map", + "release_cmd": "release", + "reserve_cmd": "reserve", + "update_cmd": "update", +} +# Session-scoped CLI writes and prunes with no MCP tool of the same name. +CLI_ONLY_NON_READ = frozenset( + {"delete", "prune_dangling", "prune_orphans", "prune_recyclable", "prune_stale"} +) def _read(path: Path) -> str: @@ -171,6 +225,100 @@ def test_readme_points_at_runtime_file(): assert "tests/test_session_evict.py" in _read(README) +def _block_names(text: str, name: str) -> list[str]: + """Surface names between ``-BEGIN`` and ``-END``, one per line.""" + begin, end = f"{name}-BEGIN", f"{name}-END" + assert text.count(begin) == 1, f"{begin} must appear exactly once in requirements.sysml" + assert text.count(end) == 1, f"{end} must appear exactly once in requirements.sysml" + body = text.split(begin, 1)[1].split(end, 1)[0] + return [line.strip() for line in body.splitlines() if line.strip()] + + +def _module_tuple(name: str) -> tuple[str, ...]: + """A string-tuple module constant of the runtime test file, read without importing it.""" + for node in ast.parse(_read(RUNTIME)).body: + if isinstance(node, ast.Assign) and any( + isinstance(t, ast.Name) and t.id == name for t in node.targets + ): + return tuple(ast.literal_eval(node.value)) + raise AssertionError(f"{name} must be a module constant in tests/test_session_evict.py") + + +def test_surface_blocks_match_runtime_constants(): + text = _read(REQ) + for block, const in (("READ-SURFACES", "READ_SURFACES"), ("ADMIN-READS", "ADMIN_READS")): + names = _block_names(text, block) + assert len(names) == len(set(names)), f"{block} must not repeat a surface" + assert set(names) == set(_module_tuple(const)), f"{block} must equal {const}" + + +def test_every_caller_mcp_read_tool_is_listed(): + from memnet.cli import admin_app + from memnet_mcp.server import mcp + + registered = {t.name for t in asyncio.run(mcp.list_tools())} + reads = set(_module_tuple("READ_SURFACES")) + admin = set(_module_tuple("ADMIN_READS")) + cli_only = set(_module_tuple("CLI_READ_ARGV")) + assert MCP_NON_READ_TOOLS <= registered, "MCP_NON_READ_TOOLS names an unregistered tool" + assert not (reads & MCP_NON_READ_TOOLS), "a READ_SURFACES entry must not be a non-read tool" + assert not (admin & MCP_NON_READ_TOOLS), "an ADMIN_READS entry must not be a non-read tool" + unlisted = registered - MCP_NON_READ_TOOLS - reads - admin + assert not unlisted, f"classify these MCP tools as read or non-read: {sorted(unlisted)}" + # get_session is the in-process read; CLI_READ_ARGV names the CLI-only reads; + # every other READ entry is an MCP tool. + mcp_reads = reads - {"get_session"} - cli_only + assert mcp_reads <= registered, "a READ_SURFACES MCP name is not registered" + # Admin entries that are not MCP tools must be real `memnet admin` commands. + admin_cmds = {"admin_" + c.name.replace("-", "_") for c in admin_app.registered_commands} + assert (admin - registered) <= admin_cmds, "ADMIN_READS names an admin command that is absent" + + +def _cli_session_commands() -> dict[str, str]: + """CLI function name -> surface name, for every session-scoped command in cli.py. + + cli.py registers commands with typer (``@.command(...)``), not argparse. + A command is session-scoped when one of its parameters names a session. + """ + found: dict[str, str] = {} + for node in ast.parse(_read(CLI)).body: + if not isinstance(node, ast.FunctionDef): + continue + is_command = any( + isinstance(d, ast.Call) + and isinstance(d.func, ast.Attribute) + and d.func.attr == "command" + for d in node.decorator_list + ) + params = [a.arg for a in node.args.args] + if is_command and any("session" in p for p in params): + found[node.name] = CLI_SURFACE_ALIAS.get(node.name, node.name) + return found + + +def test_every_cli_session_command_is_classified(): + from memnet_mcp.server import mcp + + registered = {t.name for t in asyncio.run(mcp.list_tools())} + reads = set(_module_tuple("READ_SURFACES")) + admin = set(_module_tuple("ADMIN_READS")) + cli_only = set(_module_tuple("CLI_READ_ARGV")) + commands = _cli_session_commands() + assert commands, "no session-scoped CLI command found in cli.py; the parser has moved" + classified = reads | admin | MCP_NON_READ_TOOLS | CLI_ONLY_NON_READ + unclassified = sorted(f for f, surface in commands.items() if surface not in classified) + assert not unclassified, ( + f"classify these session-scoped CLI commands as read, admin or non-read: {unclassified}" + ) + # Every CLI-only read must be a real session-scoped command, and every read + # that is not an MCP tool must be a CLI-only read with its argv. + surfaces = set(commands.values()) + assert cli_only <= surfaces, "CLI_READ_ARGV names a command absent from cli.py" + assert (reads - {"get_session"} - registered) == cli_only, ( + "a READ_SURFACES entry that is not an MCP tool must be in CLI_READ_ARGV" + ) + + def test_no_lease_carried_wording_anywhere_in_models(): everything = "\n".join(_read(p) for p in MODELS.glob("*.sysml")) + _read(README) assert "evictKeepsAclLease" not in everything From e61e5db293afa3d4d5470d5c2b65aacf5935ccad Mon Sep 17 00:00:00 2001 From: chouswei <104312007+chouswei@users.noreply.github.com> Date: Tue, 20 Oct 2026 23:01:33 +0800 Subject: [PATCH 7/7] model: MN-REQ-05.5 maintenance saves not touches, open first touch, ship-sync strict xfails, surface split, classifier, helper constants --- sysml-models/models/deploy.sysml | 5 +- sysml-models/models/requirements.sysml | 46 +++-- sysml-models/models/verify.sysml | 11 +- tests/evict_surfaces.py | 112 +++++++++++ tests/test_read_touch_regression.py | 37 ++-- tests/test_session_evict.py | 122 ++++++------ tests/test_sysml_session_evict.py | 250 ++++++++++++++++--------- 7 files changed, 403 insertions(+), 180 deletions(-) create mode 100644 tests/evict_surfaces.py diff --git a/sysml-models/models/deploy.sysml b/sysml-models/models/deploy.sysml index 31e28628..b19af22b 100644 --- a/sysml-models/models/deploy.sysml +++ b/sysml-models/models/deploy.sysml @@ -169,7 +169,10 @@ package MemNet { attribute evictCapFullWithDirEvicts : Boolean = true; // test_cap_full_with_snapshot_dir_evicts_oldest attribute evictPicksOldestTouch : Boolean = true; // test_evicts_oldest_touched_first attribute evictTouchOnReadOrWrite : Boolean = true; // test_reads_and_writes_are_touches - attribute evictAdminReadsNotTouch : Boolean = true; // test_admin_and_serve_status_reads_are_not_touches + attribute evictNonTouchReadsNotTouch : Boolean = true; // test_non_touch_reads_do_not_touch + attribute evictMaintenanceSavesNotTouch : Boolean = true; // test_maintenance_save_is_not_a_touch + attribute evictNeverReadOpenIsVictim : Boolean = true; // test_never_read_earliest_open_is_victim + attribute evictOpenIsFirstTouch : Boolean = true; // tests/test_read_touch_regression.py::test_open_stamps_first_touch // Tie order (MN-REQ-05.5): pick is (modified_at, touch_seq). touch_seq is a // process-wide monotonic counter on SessionEntry, not persisted in snapshots // (a load is a fresh touch). Name-then-id fallback is unused: the counter is held. diff --git a/sysml-models/models/requirements.sysml b/sysml-models/models/requirements.sysml index ae2c4cb6..aaa42227 100644 --- a/sysml-models/models/requirements.sysml +++ b/sysml-models/models/requirements.sysml @@ -777,8 +777,9 @@ package MemNetRequirements { in-process get_session() only extends the TTL and does NOT touch: a read through get_session() alone leaves modified_at unchanged today. That is the gap the touch rule below closes. session_list, - serve_status and the admin commands do not touch. session_save - writes a file and does not touch; it is not a read surface. + serve_status and the admin commands do not touch. The saves + session_save, expire-save, admin checkpoint and evict-save do not + touch either (MAINTENANCE-SAVES below); a save is not a read surface. Cap. At session open or load, after purge_expired, when the count reaches MEMNET_MAX_SESSIONS (default 1024) the engine SHALL pick at @@ -793,11 +794,14 @@ package MemNetRequirements { touch_seq is the tie-break (see Tie order). Every non-admin caller read SHALL set SessionMeta.modified_at through SessionStore.touch(). The caller read surfaces are the READ-SURFACES block below; the - reads that are NOT touches are the ADMIN-READS block below. Writes - (mutate, add, update, import_slice, ingest_*) are touches. Load - (session_load) is a touch with a fresh TTL. Open stamps the first - touch (modified_at = created_at) and takes a touch_seq, so a - never-read session has a defined last touch. + reads that are NOT touches are the NON-TOUCH-READS block below. + Writes (mutate, add, update, import_slice, ingest_*) are touches. + Load (session_load) is a touch with a fresh TTL. Saves SHALL NOT + touch: session_save, expire-save, admin checkpoint and evict-save + (the MAINTENANCE-SAVES block below) SHALL leave modified_at and + touch_seq unchanged. Open stamps the first touch (modified_at = + created_at) and takes a touch_seq, so a never-read session has a + defined last touch. Tie order. touch_seq is a process-wide monotonic counter held on the registry entry (SessionEntry) and advanced at every touch and open. @@ -807,13 +811,15 @@ package MemNetRequirements { is the fallback only if a build cannot hold the counter; this build can, so the fallback is not used. - The READ-SURFACES and ADMIN-READS lists cover the MCP tools and the - CLI-only surfaces. READ-SURFACES is MCP read tools, CLI-only reads + The READ-SURFACES, NON-TOUCH-READS and MAINTENANCE-SAVES lists cover + the MCP tools and the CLI-only surfaces. READ-SURFACES is MCP read + tools, CLI-only reads (session_resume, tagmap_show, relations_list, query_neighbors, query_path, query_context, housekeep_stale, housekeep_orphans, housekeep_dangling, housekeep_recyclable) and the in-process get_session. Every session-scoped CLI command in cli.py is a read, - an admin read, or a non-read; the sync test fails on any other. + a non-touch read, a maintenance save, or a non-read; the sync test fails + on any other. READ-SURFACES-BEGIN get_session @@ -837,13 +843,19 @@ package MemNetRequirements { housekeep_recyclable READ-SURFACES-END - ADMIN-READS-BEGIN + NON-TOUCH-READS-BEGIN serve_status session_list admin_usage_report - admin_checkpoint admin_checkpoint_verify - ADMIN-READS-END + NON-TOUCH-READS-END + + MAINTENANCE-SAVES-BEGIN + session_save + expire_save + admin_checkpoint + evict_save + MAINTENANCE-SAVES-END A fresh open cannot be its own victim: its session is not in the registry until its slot is reserved under the cap lock, so the pick never sees it. A load of an evicted id is excluded from its own pick @@ -923,7 +935,7 @@ package MemNetRequirements { caller-visible signal and is not hidden. Settled (not open): a lease does not survive eviction; a load is a - touch with a fresh TTL; admin and serve_status reads are not + touch with a fresh TTL; non-touch reads and saves are not touches; no default snapshot dir (no dir means the cap refuses; MEMNET_EXPIRE_SNAPSHOT_DIR is reused, with MEMNET_SNAPSHOT_DIR as an alias that must agree); one cap lock for count, pick and slot @@ -933,7 +945,9 @@ package MemNetRequirements { Ship (one commit, PR-facing). The commit that ships the engine SHALL in one change: (1) flip the module pytestmark in - tests/test_session_evict.py to strict=True or drop the xfail; (2) set + tests/test_session_evict.py to strict=True or drop the xfail, and drop + the get_session and test_open_stamps_first_touch xfail marks in + tests/test_read_touch_regression.py; (2) set deploy CapsPolicy evictShipped=true and commitRefusesLostLease=true; (3) add the deploy satisfy link MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru; @@ -941,7 +955,7 @@ package MemNetRequirements { MN-VER-05-S03..S09 and caps.commitRefusesLostLease == true in MN-VER-05-S09. tests/test_sysml_session_evict.py::test_ship_flags_flip_together enforces (1) to (4): it fails unless evictShipped, commitRefusesLostLease, - the satisfy link and the xfail mark all agree, and every guard matches. + the satisfy link and the xfail marks all agree, and every guard matches. LATER (not dropped, not modelled): a "touched within the last N minutes" exemption. Do not add it until a measured run shows diff --git a/sysml-models/models/verify.sysml b/sysml-models/models/verify.sysml index cb765cf8..3829cb84 100644 --- a/sysml-models/models/verify.sysml +++ b/sysml-models/models/verify.sysml @@ -2326,18 +2326,23 @@ package MemNetVerification { MN-REQ-05.5 R1 (proposed, not shipped) — at MEMNET_MAX_SESSIONS on open or load, after purge_expired, evict the live session with the oldest last touch, ordered by (modified_at, touch_seq). Any caller read in - READ-SURFACES and any write is a touch; reads in ADMIN-READS are not. + READ-SURFACES and any write is a touch; reads in NON-TOUCH-READS and + saves in MAINTENANCE-SAVES are not. Open is the first touch. Runtime checks (xfail until shipped): tests/test_session_evict.py::test_evicts_oldest_touched_first, ::test_reads_and_writes_are_touches, - ::test_admin_and_serve_status_reads_are_not_touches (parametrized over - ADMIN_READS), + ::test_non_touch_reads_do_not_touch (parametrized over NON_TOUCH_READS), + ::test_maintenance_save_is_not_a_touch (parametrized over the saves + reachable from tests), + ::test_never_read_earliest_open_is_victim, ::test_caller_read_is_a_touch_and_moves_lru_pick (parametrized over READ_SURFACES), ::test_tie_touch_order_a_then_b_evicts_a, ::test_tie_touch_order_b_then_a_evicts_b, ::test_open_assigns_touch_seq, ::test_victim_order_compares_modified_at_as_instant. + Open as first touch (read-touch regression, strict xfail until shipped): + tests/test_read_touch_regression.py::test_open_stamps_first_touch. Presence and surface-list sync: the sysml session-evict sync module in tests/ (not an xfail runtime file). */ diff --git a/tests/evict_surfaces.py b/tests/evict_surfaces.py new file mode 100644 index 00000000..5a010f52 --- /dev/null +++ b/tests/evict_surfaces.py @@ -0,0 +1,112 @@ +"""MN-REQ-05.5 surface lists, shared by the runtime and sysml sync tests. + +A helper, not a test module: pytest does not collect it. The READ-SURFACES, +NON-TOUCH-READS and MAINTENANCE-SAVES blocks in sysml-models/models/requirements.sysml +name the same entries; tests/test_sysml_session_evict.py asserts they stay equal. +""" + +# Caller reads: each one SHALL set modified_at through SessionStore.touch(). +# READ_SURFACES is the MCP read tools plus the CLI-only reads (CLI_READ_ARGV) +# plus the in-process get_session. +READ_SURFACES = ( + "get_session", + "pin_map", + "query_warm", + "find", + "query_walk", + "read_list", + "export_pin_map", + "housekeep_stats", + "session_current", + "session_resume", + "tagmap_show", + "relations_list", + "query_neighbors", + "query_path", + "query_context", + "housekeep_stale", + "housekeep_orphans", + "housekeep_dangling", + "housekeep_recyclable", +) +# Reads that SHALL NOT touch: status, listing, usage and checkpoint verification. +NON_TOUCH_READS = ( + "serve_status", + "session_list", + "admin_usage_report", + "admin_checkpoint_verify", +) +# Saves that SHALL NOT touch: they write a file, they are not reads. +# evict_save is the eviction's own save, so it has no surface of its own yet. +MAINTENANCE_SAVES = ( + "session_save", + "expire_save", + "admin_checkpoint", + "evict_save", +) +# Maintenance saves with no MCP tool or admin command of their own; the engine runs them. +ENGINE_SAVES = frozenset({"expire_save", "evict_save"}) +# CLI-only caller reads (no MCP tool). "{sid}" is the session id; each argv +# names ids that workflow.example.txt seeds (PLR01, TEC01, E02). +CLI_READ_ARGV = { + "session_resume": ("session", "resume", "{sid}"), + "tagmap_show": ("tagmap", "show", "--session", "{sid}"), + "relations_list": ("relations", "list", "--session", "{sid}"), + "query_neighbors": ("query", "neighbors", "PLR01", "--session", "{sid}"), + "query_path": ("query", "path", "PLR01", "TEC01", "--session", "{sid}"), + "query_context": ("query", "context", "--session", "{sid}"), + "housekeep_stale": ("housekeep", "stale", "--session", "{sid}"), + "housekeep_orphans": ("housekeep", "orphans", "--session", "{sid}"), + "housekeep_dangling": ("housekeep", "dangling", "--session", "{sid}"), + "housekeep_recyclable": ("housekeep", "recyclable", "--session", "{sid}"), +} +# Registered MCP tools that are not caller reads: writes, lifecycle, lease verbs. +# Every other registered tool must be a READ-SURFACES or NON-TOUCH-READS entry, so a +# new tool fails test_every_caller_mcp_read_tool_is_listed until it is classified. +MCP_NON_READ_TOOLS = frozenset( + { + "add", + "extend", + "import_slice", + "ingest_codebase", + "ingest_pcba", + "ingest_skills", + "ingest_sysml", + "mutate", + "release", + "reserve", + "session_acl_bind", + "session_acl_enable", + "session_acl_grant", + "session_close", + "session_load", + "session_open", + "session_save", + "snap_model", + "update", + } +) +# CLI function name -> surface name, where the CLI function is named differently +# from its MCP tool or classification entry. Other session-scoped commands match by name. +CLI_SURFACE_ALIAS = { + "add_cmd": "add", + "delete_cmd": "delete", + "export_pin_map_cmd": "export_pin_map", + "extend_cmd": "extend", + "import_slice_cmd": "import_slice", + "ingest_codebase_cmd": "ingest_codebase", + "ingest_pcba_cmd": "ingest_pcba", + "ingest_skills_cmd": "ingest_skills", + "ingest_sysml_cmd": "ingest_sysml", + "mutate_cmd": "mutate", + "prune_stale_cmd": "prune_stale", + "query_find": "find", + "query_pin_map": "pin_map", + "release_cmd": "release", + "reserve_cmd": "reserve", + "update_cmd": "update", +} +# Session-scoped CLI writes and prunes with no MCP tool of the same name. +CLI_ONLY_NON_READ = frozenset( + {"delete", "prune_dangling", "prune_orphans", "prune_recyclable", "prune_stale"} +) diff --git a/tests/test_read_touch_regression.py b/tests/test_read_touch_regression.py index 29788573..cc4e941c 100644 --- a/tests/test_read_touch_regression.py +++ b/tests/test_read_touch_regression.py @@ -5,6 +5,10 @@ which touches. The in-process get_session() only extends the TTL, so it is marked xfail(strict=True): the mark must come off when the touch rule ships, and it fails loudly if that happens without the mark being removed. + +test_open_stamps_first_touch is the open side of the same rule: open is the +first touch, so modified_at = created_at right after open. It is strict xfail +until the engine stamps it. """ from __future__ import annotations @@ -13,10 +17,11 @@ import pytest +from evict_surfaces import READ_SURFACES from memnet.cli import app from memnet.registry import get_entry from memnet.session import open_session, set_now_override -from test_session_evict import BASE, READ_SURFACES, caller_read, runner +from test_session_evict import BASE, caller_read, runner def _instant(text: str) -> datetime: @@ -31,21 +36,20 @@ def _seeded_session(schema_file, workflow_file) -> str: return sid -_PARAMS = [ - pytest.param( - surface, - marks=pytest.mark.xfail( - strict=True, - reason="get_session() only extends the TTL; the touch rule is not shipped", - ), - ) +_GET_SESSION_XFAIL = pytest.mark.xfail( + strict=True, + reason="get_session() only extends the TTL; the touch rule is not shipped", +) +# Module-level so the sync test can read the get_session mark from the parameter set. +SURFACE_PARAMS = [ + pytest.param(surface, marks=_GET_SESSION_XFAIL) if surface == "get_session" - else surface + else pytest.param(surface) for surface in READ_SURFACES ] -@pytest.mark.parametrize("surface", _PARAMS) +@pytest.mark.parametrize("surface", SURFACE_PARAMS) def test_cli_path_read_moves_modified_at(memnet_temp, schema_file, workflow_file, surface): sid = _seeded_session(schema_file, workflow_file) before = get_entry(sid).meta.modified_at @@ -53,3 +57,14 @@ def test_cli_path_read_moves_modified_at(memnet_temp, schema_file, workflow_file assert caller_read(surface, sid) == 0, f"{surface} read must succeed before its touch" after = get_entry(sid).meta.modified_at assert _instant(after) > _instant(before), f"{surface} must set modified_at" + + +@pytest.mark.xfail( + strict=True, + reason="open does not stamp modified_at yet; open is the first touch once the rule ships", +) +def test_open_stamps_first_touch(memnet_temp, schema_file): + set_now_override(BASE) + sid = open_session(map_file=str(schema_file), ttl_minutes=600).session_id + meta = get_entry(sid).meta + assert meta.modified_at == meta.created_at, "open is the first touch: modified_at = created_at" diff --git a/tests/test_session_evict.py b/tests/test_session_evict.py index 62cfebe7..42851d2a 100644 --- a/tests/test_session_evict.py +++ b/tests/test_session_evict.py @@ -25,6 +25,7 @@ import memnet.registry as registry_mod import memnet.session as session_mod import memnet.snapshot as snapshot_mod +from evict_surfaces import CLI_READ_ARGV, NON_TOUCH_READS, READ_SURFACES from memnet.acl import acl_to_dict from memnet.admin_usage import build_report # noqa: F401 (admin read surface) from memnet.checkpoint import checkpoint_dir, run_checkpoint, verify_checkpoint @@ -40,6 +41,7 @@ open_session, reset_registry, set_now_override, + snapshot_expired_session, ) from memnet.snapshot import load_snapshot @@ -60,58 +62,15 @@ ) -# Surface lists. The MN-REQ-05.5 READ-SURFACES and ADMIN-READS blocks in -# sysml-models/models/requirements.sysml name the same entries; -# tests/test_sysml_session_evict.py asserts the two stay equal. READ_SURFACES -# is the MCP read tools plus the CLI-only reads (CLI_READ_ARGV) plus get_session. -READ_SURFACES = ( - "get_session", - "pin_map", - "query_warm", - "find", - "query_walk", - "read_list", - "export_pin_map", - "housekeep_stats", - "session_current", - "session_resume", - "tagmap_show", - "relations_list", - "query_neighbors", - "query_path", - "query_context", - "housekeep_stale", - "housekeep_orphans", - "housekeep_dangling", - "housekeep_recyclable", -) -ADMIN_READS = ( - "serve_status", - "session_list", - "admin_usage_report", - "admin_checkpoint", - "admin_checkpoint_verify", -) # Arguments beyond the session for the MCP caller reads that need them. _READ_ARGS = { "find": {"limit": 5, "kind": "PLR"}, "query_walk": {"cue": "PLR01"}, "read_list": {"tag": "PLR"}, } -# CLI-only caller reads (no MCP tool). "{sid}" is the session id; each argv -# names ids that workflow.example.txt seeds (PLR01, TEC01, E02). -CLI_READ_ARGV = { - "session_resume": ("session", "resume", "{sid}"), - "tagmap_show": ("tagmap", "show", "--session", "{sid}"), - "relations_list": ("relations", "list", "--session", "{sid}"), - "query_neighbors": ("query", "neighbors", "PLR01", "--session", "{sid}"), - "query_path": ("query", "path", "PLR01", "TEC01", "--session", "{sid}"), - "query_context": ("query", "context", "--session", "{sid}"), - "housekeep_stale": ("housekeep", "stale", "--session", "{sid}"), - "housekeep_orphans": ("housekeep", "orphans", "--session", "{sid}"), - "housekeep_dangling": ("housekeep", "dangling", "--session", "{sid}"), - "housekeep_recyclable": ("housekeep", "recyclable", "--session", "{sid}"), -} +# Saves that SHALL NOT touch, reachable from tests. evict_save runs inside the +# eviction itself, so it is covered once the engine ships (see MAINTENANCE-SAVES). +MAINTENANCE_SAVES_REACHABLE = ("session_save", "expire_save", "admin_checkpoint") def _at(minute: float) -> datetime: @@ -209,8 +168,8 @@ def caller_read(surface: str, sid: str) -> int: return resp["exit_code"] -def _admin_read(surface: str, ckpt_dir) -> None: - """One admin or session-less read through the surface named in ADMIN_READS.""" +def _non_touch_read(surface: str, ckpt_dir) -> None: + """One non-touch read through the surface named in NON_TOUCH_READS.""" if surface == "serve_status": _serve_status_payload() elif surface == "session_list": @@ -219,13 +178,24 @@ def _admin_read(surface: str, ckpt_dir) -> None: asyncio.run(mcp_server.session_list()) elif surface == "admin_usage_report": build_report(ADMIN_TOKEN) - elif surface == "admin_checkpoint": - run_checkpoint(ADMIN_TOKEN, directory=ckpt_dir) elif surface == "admin_checkpoint_verify": - run_checkpoint(ADMIN_TOKEN, directory=ckpt_dir) verify_checkpoint(checkpoint_dir(ckpt_dir), ADMIN_TOKEN) else: - raise AssertionError(f"no admin call for {surface}") + raise AssertionError(f"no non-touch read for {surface}") + + +def _maintenance_save(surface: str, sid: str, tmp_path) -> None: + """One save through the surface named in MAINTENANCE_SAVES_REACHABLE.""" + if surface == "session_save": + snap = str(tmp_path / "s.snap") + r = runner.invoke(app, ["session", "save", "--file", snap, "--session", sid]) + assert r.exit_code == 0, "session save failed" + elif surface == "expire_save": + assert snapshot_expired_session(sid) is not None, "expire save failed" + elif surface == "admin_checkpoint": + run_checkpoint(ADMIN_TOKEN, directory=tmp_path / "ckpt") + else: + raise AssertionError(f"no maintenance save for {surface}") def _open_frozen(schema) -> SessionStore: @@ -303,20 +273,53 @@ def test_caller_read_is_a_touch_and_moves_lru_pick(evict, schema_file, workflow_ assert contains(a.session_id) and contains(c.session_id) -@pytest.mark.parametrize("surface", ADMIN_READS) -def test_admin_and_serve_status_reads_are_not_touches( - evict, schema_file, monkeypatch, tmp_path, surface +@pytest.mark.parametrize("surface", NON_TOUCH_READS) +def test_non_touch_reads_do_not_touch(evict, schema_file, monkeypatch, tmp_path, surface): + monkeypatch.setenv(ENV_ADMIN, ADMIN_TOKEN) + ckpt = tmp_path / "ckpt" + a = _open(schema_file, 0) + b = _open(schema_file, 1) + c = _open(schema_file, 2) + if surface == "admin_checkpoint_verify": + # A checkpoint to verify, taken before the measured window. + run_checkpoint(ADMIN_TOKEN, directory=ckpt) + before = _last_touch(a.session_id) + set_now_override(_at(3)) + _non_touch_read(surface, ckpt) + assert _last_touch(a.session_id) == before, f"{surface} must not move modified_at" + _open(schema_file, 4) + assert not contains(a.session_id), f"{surface} must not change the victim pick" + assert contains(b.session_id) and contains(c.session_id) + + +@pytest.mark.parametrize("surface", MAINTENANCE_SAVES_REACHABLE) +def test_maintenance_save_is_not_a_touch( + evict, schema_file, workflow_file, monkeypatch, tmp_path, surface ): monkeypatch.setenv(ENV_ADMIN, ADMIN_TOKEN) + if surface == "expire_save": + monkeypatch.setenv("MEMNET_SAVE_ON_EXPIRE", "1") a = _open(schema_file, 0) + _seed(a.session_id, workflow_file) # a's last touch is the write at minute 0 b = _open(schema_file, 1) c = _open(schema_file, 2) before = _last_touch(a.session_id) + before_seq = get_entry(a.session_id).touch_seq set_now_override(_at(3)) - _admin_read(surface, tmp_path / "ckpt") - assert _last_touch(a.session_id) == before, f"admin read {surface} must not move modified_at" + _maintenance_save(surface, a.session_id, tmp_path) + assert _last_touch(a.session_id) == before, f"{surface} must not move modified_at" + assert get_entry(a.session_id).touch_seq == before_seq, f"{surface} must not take a touch_seq" _open(schema_file, 4) - assert not contains(a.session_id), f"admin read {surface} must not change the victim pick" + assert not contains(a.session_id), f"after {surface}, a must still be the victim" + assert contains(b.session_id) and contains(c.session_id) + + +def test_never_read_earliest_open_is_victim(evict, schema_file): + a = _open(schema_file, 0) + b = _open(schema_file, 1) + c = _open(schema_file, 2) + _open(schema_file, 4) # nothing was read: the earliest open is the oldest touch + assert not contains(a.session_id), "a never-read session opened earliest must be the victim" assert contains(b.session_id) and contains(c.session_id) @@ -360,6 +363,9 @@ def test_victim_order_compares_modified_at_as_instant(evict_pair, schema_file): whole = open_session(map_file=str(schema_file), ttl_minutes=600) set_now_override(BASE + timedelta(milliseconds=500)) fractional = open_session(map_file=str(schema_file), ttl_minutes=600) + assert re.search(r"\.5\d*Z$", _last_touch(fractional.session_id)), ( + "the stored modified_at must keep its fraction, or the ordering test proves nothing" + ) set_now_override(_at(1)) open_session(map_file=str(schema_file), ttl_minutes=600) # cap 2: one victim assert not contains(whole.session_id), "the oldest instant must be the victim" diff --git a/tests/test_sysml_session_evict.py b/tests/test_sysml_session_evict.py index e3cb51aa..2b4cfe2a 100644 --- a/tests/test_sysml_session_evict.py +++ b/tests/test_sysml_session_evict.py @@ -2,10 +2,10 @@ Runtime behaviour lives in tests/test_session_evict.py. This file only checks that the model points at those tests, that every cited test exists, that the -runtime module stays xfail until the engine ships, and that the READ-SURFACES -and ADMIN-READS blocks match the runtime surface lists and cover every -registered MCP tool and every session-scoped CLI command in cli.py. It makes -no claim that a flag is true. +runtime module stays xfail until the engine ships, and that the READ-SURFACES, +NON-TOUCH-READS and MAINTENANCE-SAVES blocks match the shared surface lists in +tests/evict_surfaces.py and cover every registered MCP tool and every +session-scoped CLI command in cli.py. It makes no claim that a flag is true. """ from __future__ import annotations @@ -15,6 +15,19 @@ import re from pathlib import Path +import test_read_touch_regression as read_touch +from evict_surfaces import ( + CLI_ONLY_NON_READ, + CLI_READ_ARGV, + CLI_SURFACE_ALIAS, + ENGINE_SAVES, + MAINTENANCE_SAVES, + MCP_NON_READ_TOOLS, + NON_TOUCH_READS, + READ_SURFACES, +) +from test_read_touch_regression import SURFACE_PARAMS + ROOT = Path(__file__).resolve().parents[1] MODELS = ROOT / "sysml-models" / "models" README = ROOT / "sysml-models" / "README.md" @@ -23,61 +36,17 @@ VERIFY = MODELS / "verify.sysml" BEHAVIOUR = MODELS / "behaviour.sysml" RUNTIME = ROOT / "tests" / "test_session_evict.py" +READ_TOUCH = ROOT / "tests" / "test_read_touch_regression.py" +# Runtime files a verify doc may cite a test from; the path itself is not a test name. +RUNTIME_FILES = ("tests/test_session_evict.py", "tests/test_read_touch_regression.py") CLI = ROOT / "parts" / "common" / "memnet" / "memnet" / "cli.py" VER_IDS = [f"MN-VER-05-S0{n}" for n in range(3, 10)] SATISFY_LINE = ( r"^\s*satisfy\s+MN_REQ_00_MissionBridge::MN_REQ_05_HardCaps::MN_REQ_05_5_SessionCapEvictLru\s*;" ) -# Registered MCP tools that are not caller reads: writes, lifecycle, lease verbs. -# Every other registered tool must be a READ-SURFACES or ADMIN-READS entry, so a -# new tool fails test_every_caller_mcp_read_tool_is_listed until it is classified. -MCP_NON_READ_TOOLS = frozenset( - { - "add", - "extend", - "import_slice", - "ingest_codebase", - "ingest_pcba", - "ingest_skills", - "ingest_sysml", - "mutate", - "release", - "reserve", - "session_acl_bind", - "session_acl_enable", - "session_acl_grant", - "session_close", - "session_load", - "session_open", - "session_save", - "snap_model", - "update", - } -) -# CLI function name -> surface name, where the CLI function is named differently -# from its MCP tool or classification entry. Other session-scoped commands match by name. -CLI_SURFACE_ALIAS = { - "add_cmd": "add", - "delete_cmd": "delete", - "export_pin_map_cmd": "export_pin_map", - "extend_cmd": "extend", - "import_slice_cmd": "import_slice", - "ingest_codebase_cmd": "ingest_codebase", - "ingest_pcba_cmd": "ingest_pcba", - "ingest_skills_cmd": "ingest_skills", - "ingest_sysml_cmd": "ingest_sysml", - "mutate_cmd": "mutate", - "prune_stale_cmd": "prune_stale", - "query_find": "find", - "query_pin_map": "pin_map", - "release_cmd": "release", - "reserve_cmd": "reserve", - "update_cmd": "update", -} -# Session-scoped CLI writes and prunes with no MCP tool of the same name. -CLI_ONLY_NON_READ = frozenset( - {"delete", "prune_dangling", "prune_orphans", "prune_recyclable", "prune_stale"} -) +# A session-scoped CLI parameter names a session by one of these names, or by a +# typer long option whose name is one of them (or contains "session"), e.g. --session. +SESSION_PARAM_NAMES = frozenset({"session", "session_id", "sid", "sess", "target"}) def _read(path: Path) -> str: @@ -96,12 +65,14 @@ def _verify_docs(text: str) -> dict[str, str]: def _cited_tests(doc: str) -> set[str]: - """Test names cited in a doc, ignoring the runtime file path itself.""" - return set(re.findall(r"\btest_\w+", doc.replace("tests/test_session_evict.py", ""))) + """Test names cited in a doc, ignoring the runtime file paths themselves.""" + for path in RUNTIME_FILES: + doc = doc.replace(path, "") + return set(re.findall(r"\btest_\w+", doc)) -def _runtime_test_names() -> set[str]: - tree = ast.parse(_read(RUNTIME)) +def _runtime_test_names(path: Path = RUNTIME) -> set[str]: + tree = ast.parse(_read(path)) return { n.name for n in tree.body if isinstance(n, ast.FunctionDef) and n.name.startswith("test_") } @@ -125,7 +96,7 @@ def test_verify_defs_s03_to_s09_present(): def test_each_verify_doc_names_runtime_pytests_that_exist(): docs = _verify_docs(_read(VERIFY)) - names = _runtime_test_names() + names = _runtime_test_names() | _runtime_test_names(READ_TOUCH) for ver_id in VER_IDS: doc = docs[ver_id] assert "tests/test_session_evict.py" in doc, f"{ver_id} must name its runtime file" @@ -140,7 +111,8 @@ def test_every_runtime_test_is_cited_by_a_verify_doc(): for ver_id in VER_IDS: doc = docs[ver_id] cited |= _cited_tests(doc) - assert _runtime_test_names() == cited + # Read-touch tests are cited too, but only the session-evict file must be fully cited here. + assert _runtime_test_names() == cited - _runtime_test_names(READ_TOUCH) def _deploy_flag(name: str) -> bool: @@ -176,6 +148,18 @@ def _xfail_mark() -> tuple[bool, bool | None]: return False, None +def _get_session_xfail_marks() -> list: + """The xfail marks on the get_session parameter of the read-touch regression test.""" + (param,) = [p for p in SURFACE_PARAMS if p.values[0] == "get_session"] + return [m for m in param.marks if m.name == "xfail"] + + +def _open_stamps_xfail_marks() -> list: + """The xfail marks on test_open_stamps_first_touch in the read-touch regression module.""" + test = read_touch.test_open_stamps_first_touch + return [m for m in getattr(test, "pytestmark", []) if m.name == "xfail"] + + def _status_guards(flag: str = "evictShipped") -> dict[str, list[bool]]: """Per MN-VER-05-S03..S09 def, the value of ``flag`` its status guard requires.""" guards: dict[str, list[bool]] = {} @@ -197,6 +181,22 @@ def test_ship_flags_flip_together(): assert not_shipped or shipped_ok, ( "evictShipped, the deploy satisfy link and the runtime xfail mark must flip together" ) + get_marks = _get_session_xfail_marks() + if shipped: + assert not get_marks, "get_session read param must drop its xfail mark when the rule ships" + else: + assert len(get_marks) == 1 and get_marks[0].kwargs.get("strict") is True, ( + "get_session read param must stay xfail(strict=True) until the touch rule ships" + ) + open_marks = _open_stamps_xfail_marks() + if shipped: + assert not open_marks, ( + "test_open_stamps_first_touch must drop its xfail mark when the rule ships" + ) + else: + assert len(open_marks) == 1 and open_marks[0].kwargs.get("strict") is True, ( + "test_open_stamps_first_touch must stay xfail(strict=True) until the touch rule ships" + ) assert _deploy_flag("commitRefusesLostLease") == shipped, ( "commitRefusesLostLease must flip with evictShipped (both false now, both true at ship)" ) @@ -234,22 +234,22 @@ def _block_names(text: str, name: str) -> list[str]: return [line.strip() for line in body.splitlines() if line.strip()] -def _module_tuple(name: str) -> tuple[str, ...]: - """A string-tuple module constant of the runtime test file, read without importing it.""" - for node in ast.parse(_read(RUNTIME)).body: - if isinstance(node, ast.Assign) and any( - isinstance(t, ast.Name) and t.id == name for t in node.targets - ): - return tuple(ast.literal_eval(node.value)) - raise AssertionError(f"{name} must be a module constant in tests/test_session_evict.py") +def test_surface_blocks_match_shared_constants(): + text = _read(REQ) + for block, names in ( + ("READ-SURFACES", READ_SURFACES), + ("NON-TOUCH-READS", NON_TOUCH_READS), + ("MAINTENANCE-SAVES", MAINTENANCE_SAVES), + ): + listed = _block_names(text, block) + assert len(listed) == len(set(listed)), f"{block} must not repeat a surface" + assert set(listed) == set(names), f"{block} must equal its tests/evict_surfaces.py list" -def test_surface_blocks_match_runtime_constants(): - text = _read(REQ) - for block, const in (("READ-SURFACES", "READ_SURFACES"), ("ADMIN-READS", "ADMIN_READS")): - names = _block_names(text, block) - assert len(names) == len(set(names)), f"{block} must not repeat a surface" - assert set(names) == set(_module_tuple(const)), f"{block} must equal {const}" +def test_surface_lists_are_disjoint(): + reads, nontouch, saves = set(READ_SURFACES), set(NON_TOUCH_READS), set(MAINTENANCE_SAVES) + assert not (reads & nontouch), "a read cannot be both a touch and a non-touch read" + assert not (saves & (reads | nontouch)), "a save is neither a read surface nor a read" def test_every_caller_mcp_read_tool_is_listed(): @@ -257,31 +257,69 @@ def test_every_caller_mcp_read_tool_is_listed(): from memnet_mcp.server import mcp registered = {t.name for t in asyncio.run(mcp.list_tools())} - reads = set(_module_tuple("READ_SURFACES")) - admin = set(_module_tuple("ADMIN_READS")) - cli_only = set(_module_tuple("CLI_READ_ARGV")) + reads = set(READ_SURFACES) + nontouch = set(NON_TOUCH_READS) + cli_only = set(CLI_READ_ARGV) assert MCP_NON_READ_TOOLS <= registered, "MCP_NON_READ_TOOLS names an unregistered tool" assert not (reads & MCP_NON_READ_TOOLS), "a READ_SURFACES entry must not be a non-read tool" - assert not (admin & MCP_NON_READ_TOOLS), "an ADMIN_READS entry must not be a non-read tool" - unlisted = registered - MCP_NON_READ_TOOLS - reads - admin + assert not (nontouch & MCP_NON_READ_TOOLS), "a NON_TOUCH_READS entry must not be a non-read" + unlisted = registered - MCP_NON_READ_TOOLS - reads - nontouch assert not unlisted, f"classify these MCP tools as read or non-read: {sorted(unlisted)}" # get_session is the in-process read; CLI_READ_ARGV names the CLI-only reads; # every other READ entry is an MCP tool. mcp_reads = reads - {"get_session"} - cli_only assert mcp_reads <= registered, "a READ_SURFACES MCP name is not registered" - # Admin entries that are not MCP tools must be real `memnet admin` commands. + # Non-touch entries that are not MCP tools must be real `memnet admin` commands. admin_cmds = {"admin_" + c.name.replace("-", "_") for c in admin_app.registered_commands} - assert (admin - registered) <= admin_cmds, "ADMIN_READS names an admin command that is absent" + assert (nontouch - registered) <= admin_cmds, "NON_TOUCH_READS names an absent command" + # Maintenance saves that are not MCP tools or admin commands must be engine saves. + saves_unknown = set(MAINTENANCE_SAVES) - registered - admin_cmds - ENGINE_SAVES + assert not saves_unknown, ( + f"MAINTENANCE_SAVES names no tool, command or engine save: {saves_unknown}" + ) + assert ENGINE_SAVES <= set(MAINTENANCE_SAVES), "ENGINE_SAVES must be maintenance saves" -def _cli_session_commands() -> dict[str, str]: - """CLI function name -> surface name, for every session-scoped command in cli.py. +def _session_named(name: str) -> bool: + return name in SESSION_PARAM_NAMES or "session" in name + + +def _session_param(arg: ast.arg, default: ast.expr | None) -> bool: + """A typer parameter that names a session: by its own name, or by a long option.""" + if _session_named(arg.arg): + return True + for expr in (arg.annotation, default): + if expr is None: + continue + for node in ast.walk(expr): + if ( + isinstance(node, ast.Constant) + and isinstance(node.value, str) + and node.value.startswith("--") + and _session_named(node.value[2:].replace("-", "_")) + ): + return True + return False + + +def _signature_params(fn: ast.FunctionDef) -> list[tuple[ast.arg, ast.expr | None]]: + """Positional and keyword-only parameters, each with its default (or None).""" + pos = fn.args.args + pos_defaults = [None] * (len(pos) - len(fn.args.defaults)) + list(fn.args.defaults) + kw_defaults = fn.args.kw_defaults + return list(zip(pos, pos_defaults, strict=True)) + list( + zip(fn.args.kwonlyargs, kw_defaults, strict=True) + ) + + +def _session_commands_in(source: str) -> dict[str, str]: + """CLI function name -> surface name, for each session-scoped typer command in source. cli.py registers commands with typer (``@.command(...)``), not argparse. A command is session-scoped when one of its parameters names a session. """ found: dict[str, str] = {} - for node in ast.parse(_read(CLI)).body: + for node in ast.parse(source).body: if not isinstance(node, ast.FunctionDef): continue is_command = any( @@ -290,25 +328,55 @@ def _cli_session_commands() -> dict[str, str]: and d.func.attr == "command" for d in node.decorator_list ) - params = [a.arg for a in node.args.args] - if is_command and any("session" in p for p in params): + if is_command and any(_session_param(a, d) for a, d in _signature_params(node)): found[node.name] = CLI_SURFACE_ALIAS.get(node.name, node.name) return found +def _cli_session_commands() -> dict[str, str]: + return _session_commands_in(_read(CLI)) + + +_CLASSIFIER_SNIPPET = """ +@app.command() +def by_keyword(*, sid: Annotated[str, typer.Option("--ident")] = ""): ... + +@app.command() +def by_option(name: Annotated[str, typer.Option("--session")] = ""): ... + +@app.command() +def by_target(*, target: str): ... + +@app.command() +def unrelated(*, count: int = 0): ... + +def helper(session: str): ... +""" + + +def test_session_classifier_sees_keyword_only_and_aliased_params(): + found = _session_commands_in(_CLASSIFIER_SNIPPET) + assert set(found) == {"by_keyword", "by_option", "by_target"}, ( + "keyword-only sid, a --session option under another name, and target must all count; " + "a non-command helper and an unrelated keyword must not" + ) + + def test_every_cli_session_command_is_classified(): from memnet_mcp.server import mcp registered = {t.name for t in asyncio.run(mcp.list_tools())} - reads = set(_module_tuple("READ_SURFACES")) - admin = set(_module_tuple("ADMIN_READS")) - cli_only = set(_module_tuple("CLI_READ_ARGV")) + reads = set(READ_SURFACES) + nontouch = set(NON_TOUCH_READS) + saves = set(MAINTENANCE_SAVES) + cli_only = set(CLI_READ_ARGV) commands = _cli_session_commands() assert commands, "no session-scoped CLI command found in cli.py; the parser has moved" - classified = reads | admin | MCP_NON_READ_TOOLS | CLI_ONLY_NON_READ + classified = reads | nontouch | saves | MCP_NON_READ_TOOLS | CLI_ONLY_NON_READ unclassified = sorted(f for f, surface in commands.items() if surface not in classified) assert not unclassified, ( - f"classify these session-scoped CLI commands as read, admin or non-read: {unclassified}" + f"classify these session-scoped CLI commands as read, non-touch read, save or non-read: " + f"{unclassified}" ) # Every CLI-only read must be a real session-scoped command, and every read # that is not an MCP tool must be a CLI-only read with its argv.