cls
9dfa06ffee
Docker image / Build (linux/amd64) (push) Has been cancelled
Docker image / Build (linux/arm64) (push) Has been cancelled
Docker image / Merge release multi-arch manifest (push) Has been cancelled
Docker image / Merge debug multi-arch manifest (push) Has been cancelled
Docker image / Build public push gateway (linux/amd64) (push) Has been cancelled
Docker image / Build public push gateway (linux/arm64) (push) Has been cancelled
Docker image / Publish public push gateway image (push) Has been cancelled
Sprig image / Build (linux/amd64) (push) Has been cancelled
Sprig image / Build (linux/arm64) (push) Has been cancelled
Sprig image / Merge multi-arch manifest (push) Has been cancelled
Harbor Buzz Orchestra / Python tests and lint (push) Has been cancelled
CI / Detect Changed Paths (push) Has been cancelled
CI / Rust Lint (push) Has been cancelled
CI / Unit Tests (push) Has been cancelled
CI / Desktop Core (push) Has been cancelled
CI / Desktop Smoke E2E (1) (push) Has been cancelled
CI / Desktop Smoke E2E (2) (push) Has been cancelled
CI / Desktop Smoke E2E (3) (push) Has been cancelled
CI / Desktop Smoke E2E (4) (push) Has been cancelled
CI / Desktop (push) Has been cancelled
CI / Desktop E2E Relay (push) Has been cancelled
CI / Desktop E2E Integration (1/2) (push) Has been cancelled
CI / Desktop E2E Integration (2/2) (push) Has been cancelled
CI / Desktop E2E Integration (push) Has been cancelled
CI / Backend Integration (relay e2e) (push) Has been cancelled
CI / Relay E2E (push) Has been cancelled
CI / Web (push) Has been cancelled
CI / Mobile (push) Has been cancelled
CI / Security (push) Has been cancelled
CI / Dead Token Reference Guard (push) Has been cancelled
CI / Server Cross-Compile (aarch64-unknown-linux-musl) (push) Has been cancelled
CI / Server Cross-Compile (x86_64-unknown-linux-musl) (push) Has been cancelled
CI / Windows Rust (x86_64-pc-windows-msvc) (push) Has been cancelled
CI / Desktop Build (macOS) (push) Has been cancelled
helm chart / lint + unittest + render matrix (push) Has been cancelled
helm chart / install on kind (gated) (push) Has been cancelled
helm chart / publish chart to GHCR (push) Has been cancelled
Mesh Lifecycle / Relay-Driven Mesh Lifecycle Smoke (push) Has been cancelled
Sprig / Build (aarch64-unknown-linux-musl) (push) Has been cancelled
Sprig / Build (x86_64-unknown-linux-musl) (push) Has been cancelled
Sprig / Publish rolling release (push) Has been cancelled
Sprig / Publish tagged release (push) Has been cancelled
Signed-off-by: cls_宁波本机 <908705107@qq.com>
38 lines
2.1 KiB
Markdown
38 lines
2.1 KiB
Markdown
---
|
|
title: "NIP-PL Formal Models: lease acceptance and stateful gateway authority"
|
|
tags: [nostr, nip-pl, push-notifications, formal-model, buzz]
|
|
status: active
|
|
created: 2026-07-11
|
|
---
|
|
|
|
# NIP-PL formal pressure test
|
|
|
|
These bounded executable models cover two distinct shipped contracts. They do not model the not-yet-shipped relay matcher/worker or any removed wake-grant protocol.
|
|
|
|
## Run
|
|
|
|
```bash
|
|
python3 acceptance.py
|
|
python3 mutation_test.py
|
|
python3 delivery.py
|
|
python3 delivery_mutation.py
|
|
python3 fixed_payload.py
|
|
python3 fixed_payload_mutation.py
|
|
```
|
|
|
|
## Lease acceptance
|
|
|
|
`acceptance.py` explores all 5040 orderings of one address's active, revoke, reactivate, replay, NIP-01-tie, high-generation/old-created-at, and high-created-at/stale-generation candidates. It checks no resurrection, monotone watermarks, no watermark poisoning, agreement between stored and effective state, and replay-window safety. `mutation_test.py` independently drops the NIP-01 and generation clauses and requires both mutants to produce witnesses.
|
|
|
|
## Stateful public gateway
|
|
|
|
`delivery.py` models the authority actually shipped by the public gateway: relay signer confinement; installation/delegation epoch, generation, and expiry; atomic replay/quota admission; revocation ordering; custody; terminal request burn versus transient release; and the exact constant APNs body. `delivery_mutation.py` requires signer, epoch, terminal-burn, quota-refund, and fixed-body mutants to be detected.
|
|
|
|
## Fixed payload
|
|
|
|
`fixed_payload.py` exhaustively varies relay-controlled and gateway-state inputs and requires the APNs body to remain byte-identical to the normative constant. `fixed_payload_mutation.py` injects each prohibited input category and requires every mutation to be caught.
|
|
|
|
## Honest limits
|
|
|
|
The models enumerate bounded abstract transitions, not SQL schedules or network behavior. Real PostgreSQL race/FK/retention tests validate the implementation separately. A crash after APNs accepts but before disposition persistence remains intentionally at-least-once; request expiry bounds the resulting replay reservation. Constant payload prevents content disclosure but cannot hide wake timing or frequency.
|