Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 0 additions & 13 deletions dsl/std/abi.dag
Original file line number Diff line number Diff line change
@@ -1,21 +1,9 @@
// std/abi.dag — arch-agnostic ABI vocabulary for the §10 execution-contract layer.
//
// Scope: ArchitecturalRegister (open atom identity) and CallingConvention (closed syscall-role
// set encoded as a record — one field per role for totality by construction). Cited per-arch
// register atoms inhabit ArchitecturalRegister in extdeps/runtime/abi/*.dag (M3); std never
// names amd64.
//
// Uses only Int / Bool / NonEmptyStr / List / records / enums — no distribution-enum imports.

module std.abi

import std.types { Bool, NonEmptyStr }

// Open register atom identity (a node). Per-arch cited atoms (e.g. Amd64Gpr) inhabit this in
// extdeps — identity only; register name is an attribute of the cited atom, not a string key.
type ArchitecturalRegister

// Closed syscall-role set (arg0..arg5, syscall_number, return_value) as record fields.
type CallingConvention {
arg0: ArchitecturalRegister
arg1: ArchitecturalRegister
Expand All @@ -27,7 +15,6 @@ type CallingConvention {
return_value: ArchitecturalRegister
}

// Stack growth direction for stack-based conventions (function-call ABIs land in later slices).
type StackLayout {
grows_down: Bool
}
33 changes: 0 additions & 33 deletions dsl/std/access.dag
Original file line number Diff line number Diff line change
@@ -1,55 +1,22 @@
// std/access.dag -- the access-control abstraction, DERIVED from extdeps/access (not re-coined).
//
// The commonality of the systems modeled in extdeps/access (zanzibar, aws_iam, posix, rbac) and
// the vendor IAMs (cloud/gcp/iam, github): every one answers the same question — may this SUBJECT
// perform this ACTION on this OBJECT? The decision procedure differs per system, so this is the
// agnostic query/decision shape — DESIGN §4 Realization (one interface, N system handlers) — NOT
// any single system's mechanism. Validated by test/claim/access_validation_test.dag, which maps each
// extdeps system into this shape; if a system can't be expressed, this abstraction is wrong.
//
// Derivation receipt (what they share, and where the shape STRAINS):
// * An attribute-carrying Subject / Action / Object triple — fits POSIX (DAC), RBAC, Zanzibar
// (ReBAC), GitHub, AND AWS IAM (ABAC) once S/A/O carry their attributes (see RESOLVED below).
// The generic params are meant to be instantiated with RICH types (a subject with its claims,
// an action with its parameters), not bare ids.
// * Decision = Permit | Deny, combined Deny-wins (AWS IAM explicit-deny-overrides; the
// conservative / fail-closed meet — DESIGN §5).
// * Subject indirection (roles / usersets / owner-classes / group membership) is each system's
// `decide` internals, not part of the shared shape.
// * RESOLVED (was "ABAC needs a context dimension"): AWS IAM Conditions do NOT need a new opaque
// dimension — they DECOMPOSE. Most condition keys are attribute-carrying S/A/O (s3:prefix → an
// ACTION parameter; principal/resource tags → subject/object attributes); the environmental
// remainder grounds in frameworks we already have (aws:SourceIp internal-CIDR → the request's
// NetworkLocality; aws:CurrentTime → Timestamp). So `decide` reads grounded S/A/O fields, never
// an opaque context map — the generics suffice and this core is UNCHANGED. Validated by
// test.claim.access_iam_validation (an aws:SourceIp + s3:prefix + MFA statement decided entirely
// from grounded fields, with no context type). "Context" as a `C` dimension was itself a nickname.
// * STRAIN: Zanzibar fuses action + subject-grouping into one `relation` — it maps, but the
// action and the grouping key are the same string.

module std.access

type AccessDecision
= Permit
| Deny

// Conservative combine: Deny wins (AWS IAM explicit-deny-overrides; the fail-closed meet, §5).
fn decision_meet(a: AccessDecision, b: AccessDecision) -> AccessDecision {
match a {
Deny => Deny
Permit => b
}
}

// The universal access query.
type AccessRequest<S, A, O> {
subject: S
action: A
object: O
}

// A system inhabits the abstraction by providing a `decide`. The data witnesses in
// test/claim/access_validation_test.dag (posix_access_policy, rbac_access_policy, …) are the validation.
type AccessPolicy<S, A, O> {
decide: fn(AccessRequest<S, A, O>) -> AccessDecision
}
Loading
Loading