IAM contract

Peak merchant authorization is a default-deny relationship model implemented by the shared IAM engine and verified by the executable Dafny specification. Use this page to understand the runtime decision; use the linked code and specification when changing it.

Canonical sources

• Formal model and proofs: apps/specifications/dafny/iam/main.dfy
• Functional companion: IAM_SPEC.md
• Runtime adapter: DafnyIamAdapter.kt
• Runtime service: IamService.kt
• Merchant role and permission catalog: MerchantIamPermissions.kt
• Merchant policy persistence: IamRepository.kt

The Merchant API OpenAPI contract describes IAM management operations. The runtime sources above define what an authorization decision means.

Relationship model

The effective chain is:

user -> role assignment -> group -> policy -> action/resource decision

An organization IAM seed creates the standard groups, policies, and role relationships. Assigning a role gives the user its group-backed policies; it does not copy permissions onto the user.

Current seeded merchant roles are:

Role	Intended scope
org_owner	Organization ownership and full organization administration
org_admin	Organization administration without changing ownership
org_member	Baseline organization membership
store_admin	Store administration
store_manager	Store operations and staff management
stocker	Store inventory, serialized inventory, transfers, and self-shift access
store_user	Baseline store operations

org_manager and cashier are not current seeded role IDs. Do not write them to the API or use them in support runbooks.

Runtime decision

For the authenticated user and organization, IamService ensures the organization seed exists, loads the user's effective policies, and sends the requested action/resource to the compiled Dafny evaluator.

The evaluator follows this precedence:

1. A matching explicit deny denies.
2. Otherwise, a matching permit allows.
3. Otherwise, the request is denied.

Structurally invalid policies are ignored rather than granting access. Policies with conditions are also skipped because conditional evaluation is reserved but not active. Store-scoped controllers therefore retain explicit organization/store membership and ownership checks before or alongside the fine-grained IAM decision.

Request enforcement

IAM is not the authentication layer. A typical Merchant API request first provides a Firebase ID token and a merchant Peak authorization token. The controller then requires a named permission, while the service verifies the resource belongs to the organization or store in the request.

These checks answer different questions:

• Authentication: which Firebase principal made the request?
• Token context: which Peak tenant and principal type is active?
• Membership: does the user belong to this organization/store?
• IAM: may the effective policies perform this action on this resource?
• Ownership: does the loaded record actually belong to the requested organization/store?

Passing one check never implies the others. Always load or query resources within the authenticated organization scope; do not authorize a record solely from a caller-supplied ID.

Separate authorization domains

Merchant roles govern merchant resources. They do not grant support-staff permissions, account access, or internal service access.

• Support and agent routes use the Management API's mgmt.* permissions and support/agent Peak token types.
• Account routes use account membership and account-scoped permissions.
• Internal routes use Cloud Run service identity, expected audiences, and principal allowlists.
• Terminal device routes use mutual TLS and enrolled device identity.

Do not translate a merchant role into one of these domains or reuse its token across the boundary.

Change and verification checklist

When adding a permission or changing a role:

1. Update the canonical permission/role catalog and organization seed.

2. Update controller annotations and service ownership checks.

3. Update the Dafny and companion specifications if decision semantics change.

4. Add tests for permit, explicit deny, default deny, and cross-scope access affected by the change.

5. Regenerate API contracts if IAM endpoints or DTOs changed.

6. Run the focused verification:

   bazel build //apps/specifications/dafny:verify
   bazel test //libs/microservices/iam-engine:iam_engine_test

An IAM change is incomplete if the seed, runtime catalog, controller annotation, and executable model disagree.