Skip to content

Commit 891ed45

Browse files
hyperpolymathhyperpolymath
authored
proof(SafeNetwork): annotate 5 bodyless decls as OWED (Refs standards#158) (#49)
## Summary Applies the estate's OWED-with-justification convention (set 2026-05-20 by SafeChecksum/Buffer/CryptoAccel/HKDF/Bloom/FPGA; live examples in sibling PRs #37 / #41 / #46) to the 5 remaining bodyless declarations in `src/Proven/SafeNetwork/Proofs.idr`. Form per decl: triple-pipe doc stating the claim + the specific Idris2 0.8.0 blocker + a "Discharge once …" condition, followed by `public export` + `0 ` erased-multiplicity bare signature. No `postulate` keyword (consistent with the other Proofs.idr in the repo). No semantic change to the postulated claims; only the annotation form and visibility (`export` -> `public export` + `0 `) change. Refs hyperpolymath/standards#158. ## Per-decl OWED reasons | Decl | Claim | Blocker | Discharge path | |------|-------|---------|----------------| | `mkPortSucceeds` | `LTE n 65535 -> IsJust (mkPort n)` | `mkPort` branches on `checkPort`, which runs the opaque primitive Nat `<=`; the resulting `Bool` does not type-level reduce to the `LTE` premise. | Nat decidability bridge `lteReflectsLTE` in `Data.Nat`, or refactor `mkPort` to consume `LTE` directly. | | `networkInOwnCIDR` | `contains cidr (networkAddress cidr) = True` | `contains` uses `ipToNat ... >= ipToNat ...`; primitive Nat `>=` is opaque when `cidr` is a free variable. | `ipToNat` monotonicity lemmas + a `>=`-to-`GTE` reflective bridge. | | `broadcastInOwnCIDR` | `contains cidr (broadcastAddress cidr) = True` | Same family as above. | Same as above. | | `systemPortBound` | `isSystemPort p = True -> LTE (portValue p) 1023` | `isSystemPort` is a runtime Bool over `classify`; the `True` arm does not type-level reduce to `LTE` (opaque primitive Nat comparison). | Reformulate `classify` to return a dependent witness carrying the `LTE`, or land a primitive-Nat reflective bridge. | | `portBounded` | `LTE (portValue p) 65535` | `Port` is constructed with an erased `IsPort` witness (`data IsPort : Nat -> Type where ItIsPort : IsPort n`) — bound enforced dynamically by `checkPort`/`mkPort`, not constructively. | Refine `IsPort n := LTE n 65535`, or rebuild `Port` to carry the `LTE` proof. | ## Test plan - [ ] Local idris2 0.8.0 type-check the file (environment-blocked in this worktree by a `base` library install mismatch — convention pattern is identical to the already-built sibling files `Proven/SafeChecksum/Proofs.idr`, `Proven/SafeBuffer/Proofs.idr`, `Proven/SafeHKDF/Proofs.idr` etc., which use the same `public export` + `0 ` form on identical claim shapes). - [ ] Draft until CI un-jams estate-wide; do not merge yet. ## Notes - DRAFT because CI is jammed estate-wide. - Touches only `src/Proven/SafeNetwork/Proofs.idr`. - Does not introduce any `postulate` keyword, `believe_me`, or `idris_crash`. The OWED witnesses are erased (`0 `) so they cannot affect runtime semantics. Refs hyperpolymath/standards#158
1 parent b1bdd6b commit 891ed45

1 file changed

Lines changed: 48 additions & 36 deletions

File tree

‎src/Proven/SafeNetwork/Proofs.idr‎

Lines changed: 48 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -28,28 +28,35 @@ public export
2828
portAlwaysValid : (p : Port) -> ValidPort p
2929
portAlwaysValid p = MkValidPort p
3030

31-
-- | mkPort succeeds for values <= 65535.
32-
-- | Postulated: mkPort uses a runtime Bool check (`n <= 65535`), and the
33-
-- | connection between the runtime `<=` and the type-level `LTE` requires
34-
-- | showing that `(n <= 65535) = True` implies `checkPort n = Just ItIsPort`,
35-
-- | which involves the opaque primitive Nat comparison.
36-
-- TODO: Update for Idris2 0.8.0 -- prove via decidability of Nat comparison.
37-
export
38-
mkPortSucceeds : (n : Nat) -> LTE n 65535 -> IsJust (mkPort n)
31+
||| OWED: `mkPort n` returns `Just _` whenever `n <= 65535`. Held back
32+
||| by Idris2 0.8.0 not bridging the runtime `Bool` test
33+
||| `n <= 65535 = True` (used by `checkPort`) to the type-level `LTE n
34+
||| 65535` witness: `mkPort` branches on `checkPort n`, which evaluates
35+
||| the opaque primitive Nat `<=`, so `IsJust (mkPort n)` does not
36+
||| reduce by Refl from an `LTE` premise. Discharge once a Nat
37+
||| decidability bridge (`lteReflectsLTE : (n <= m) = True -> LTE n m`)
38+
||| is exposed by `Data.Nat`, or `mkPort` is refactored to take the
39+
||| `LTE` proof directly.
40+
public export
41+
0 mkPortSucceeds : (n : Nat) -> LTE n 65535 -> IsJust (mkPort n)
3942

40-
-- | Network address is always contained in its own CIDR.
41-
-- | Postulated: `contains` does not reduce on abstract `CIDRBlock` in
42-
-- | Idris 2 0.8.0 because it involves runtime Nat comparisons
43-
-- | (`ipToNat ... >= ipToNat ...`) that are opaque at the type level.
44-
-- TODO: Update for Idris2 0.8.0 -- prove via ipToNat monotonicity lemmas.
45-
export
46-
networkInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (networkAddress cidr) = True
43+
||| OWED: every CIDR block contains its own network address. Held back
44+
||| by Idris2 0.8.0 not reducing `contains` on an abstract `CIDRBlock`:
45+
||| `contains` is defined via `ipToNat ... >= ipToNat ...`, and those
46+
||| primitive Nat `>=` comparisons stay opaque at the type level when
47+
||| the `CIDRBlock` is a free variable rather than a concrete literal.
48+
||| Discharge once `ipToNat` monotonicity lemmas are proven and a
49+
||| reflective bridge from primitive `>=` to `GTE` is available.
50+
public export
51+
0 networkInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (networkAddress cidr) = True
4752

48-
-- | Broadcast address is always contained in its own CIDR.
49-
-- | Postulated for same reason as networkInOwnCIDR.
50-
-- TODO: Update for Idris2 0.8.0 -- prove via ipToNat monotonicity lemmas.
51-
export
52-
broadcastInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (broadcastAddress cidr) = True
53+
||| OWED: every CIDR block contains its own broadcast address. Same
54+
||| blocker family as `networkInOwnCIDR` — `contains` does not reduce
55+
||| on an abstract `CIDRBlock` argument because of opaque primitive
56+
||| Nat `>=`. Discharge once `ipToNat` monotonicity + a `>=`-to-`GTE`
57+
||| reflective bridge are in place.
58+
public export
59+
0 broadcastInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (broadcastAddress cidr) = True
5360

5461
||| CIDR subset transitivity: if A is a subset of B and B is a subset of C then A is a subset of C
5562
||| This follows from the transitivity of the containment relation
@@ -59,23 +66,28 @@ data SubsetTransitive : CIDRBlock -> CIDRBlock -> CIDRBlock -> Type where
5966
isSubsetOf b c = True ->
6067
SubsetTransitive a b c
6168

62-
-- | System ports are always < 1024.
63-
-- | Postulated: requires connecting the runtime Bool classification
64-
-- | (`isSystemPort`) with the type-level `LTE` relation, which involves
65-
-- | the opaque Nat comparison primitives.
66-
-- TODO: Update for Idris2 0.8.0 -- prove via decidability of Nat comparison.
67-
export
68-
systemPortBound : (p : Port) -> isSystemPort p = True -> LTE (portValue p) 1023
69+
||| OWED: a port classified as a system port has value `<= 1023`.
70+
||| Held back by Idris2 0.8.0's Bool-to-LTE bridge: `isSystemPort` is a
71+
||| runtime classification that pattern-matches on the result of
72+
||| `classify`, and the `True` outcome does not type-level reduce to a
73+
||| `LTE` witness without an opaque primitive Nat comparison.
74+
||| Discharge once `classify` is reformulated to return a dependent
75+
||| witness (e.g. `(c : Class ** ClassifiedAs p c)`) carrying the
76+
||| `LTE` proof, or once a primitive-Nat reflective bridge lands.
77+
public export
78+
0 systemPortBound : (p : Port) -> isSystemPort p = True -> LTE (portValue p) 1023
6979

70-
-- | Every port value is <= 65535.
71-
-- | Postulated: Port construction now uses a runtime bounds check via
72-
-- | `checkPort` with an erased `IsPort` witness, rather than a
73-
-- | constructive `LTE n 65535` proof. The bound holds by the runtime
74-
-- | check in mkPort/unsafeMkPort.
75-
-- TODO: Update for Idris2 0.8.0 -- either restore LTE proof with
76-
-- efficient representation, or prove from IsPort witness semantics.
77-
export
78-
portBounded : (p : Port) -> LTE (portValue p) 65535
80+
||| OWED: every well-typed `Port` has `portValue p <= 65535`. Held
81+
||| back by the move to runtime bounds checking: `mkPort` / `unsafeMkPort`
82+
||| now carry an erased `IsPort` witness (`data IsPort : Nat -> Type
83+
||| where ItIsPort : IsPort n`) rather than a constructive `LTE n
84+
||| 65535` proof, so the bound is enforced dynamically by `checkPort`
85+
||| but not recoverable at the type level by Refl. Discharge once
86+
||| `IsPort` is refined to a non-trivial witness carrying the `LTE`
87+
||| (i.e. `IsPort n := LTE n 65535`), or `Port` is rebuilt to store
88+
||| the `LTE` proof directly.
89+
public export
90+
0 portBounded : (p : Port) -> LTE (portValue p) 65535
7991

8092
||| Proof that host count is positive for prefix < 32
8193
public export

0 commit comments

Comments
 (0)