Apr 07, 5-6 AM (17)
Apr 07, 6-7 AM (6)
Apr 07, 7-8 AM (14)
Apr 07, 8-9 AM (35)
Apr 07, 9-10 AM (38)
Apr 07, 10-11 AM (25)
Apr 07, 11-12 PM (63)
Apr 07, 12-1 PM (38)
Apr 07, 1-2 PM (56)
Apr 07, 2-3 PM (54)
Apr 07, 3-4 PM (25)
Apr 07, 4-5 PM (36)
Apr 07, 5-6 PM (19)
Apr 07, 6-7 PM (22)
Apr 07, 7-8 PM (21)
Apr 07, 8-9 PM (20)
Apr 07, 9-10 PM (16)
Apr 07, 10-11 PM (41)
Apr 07, 11-12 AM (21)
Apr 08, 12-1 AM (13)
Apr 08, 1-2 AM (6)
Apr 08, 2-3 AM (9)
Apr 08, 3-4 AM (9)
Apr 08, 4-5 AM (4)
Apr 08, 5-6 AM (21)
Apr 08, 6-7 AM (40)
Apr 08, 7-8 AM (72)
Apr 08, 8-9 AM (42)
Apr 08, 9-10 AM (24)
Apr 08, 10-11 AM (56)
Apr 08, 11-12 PM (43)
Apr 08, 12-1 PM (36)
Apr 08, 1-2 PM (64)
Apr 08, 2-3 PM (45)
Apr 08, 3-4 PM (17)
Apr 08, 4-5 PM (16)
Apr 08, 5-6 PM (17)
Apr 08, 6-7 PM (27)
Apr 08, 7-8 PM (12)
Apr 08, 8-9 PM (11)
Apr 08, 9-10 PM (6)
Apr 08, 10-11 PM (50)
Apr 08, 11-12 AM (18)
Apr 09, 12-1 AM (7)
Apr 09, 1-2 AM (5)
Apr 09, 2-3 AM (2)
Apr 09, 3-4 AM (4)
Apr 09, 4-5 AM (6)
Apr 09, 5-6 AM (15)
Apr 09, 6-7 AM (36)
Apr 09, 7-8 AM (22)
Apr 09, 8-9 AM (25)
Apr 09, 9-10 AM (33)
Apr 09, 10-11 AM (20)
Apr 09, 11-12 PM (60)
Apr 09, 12-1 PM (68)
Apr 09, 1-2 PM (43)
Apr 09, 2-3 PM (74)
Apr 09, 3-4 PM (22)
Apr 09, 4-5 PM (51)
Apr 09, 5-6 PM (26)
Apr 09, 6-7 PM (23)
Apr 09, 7-8 PM (21)
Apr 09, 8-9 PM (39)
Apr 09, 9-10 PM (18)
Apr 09, 10-11 PM (29)
Apr 09, 11-12 AM (15)
Apr 10, 12-1 AM (5)
Apr 10, 1-2 AM (4)
Apr 10, 2-3 AM (4)
Apr 10, 3-4 AM (12)
Apr 10, 4-5 AM (3)
Apr 10, 5-6 AM (9)
Apr 10, 6-7 AM (30)
Apr 10, 7-8 AM (45)
Apr 10, 8-9 AM (47)
Apr 10, 9-10 AM (20)
Apr 10, 10-11 AM (61)
Apr 10, 11-12 PM (70)
Apr 10, 12-1 PM (46)
Apr 10, 1-2 PM (23)
Apr 10, 2-3 PM (36)
Apr 10, 3-4 PM (33)
Apr 10, 4-5 PM (38)
Apr 10, 5-6 PM (30)
Apr 10, 6-7 PM (11)
Apr 10, 7-8 PM (13)
Apr 10, 8-9 PM (7)
Apr 10, 9-10 PM (25)
Apr 10, 10-11 PM (47)
Apr 10, 11-12 AM (18)
Apr 11, 12-1 AM (6)
Apr 11, 1-2 AM (4)
Apr 11, 2-3 AM (2)
Apr 11, 3-4 AM (0)
Apr 11, 4-5 AM (8)
Apr 11, 5-6 AM (4)
Apr 11, 6-7 AM (5)
Apr 11, 7-8 AM (7)
Apr 11, 8-9 AM (3)
Apr 11, 9-10 AM (0)
Apr 11, 10-11 AM (10)
Apr 11, 11-12 PM (4)
Apr 11, 12-1 PM (7)
Apr 11, 1-2 PM (3)
Apr 11, 2-3 PM (7)
Apr 11, 3-4 PM (12)
Apr 11, 4-5 PM (18)
Apr 11, 5-6 PM (39)
Apr 11, 6-7 PM (0)
Apr 11, 7-8 PM (0)
Apr 11, 8-9 PM (2)
Apr 11, 9-10 PM (1)
Apr 11, 10-11 PM (19)
Apr 11, 11-12 AM (23)
Apr 12, 12-1 AM (4)
Apr 12, 1-2 AM (1)
Apr 12, 2-3 AM (9)
Apr 12, 3-4 AM (2)
Apr 12, 4-5 AM (0)
Apr 12, 5-6 AM (2)
Apr 12, 6-7 AM (2)
Apr 12, 7-8 AM (1)
Apr 12, 8-9 AM (3)
Apr 12, 9-10 AM (2)
Apr 12, 10-11 AM (11)
Apr 12, 11-12 PM (4)
Apr 12, 12-1 PM (1)
Apr 12, 1-2 PM (10)
Apr 12, 2-3 PM (24)
Apr 12, 3-4 PM (7)
Apr 12, 4-5 PM (7)
Apr 12, 5-6 PM (17)
Apr 12, 6-7 PM (2)
Apr 12, 7-8 PM (1)
Apr 12, 8-9 PM (8)
Apr 12, 9-10 PM (9)
Apr 12, 10-11 PM (38)
Apr 12, 11-12 AM (23)
Apr 13, 12-1 AM (5)
Apr 13, 1-2 AM (6)
Apr 13, 2-3 AM (5)
Apr 13, 3-4 AM (6)
Apr 13, 4-5 AM (2)
Apr 13, 5-6 AM (18)
Apr 13, 6-7 AM (23)
Apr 13, 7-8 AM (39)
Apr 13, 8-9 AM (43)
Apr 13, 9-10 AM (51)
Apr 13, 10-11 AM (56)
Apr 13, 11-12 PM (35)
Apr 13, 12-1 PM (55)
Apr 13, 1-2 PM (80)
Apr 13, 2-3 PM (42)
Apr 13, 3-4 PM (20)
Apr 13, 4-5 PM (31)
Apr 13, 5-6 PM (25)
Apr 13, 6-7 PM (17)
Apr 13, 7-8 PM (13)
Apr 13, 8-9 PM (15)
Apr 13, 9-10 PM (22)
Apr 13, 10-11 PM (29)
Apr 13, 11-12 AM (13)
Apr 14, 12-1 AM (6)
Apr 14, 1-2 AM (8)
Apr 14, 2-3 AM (15)
Apr 14, 3-4 AM (4)
Apr 14, 4-5 AM (4)
Apr 14, 5-6 AM (4)
3,575 commits this week Apr 07, 2026 - Apr 14, 2026
fix(pollux): add exp/nbf validation and fix error logging in SDJWT.verify
Fixes #553 — replaced console.log with silent catch in verification
error path, consistent with JWT.verify behavior.

Fixes #554 — added exp and nbf temporal claim validation per
RFC 7519 §4.1.4 and §4.1.5. SDJWT.verify now returns false for
expired or not-yet-valid credentials.

Changes:
- Check exp claim before signature verification; return false if expired
- Check nbf claim before signature verification; return false if too early
- Remove console.log(err) from catch block (was leaking error details)
- Change import from type-only to value import for Domain (needed for
  runtime access to JWT.Claims enum)

Signed-off-by: abhigyan1102 <[email protected]>
Signed-off-by: Abhigyan Singh <[email protected]>
CIP-159-11: Initial PoV property module skeletons (#1123)
Add preservation-of-value property modules for the Dijkstra era,
adapted from the Conway PoV proof structure for CIP-159 (partial
withdrawals and direct deposits).

New modules:
- Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov,
  PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics)
- Certs.Properties.PoV: CERTS-pov top-level theorem
- Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing
  applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls
- Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement
  with proof sketch for direct deposit cancellation

Design notes:
- PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction)
  instead of Conway's constMap/res-decomp/sumConstZero chain
- LEDGER-pov identifies the applyDirectDeposits cancellation as the
  main new proof obligation vs Conway
- applyWithdrawals-pov is structured as three layers: single-step
  (applyOne-pov), fold induction (foldl-applyOne-pov), top-level

Status: Skeleton with holes; does not yet fully typecheck.
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120)
Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (21+h → 22+h)
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120)
Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (21+h → 22+h)
[Dijkstra] CIP-159-07: Use explicit legacy premises instead of allowedLanguagesLegacyMode
Address Carlos's review: `allowedLanguagesLegacyMode` is intended for use
*within* legacy mode to select among V1–V3 versions, not to gate entry
into legacy mode.

`Utxow.lagda.md`:
+  Revert allowedLanguagesLegacyMode to its original form (remove
   UsesV4Features check)
+  Add explicit `Is-∅ (dom txDirectDeposits)` and
   `Is-∅ (dom txBalanceIntervals)` premises to UTXOW-legacy
+  Update `UTXOW-legacy-⋯` pattern synonym for 13 premises
+  Revise documentation to describe the premise-based approach

`Utxow/Properties/Computational.lagda.md`:
+  Update computeProof and completeness for the new legacy tuple arity.
[Dijkstra] CIP-159-07: Version gating for CIP-159 fields (#1119)
Extend `UsesV4Features` to detect CIP-159 transaction fields and update
`allowedLanguagesLegacyMode` to forbid them in legacy mode.

+  Add hasDirectDeposits and hasBalanceIntervals constructors to
   `UsesV4Features`, detecting non-empty
   `txDirectDeposits`/`txBalanceIntervals`.
+  Prepend `UsesV4Features` check to `allowedLanguagesLegacyMode`,
   returning ∅ when V4 features are present (making legacy rule unsatisfiable).
+  Update `Dec-UsesV4Features` instance for the two new constructors.
+  Document the CIP-159/CIP-118 interaction for version gating.

No changes to `Utxow/Properties/Computational.lagda.md`; premise shapes are
unchanged since no new fields are added to `UTXOW-legacy` or `UTXOW-normal`.
[Dijkstra] CIP-159-07: Use explicit legacy premises instead of allowedLanguagesLegacyMode
Address Carlos's review: `allowedLanguagesLegacyMode` is intended for use
*within* legacy mode to select among V1–V3 versions, not to gate entry
into legacy mode.

`Utxow.lagda.md`:
+  Revert allowedLanguagesLegacyMode to its original form (remove
   UsesV4Features check)
+  Add explicit `Is-∅ (dom txDirectDeposits)` and
   `Is-∅ (dom txBalanceIntervals)` premises to UTXOW-legacy
+  Update `UTXOW-legacy-⋯` pattern synonym for 13 premises
+  Revise documentation to describe the premise-based approach

`Utxow/Properties/Computational.lagda.md`:
+  Update computeProof and completeness for the new legacy tuple arity.
[Dijkstra] CIP-159-07: Version gating for CIP-159 fields (#1119)
Extend `UsesV4Features` to detect CIP-159 transaction fields and update
`allowedLanguagesLegacyMode` to forbid them in legacy mode.

+  Add hasDirectDeposits and hasBalanceIntervals constructors to
   `UsesV4Features`, detecting non-empty
   `txDirectDeposits`/`txBalanceIntervals`.
+  Prepend `UsesV4Features` check to `allowedLanguagesLegacyMode`,
   returning ∅ when V4 features are present (making legacy rule unsatisfiable).
+  Update `Dec-UsesV4Features` instance for the two new constructors.
+  Document the CIP-159/CIP-118 interaction for version gating.

No changes to `Utxow/Properties/Computational.lagda.md`; premise shapes are
unchanged since no new fields are added to `UTXOW-legacy` or `UTXOW-normal`.
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
CIP-159 changes the transaction balancing rules and introduces Phase-1
balance interval validation.  This commit updates the UTxO transition
system accordingly.

`Utxo.lagda.md`:
+  Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for
   pre-batch account balance lookups;
+  Add HasAccountBalances type class and instances;
+  Update producedTx to include direct deposit amounts on the produced
   side of the preservation-of-value equation;
+  Add direct deposit registration premise to UTXO and SUBUTXO
   (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`);
+  Add balance interval validation premise to UTXO and SUBUTXO
   (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using
   pre-batch account balances).

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (19+h → 21+h)

`Ledger.lagda.md`:
+  Add accountBalances field to SubLedgerEnv;
+  Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V,
   LEDGER-I using RewardsOf certState₀ (pre-batch balances).
Remove deprecated 'pie' hardening flag for musl builds
nixpkgs 26.05 removed 'pie' from the hardening system entirely -- PIE
is now enabled by default in compilers. Any mention of 'pie' in either
hardeningEnable or hardeningDisable triggers a deprecation warning:

  "The 'pie' hardening flag has been removed in favor of enabling PIE
   by default in compilers and should no longer be used."

This causes ~68 warnings per evaluation for projects with musl
cross-compilation, which is every haskell.nix project using
crossPlatforms with musl64 or aarch64-multiplatform-musl.

Remove the two places where 'pie' was added to hardeningDisable:
- builder/comp-builder.nix: every Haskell component on musl
- compiler/ghc/default.nix: GHC itself on musl targets