Pith Number

pith:H6S4RIPS

pith:2026:H6S4RIPSDSQOWDDUSGUEFVV5BJ

not attested not anchored not stored refs resolved

First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation

Deepak Garg, Derek Dreyer, Emanuele D'Osualdo, Iona Kuhn, Janine Lohse, Jimmy Xin, Niklas M\"uck, Tim Rohde

Amaryllis is the first general-purpose probabilistic logic to support independence, conditioning, and dynamic memory allocation.

arxiv:2605.13765 v1 · 2026-05-13 · cs.LO · cs.PL

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{H6S4RIPSDSQOWDDUSGUEFVV5BJ}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

Amaryllis is the first GPL to support independence and conditional reasoning while also handling dynamic memory allocation.

C2weakest assumption

The indexed valuation-style model can be soundly integrated with Iris-style resource algebras for dynamic allocation without breaking independence or conditioning properties.

C3one line summary

Amaryllis is the first general-purpose probabilistic separation logic supporting dynamic memory allocation, independence, and conditioning, with a mechanized soundness proof in Rocq.

References

37 extracted · 37 resolved · 0 Pith anchors

[1] Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal 2024 · doi:10.1145/3674635

[2] Amal Ahmed. 2004. Semantics of types for mutable state . Ph.D. Dissertation. Princeton University 2004

[3] First Steps Towards Probabilistic Iris: A Separation Logic with Independence, Conditioning, and Dynamic Heap Allocation 2026

[4] [Bau06] Andrej Bauer 2001 · doi:10.1145/504709.504712

[5] Jialu Bao, Emanuele D’Osualdo, and Azadeh Farzan. 2025. Bluebell: an alliance of relational lifting and independence for probabilistic reasoning. Proc. ACM Program. Lang., 9, POPL, 1719–1749. doi: 10. 2025 · doi:10.1145/3704894

Receipt and verification

First computed	2026-05-18T02:44:16.108191Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

3fa5c8a1f21ca0eb0c7491a842d6bd0a647cdbf34b05c54c655544c91ff62c31

Aliases

arxiv: 2605.13765 · arxiv_version: 2605.13765v1 · doi: 10.48550/arxiv.2605.13765 · pith_short_12: H6S4RIPSDSQO · pith_short_16: H6S4RIPSDSQOWDDU · pith_short_8: H6S4RIPS

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/H6S4RIPSDSQOWDDUSGUEFVV5BJ \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 3fa5c8a1f21ca0eb0c7491a842d6bd0a647cdbf34b05c54c655544c91ff62c31

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "df24d7f5045c44d8f03eee2213b3e75e7b4a5e3588a5318af00ea8e5a2d1e6c5",
    "cross_cats_sorted": [
      "cs.PL"
    ],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-13T16:46:19Z",
    "title_canon_sha256": "a4f3f53a6c20aaa9d5b75bd698ccfc37e0c249ddbdff2c29d42f59ab9694cac4"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.13765",
    "kind": "arxiv",
    "version": 1
  }
}