chore: include all pending refoundation and runtime changes

Author: francescomaiomascio

Documentation/formal/tla/yai_enforcement.tla

@@ -2,7 +2,7 @@
 EXTENDS Naturals
 
 EnforcementStatus == {"ok", "error"}
-EnforcementCode == {"OK", "AUTHORITY_BLOCK", "POLICY_BLOCK", "WORKSPACE_BIND_MISMATCH"}
+EnforcementCode == {"OK", "AUTHORITY_BLOCK", "POLICY_BLOCK", "SCOPE_BIND_MISMATCH"}
 ReviewStates == {"clear", "blocked", "review_required"}
 
 EnforcementInvariant(status, code, reviewState) ==

Documentation/formal/tla/yai_scope_state.tla

@@ -0,0 +1,12 @@
+--------------------- MODULE yai_scope_state ---------------------
+EXTENDS Naturals
+
+ScopeStates == {"created", "active", "attached", "suspended", "destroyed", "error"}
+
+ScopeInvariant(state, runtimeAttached, wsId) ==
+  /\ state \in ScopeStates
+  /\ runtimeAttached \in BOOLEAN
+  /\ wsId \in STRING
+  /\ state = "attached" => runtimeAttached
+
+=============================================================================

Documentation/formal/tla/yai_system.tla

@@ -5,7 +5,7 @@ INSTANCE yai_ids
 INSTANCE yai_authority
 INSTANCE yai_resolution
 INSTANCE yai_runtime_state
-INSTANCE yai_workspace_state
+INSTANCE yai_scope_state
 INSTANCE yai_enforcement
 INSTANCE yai_protocol_control
 INSTANCE yai_traceability
@@ -20,7 +20,7 @@ CONSTANTS
 
 VARIABLES
   runtimeState,
-  workspaceState,
+  scopeState,
   authorityLevel,
   policyMode,
   grantValidity,
@@ -31,7 +31,7 @@ VARIABLES
 
 TypeInvariant ==
   /\ yai_runtime_state!RuntimeTypeInvariant(runtimeState, MaxEnergy, TRUE)
-  /\ yai_workspace_state!WorkspaceInvariant(workspaceState, TRUE, "ws")
+  /\ yai_scope_state!ScopeInvariant(scopeState, TRUE, "ws")
   /\ yai_authority!AuthorityTypeInvariant(authorityLevel, "allow")
   /\ yai_policy_application!PolicyApplicationInvariant(policyMode, 1, 1, "snapshot")
   /\ yai_grants!GrantInvariant(grantValidity, 1, 2, 3)
@@ -45,7 +45,7 @@ TypeInvariant ==
 
 Init ==
   /\ runtimeState = "ready"
-  /\ workspaceState = "attached"
+  /\ scopeState = "attached"
   /\ authorityLevel = "operator"
   /\ policyMode = "active"
   /\ grantValidity = "valid"
@@ -56,7 +56,7 @@ Init ==
 
 Next ==
   /\ runtimeState' \in {"ready", "running", "suspend"}
-  /\ workspaceState' \in {"attached", "active", "suspended"}
+  /\ scopeState' \in {"attached", "active", "suspended"}
   /\ authorityLevel' \in {"none", "operator", "system"}
   /\ policyMode' \in {"pending", "active"}
   /\ grantValidity' \in {"valid", "refresh_required", "expired", "revoked"}
@@ -65,7 +65,7 @@ Next ==
   /\ reviewState' \in {"clear", "review_required", "blocked", "escalated"}
   /\ traceId' \in Nat
 
-Spec == Init /\ [][Next]_<<runtimeState, workspaceState, authorityLevel, policyMode, grantValidity, containmentMode, enforcementStatus, reviewState, traceId>>
+Spec == Init /\ [][Next]_<<runtimeState, scopeState, authorityLevel, policyMode, grantValidity, containmentMode, enforcementStatus, reviewState, traceId>>
 
 THEOREM Spec => []TypeInvariant
 =============================================================================

Documentation/formal/tla/yai_workspace_state.tla

@@ -27,9 +27,9 @@
     },
     {
       "id": "F-005-scope-binding",
-      "modules": ["yai_workspace_state", "yai_runtime_state"],
+      "modules": ["yai_scope_state", "yai_runtime_state"],
       "configs": ["yai_system.deep.cfg"],
-      "runtime_surfaces": ["runtime_capabilities_bind_workspace"]
+      "runtime_surfaces": ["runtime_capabilities_bind_scope"]
     }
   ]
 }

Documentation/formal/traceability/invariant-linkage.json

@@ -6,7 +6,7 @@
     "yai_authority": ["runtime/authority", "runtime/enforcement", "governance/authority"],
     "yai_resolution": ["governance/resolution", "governance/manifests"],
     "yai_runtime_state": ["runtime/lifecycle", "runtime/session"],
-    "yai_workspace_state": ["runtime/scope", "data/binding"],
+    "yai_scope_state": ["runtime/scope", "data/binding"],
     "yai_policy_application": ["runtime/policy", "governance/policy_effects"],
     "yai_grants": ["runtime/grants", "runtime/containment", "edge"],
     "yai_containment": ["runtime/containment", "runtime/enforcement"],

Documentation/formal/traceability/model.map.json

@@ -68,8 +68,8 @@ int yai_init_system_shm(void)
     }
 
     memset(vault, 0, sizeof(yai_vault_t));
-    strncpy(vault->workspace_id, SYSTEM_WS, MAX_WS_ID - 1);
-    vault->workspace_id[MAX_WS_ID - 1] = '\0';
+    strncpy(vault->scope_id, SYSTEM_WS, MAX_WS_ID - 1);
+    vault->scope_id[MAX_WS_ID - 1] = '\0';
 
     if (munmap(vault, sizeof(yai_vault_t)) != 0) {
         perror("[YAI-RUNTIME] munmap failed");

Documentation/yai/YAI_OS_TOPOLOGY.md

@@ -233,7 +233,7 @@ extern char _end;
 
 /* KSEG addresses for the uncompressed kernel.
 
-   Note that the end address includes workspace for the decompression.
+   Note that the end address includes scope for the decompression.
    Note also that the DATA_START address is ZERO_PGE, to which we write
    just before jumping to the kernel image at START_ADDR.
  */