From cb3ff5d1a5cc14d74f1efb1a367db2244acfbd15 Mon Sep 17 00:00:00 2001
From: EpsilonPhoenix <129551402+EpsilonPhoenix@users.noreply.github.com>
Date: Sat, 31 Oct 2026 04:34:14 +0000
Subject: [PATCH] tcpip: verify UDP checksums within the declared datagram
 length

---
 tcpip/PROOF_packet.bend | 60 +++++++++++++++++++++++++++-
 tcpip/README.md         | 18 ++++++++-
 tcpip/VERSION           |  2 +-
 tcpip/ref/.gitignore    |  2 +
 tcpip/ref/gen_packet.py | 86 ++++++++++++++++++++++++++++++++---------
 tcpip/ref/gen_udp.py    | 78 +++++++++++++++++++++++++++++++++++++
 tcpip/ref/run.sh        |  7 ++++
 tcpip/udp.bend          | 23 +++++++++--
 8 files changed, 250 insertions(+), 26 deletions(-)
 create mode 100644 tcpip/ref/gen_udp.py

diff --git a/tcpip/PROOF_packet.bend b/tcpip/PROOF_packet.bend
index 45be64d..dd3665a 100644
--- a/tcpip/PROOF_packet.bend
+++ b/tcpip/PROOF_packet.bend
@@ -179,14 +179,70 @@ def tp.reply_rep(st: IC.IcmpState, +src: U32, +dst: U32, +id: U32, +seq: U32, +d
 def Laws.icmp_reply_packet_reported(st, src, dst, id, seq, data):
   tp.reply_rep(st, src, dst, id, seq, data)
 
-# UDP: a datagram's bytes received
+# UDP: validate and trim before checksum verification. Equalities are affine;
+# transport the pair of reflexive proofs once to obtain two length witnesses.
+def tp.nat_eq_twice(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {a == b : Nat} & {a == b : Nat}:
+  %e : {a == _ : Nat} & {a == _ : Nat}
+  ({==}, {==})
+
+def tp.udp_list(a: U32, b: U32, l: U32, k: U32) -> List<&2, U32>:
+  B.append(B.be16(a), B.append(B.be16(b), B.append(B.be16(l), B.be16(k))))
+
+def tp.udp_blen(a: U32, b: U32, l: U32, k: U32) -> {B.len(tp.udp_list(a, b, l, k)) == 8n : Nat}:
+  match a b l k:
+    case U32{a_} U32{b_} U32{l_} U32{k_}:
+      {==}
 
-def Laws.udp_packet_received(st, src, dst, sport, dport, length, checksum, data, hl):
+def tp.udp_hlen(+a: U32, +b: U32, +l: U32, +k: U32) -> {B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{a, b, l, k})) == 8n : Nat}:
+  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(tp.udp_list(a, b, l, k))), B.len(tp.udp_list(a, b, l, k)), BL.octets_len_of_list(tp.udp_list(a, b, l, k))) : {_ == 8n : Nat}
+  tp.udp_blen(a, b, l, k)
+
+def tp.ge8(n: Nat) -> {Nat.is_ge(Nat.add(8n, n), 8n) == True{} : Bool}:
+  match n:
+    case 0n: {==}
+    case 1n+p: {==}
+
+def tp.le8(n: Nat) -> {Nat.is_le(8n, Nat.add(8n, n)) == True{} : Bool}:
+  match n:
+    case 0n: {==}
+    case 1n+p: {==}
+
+def tp.udp_bound(+sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets) -> {Nat.is_le(8n, B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data))) == True{} : Bool}:
+  %Equal.sym(Nat, B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)), Nat.add(B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), B.Octets.len(data)), BL.octets_len_append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)) : {Nat.is_le(8n, _) == True{} : Bool}
+  %Equal.sym(Nat, B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), 8n, tp.udp_hlen(sport, dport, length, checksum)) : {Nat.is_le(8n, Nat.add(_, B.Octets.len(data))) == True{} : Bool}
+  tp.le8(B.Octets.len(data))
+
+def tp.udp_len(+sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets, +c: U32) -> {B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, c)) == Nat.add(8n, B.Octets.len(data)) : Nat}:
+  %Equal.sym(Nat, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, c)), B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)), NS.inet_put16_len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, c, tp.udp_bound(sport, dport, length, checksum, data))) : {_ == Nat.add(8n, B.Octets.len(data)) : Nat}
+  %Equal.sym(Nat, B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)), Nat.add(B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), B.Octets.len(data)), BL.octets_len_append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)) : {_ == Nat.add(8n, B.Octets.len(data)) : Nat}
+  %Equal.sym(Nat, B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), 8n, tp.udp_hlen(sport, dport, length, checksum)) : {Nat.add(_, B.Octets.len(data)) == Nat.add(8n, B.Octets.len(data)) : Nat}
+  {==}
+
+def tp.udp_old(+st: U.UdpState, +src: U32, +dst: U32, +sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets, hl: {U32.to_nat(N.NetField.low(16n, length)) == Nat.add(8n, B.Octets.len(data)) : Nat}) -> {U.Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)), st, src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}:
   %Equal.sym(Bool, NU.UdpHeader.verify_ipv4(src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)), True{}, NS.udp_ipv4_build_verifies(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) : {U.Udp.recv.go(_, st, src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
   %Equal.sym(B.Octets, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), NS.udp_ipv4_build_fill(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) : {U.Udp.recv.go(True{}, st, src, dst, _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
   %Equal.sym(Result<&2, &2, N.NetError, NU.UdpHeader>, NU.UdpHeader.parse(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Done{NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))})}, NS.udp_put_parse(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) : {U.Udp.recv.header(_, st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
   %Equal.sym(Result<&2, &2, N.NetError, B.Octets>, NU.UdpHeader.payload(NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))}), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Done{data}, NS.udp_put_payload(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))), hl)) : {U.Udp.recv.payload(_, st, src, dst, NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))})) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
   {==}
 
+
+def tp.udp_received(+st: U.UdpState, +src: U32, +dst: U32, +sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets, hs: {U32.to_nat(N.NetField.low(16n, length)) == Nat.add(8n, B.Octets.len(data)) : Nat} & {U32.to_nat(N.NetField.low(16n, length)) == Nat.add(8n, B.Octets.len(data)) : Nat}) -> {Pair.snd(U.UdpState, List<&2, U.UdpAction>, U.Udp.recv(st, src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}:
+  match hs:
+    case (ha, hb):
+      %Equal.sym(B.Octets, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), NS.udp_ipv4_build_fill(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) : {Pair.snd(U.UdpState, List<&2, U.UdpAction>, U.Udp.recv(st, src, dst, _)) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Result<&2, &2, N.NetError, NU.UdpHeader>, NU.UdpHeader.parse(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Done{NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))})}, NS.udp_put_parse(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) : {U.Udp.recv.trim_header(_, st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Nat, U32.to_nat(N.NetField.low(16n, length)), Nat.add(8n, B.Octets.len(data)), ha) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(_, 8n), Nat.is_le(_, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))))), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %tp.udp_len(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(_, 8n), Nat.is_le(_, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))))), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Bool, Nat.is_le(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))), True{}, UL.nat_le_refl(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))))) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), 8n), _), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Nat, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Nat.add(8n, B.Octets.len(data)), tp.udp_len(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(_, 8n), True{}), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Bool, Nat.is_ge(Nat.add(8n, B.Octets.len(data)), 8n), True{}, tp.ge8(B.Octets.len(data))) : {U.Udp.recv.trim_length(Bool.and(_, True{}), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), BL.octets_take_len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) : {U.Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, _), st, src, dst, _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %NS.udp_ipv4_build_fill(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data) : {U.Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, _), st, src, dst, _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      tp.udp_old(st, src, dst, sport, dport, length, checksum, data, hb)
+
+
+def Laws.udp_packet_received(st, src, dst, sport, dport, length, checksum, data, hl):
+  tp.udp_received(st, src, dst, sport, dport, length, checksum, data, tp.nat_eq_twice(U32.to_nat(N.NetField.low(16n, length)), Nat.add(8n, B.Octets.len(data)), hl))
+
 def Laws.udp_packet_received_sat():
   {==}
diff --git a/tcpip/README.md b/tcpip/README.md
index ea06c1a..e0a07b1 100644
--- a/tcpip/README.md
+++ b/tcpip/README.md
@@ -35,7 +35,8 @@ bend-osdev-netheaders; byte strings are bend-osdev-bytes' `Octets`.
   default ISN function; see Extension points);
 * RFC 791, Internet Protocol (version 4), with fragmentation and reassembly;
 * RFC 792, Internet Control Message Protocol;
-* RFC 768, User Datagram Protocol;
+* RFC 768, User Datagram Protocol; [RFC 9868](https://www.rfc-editor.org/rfc/rfc9868.html)
+  sections 7–9 for the surplus area outside the UDP length and checksum;
 * RFC 826, An Ethernet Address Resolution Protocol (the packet reception
   algorithm);
 * RFC 1122, Requirements for Internet Hosts: Communication Layers (ARP cache
@@ -293,6 +294,14 @@ bend-osdev-bytes' laws of take, drop and append on Octets.
 
 ## Tests
 
+`ref/gen_udp.py` independently constructs UDP wire bytes and checksums using
+Python `struct`. Its receive regressions cover odd/even and empty payloads,
+surplus bytes, corruption inside the datagram, absent checksums, truncated
+headers/data, and invalid lengths. `ref/run.sh` runs these alongside the TCP
+model tests. The receiver validates length before checking only the declared
+UDP datagram; surplus bytes are ignored, without processing UDP options.
+
+
 * `check.bend`: five TCP walk-throughs through `sim.bend` (the three-way
   handshake, data both ways and both closes with TIME-WAIT; a segment lost
   three times, with the RTO doubling from 1 s to 2 s to 4 s; segments out of
@@ -343,6 +352,13 @@ values (`LAWS.bend`) and the order of `Nat` and words (`LAWS_order.bend`).
 
 ## Status
 
+2026-10-31: Bend 2.0.39 / Lean 4.34.0: `scripts/check.sh tcpip` and
+`VERDICT=1 scripts/check.sh tcpip` pass (all three proof files, runtime
+examples, 100 TCP model cases / 6671 trace lines, and 86 UDP cases).
+`scripts/deps.sh tcpip`, the public-interface audit, and the packet proof
+generator's `--check` pass. Linux TAP integration is skipped on this VM
+(no usable namespace/TAP setup).
+
 Bend 2.0.39 (2026-10-26, native, three packages at a time): `PROOF.bend`
 (2 s, 0.35 GB peak; `--verdict` 5 s, 0.41 GB peak), `PROOF_packet.bend`
 (3 s, 0.35 GB peak; `--verdict` 5 s, 0.40 GB peak) and `PROOF_stream.bend`
diff --git a/tcpip/VERSION b/tcpip/VERSION
index 482e997..4180912 100644
--- a/tcpip/VERSION
+++ b/tcpip/VERSION
@@ -1 +1 @@
-0.1.0.0
+0.1.0.1
diff --git a/tcpip/ref/.gitignore b/tcpip/ref/.gitignore
index 53af1f2..7e7914a 100644
--- a/tcpip/ref/.gitignore
+++ b/tcpip/ref/.gitignore
@@ -1,3 +1,5 @@
 cases.bend
 expected.txt
 __pycache__/
+udp_cases.bend
+udp_expected.txt
diff --git a/tcpip/ref/gen_packet.py b/tcpip/ref/gen_packet.py
index e2268af..01269d5 100644
--- a/tcpip/ref/gen_packet.py
+++ b/tcpip/ref/gen_packet.py
@@ -156,24 +156,15 @@ def tp.rest_mask(+id: U32, +seq: U32) -> {{IC.Icmp.rest(U32.and(id, 65535), U32.
 
 # Lengths of ICMP headers
 
-def tp.icmp_blen(h: NI.IcmpHeader) -> {{B.len(NI.IcmpHeader.build.list(h)) == 8n : Nat}}:
-  match h:
-    case NI.IcmpHeader{{U32{{a}}, U32{{b}}, U32{{c}}, U32{{d}}}}:
-      {{==}}
-
-def tp.icmp_len_build(+h: NI.IcmpHeader) -> {{B.Octets.len(NI.IcmpHeader.build(h)) == 8n : Nat}}:
-  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(NI.IcmpHeader.build.list(h))), B.len(NI.IcmpHeader.build.list(h)), BL.octets_len_of_list(NI.IcmpHeader.build.list(h))) : {{_ == 8n : Nat}}
-  tp.icmp_blen(h)
-
 def tp.icmp_mlen(+h: NI.IcmpHeader, +data: B.Octets) -> {{Nat.is_le(Nat.add(2n, 2n), B.Octets.len(B.Octets.append(NI.IcmpHeader.build(h), data))) == True{{}} : Bool}}:
   %Equal.sym(Nat, B.Octets.len(B.Octets.append(NI.IcmpHeader.build(h), data)), Nat.add(B.Octets.len(NI.IcmpHeader.build(h)), B.Octets.len(data)), BL.octets_len_append(NI.IcmpHeader.build(h), data)) : {{Nat.is_le(Nat.add(2n, 2n), _) == True{{}} : Bool}}
-  %Equal.sym(Nat, B.Octets.len(NI.IcmpHeader.build(h)), 8n, tp.icmp_len_build(h)) : {{Nat.is_le(Nat.add(2n, 2n), Nat.add(_, B.Octets.len(data))) == True{{}} : Bool}}
+  %Equal.sym(Nat, B.Octets.len(NI.IcmpHeader.build(h)), 8n, NS.icmp_build_length(h)) : {{Nat.is_le(Nat.add(2n, 2n), Nat.add(_, B.Octets.len(data))) == True{{}} : Bool}}
   {{==}}
 
 # the data past the 8-byte header, whatever checksum was written
 def tp.icmp_drop8(+h: NI.IcmpHeader, +data: B.Octets, +c: U32) -> {{B.Octets.drop(8n, K.inet_put16(B.Octets.append(NI.IcmpHeader.build(h), data), 2n, c)) == data : B.Octets}}:
   %Equal.sym(B.Octets, B.Octets.drop(8n, K.inet_put16(B.Octets.append(NI.IcmpHeader.build(h), data), 2n, c)), B.Octets.drop(8n, B.Octets.append(NI.IcmpHeader.build(h), data)), NS.inet_put16_drop(B.Octets.append(NI.IcmpHeader.build(h), data), 2n, c, 8n, {{==}}, tp.icmp_mlen(h, data))) : {{_ == data : B.Octets}}
-  %tp.icmp_len_build(h) : {{B.Octets.drop(_, B.Octets.append(NI.IcmpHeader.build(h), data)) == data : B.Octets}}
+  %NS.icmp_build_length(h) : {{B.Octets.drop(_, B.Octets.append(NI.IcmpHeader.build(h), data)) == data : B.Octets}}
   BL.octets_drop_append(NI.IcmpHeader.build(h), data)
 """)
 
@@ -222,23 +213,80 @@ def Laws.icmp_reply_packet_reported(st, src, dst, id, seq, data):
 
 H = "NU.UdpHeader{sport, dport, length, checksum}"
 DG0 = f"B.Octets.append(NU.UdpHeader.build({H}), data)"
-PS = f"I4.ipv4_pseudo(src, dst, 17, N.net.len32({DG0}))"
+PS = f"I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len({DG0})))"
 NZ = f"NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append({PS}, K.inet_put16({DG0}, 6n, 0))))"
 BUILT = f"NU.UdpHeader.build_ipv4(src, dst, {H}, data)"
 HN = f"NU.UdpHeader.norm(NU.UdpHeader{{sport, dport, length, {NZ}}})"
 RHS = "U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data)"
 UL_ = "List<&2, U.UdpAction>"
-w(f"""
-# UDP: a datagram's bytes received
+w("""
+# UDP: validate and trim before checksum verification. Equalities are affine;
+# transport the pair of reflexive proofs once to obtain two length witnesses.
+def tp.nat_eq_twice(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {a == b : Nat} & {a == b : Nat}:
+  %e : {a == _ : Nat} & {a == _ : Nat}
+  ({==}, {==})
+
+def tp.udp_list(a: U32, b: U32, l: U32, k: U32) -> List<&2, U32>:
+  B.append(B.be16(a), B.append(B.be16(b), B.append(B.be16(l), B.be16(k))))
+
+def tp.udp_blen(a: U32, b: U32, l: U32, k: U32) -> {B.len(tp.udp_list(a, b, l, k)) == 8n : Nat}:
+  match a b l k:
+    case U32{a_} U32{b_} U32{l_} U32{k_}:
+      {==}
+
+def tp.udp_hlen(+a: U32, +b: U32, +l: U32, +k: U32) -> {B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{a, b, l, k})) == 8n : Nat}:
+  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(tp.udp_list(a, b, l, k))), B.len(tp.udp_list(a, b, l, k)), BL.octets_len_of_list(tp.udp_list(a, b, l, k))) : {_ == 8n : Nat}
+  tp.udp_blen(a, b, l, k)
+
+def tp.ge8(n: Nat) -> {Nat.is_ge(Nat.add(8n, n), 8n) == True{} : Bool}:
+  match n:
+    case 0n: {==}
+    case 1n+p: {==}
+
+def tp.le8(n: Nat) -> {Nat.is_le(8n, Nat.add(8n, n)) == True{} : Bool}:
+  match n:
+    case 0n: {==}
+    case 1n+p: {==}
+
+def tp.udp_bound(+sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets) -> {Nat.is_le(8n, B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data))) == True{} : Bool}:
+  %Equal.sym(Nat, B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)), Nat.add(B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), B.Octets.len(data)), BL.octets_len_append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)) : {Nat.is_le(8n, _) == True{} : Bool}
+  %Equal.sym(Nat, B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), 8n, tp.udp_hlen(sport, dport, length, checksum)) : {Nat.is_le(8n, Nat.add(_, B.Octets.len(data))) == True{} : Bool}
+  tp.le8(B.Octets.len(data))
+
+def tp.udp_len(+sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets, +c: U32) -> {B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, c)) == Nat.add(8n, B.Octets.len(data)) : Nat}:
+  %Equal.sym(Nat, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, c)), B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)), NS.inet_put16_len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, c, tp.udp_bound(sport, dport, length, checksum, data))) : {_ == Nat.add(8n, B.Octets.len(data)) : Nat}
+  %Equal.sym(Nat, B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)), Nat.add(B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), B.Octets.len(data)), BL.octets_len_append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)) : {_ == Nat.add(8n, B.Octets.len(data)) : Nat}
+  %Equal.sym(Nat, B.Octets.len(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum})), 8n, tp.udp_hlen(sport, dport, length, checksum)) : {Nat.add(_, B.Octets.len(data)) == Nat.add(8n, B.Octets.len(data)) : Nat}
+  {==}
+
+def tp.udp_old(+st: U.UdpState, +src: U32, +dst: U32, +sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets, hl: {U32.to_nat(N.NetField.low(16n, length)) == Nat.add(8n, B.Octets.len(data)) : Nat}) -> {U.Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)), st, src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}:
+  %Equal.sym(Bool, NU.UdpHeader.verify_ipv4(src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)), True{}, NS.udp_ipv4_build_verifies(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) : {U.Udp.recv.go(_, st, src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+  %Equal.sym(B.Octets, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), NS.udp_ipv4_build_fill(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) : {U.Udp.recv.go(True{}, st, src, dst, _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+  %Equal.sym(Result<&2, &2, N.NetError, NU.UdpHeader>, NU.UdpHeader.parse(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Done{NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))})}, NS.udp_put_parse(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) : {U.Udp.recv.header(_, st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+  %Equal.sym(Result<&2, &2, N.NetError, B.Octets>, NU.UdpHeader.payload(NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))}), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Done{data}, NS.udp_put_payload(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))), hl)) : {U.Udp.recv.payload(_, st, src, dst, NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))})) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+  {==}
+
+
+def tp.udp_received(+st: U.UdpState, +src: U32, +dst: U32, +sport: U32, +dport: U32, +length: U32, +checksum: U32, +data: B.Octets, hs: {U32.to_nat(N.NetField.low(16n, length)) == Nat.add(8n, B.Octets.len(data)) : Nat} & {U32.to_nat(N.NetField.low(16n, length)) == Nat.add(8n, B.Octets.len(data)) : Nat}) -> {Pair.snd(U.UdpState, List<&2, U.UdpAction>, U.Udp.recv(st, src, dst, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}:
+  match hs:
+    case (ha, hb):
+      %Equal.sym(B.Octets, NU.UdpHeader.build_ipv4(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), NS.udp_ipv4_build_fill(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data)) : {Pair.snd(U.UdpState, List<&2, U.UdpAction>, U.Udp.recv(st, src, dst, _)) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Result<&2, &2, N.NetError, NU.UdpHeader>, NU.UdpHeader.parse(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Done{NU.UdpHeader.norm(NU.UdpHeader{sport, dport, length, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))})}, NS.udp_put_parse(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) : {U.Udp.recv.trim_header(_, st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Nat, U32.to_nat(N.NetField.low(16n, length)), Nat.add(8n, B.Octets.len(data)), ha) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(_, 8n), Nat.is_le(_, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))))), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %tp.udp_len(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(_, 8n), Nat.is_le(_, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))))), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Bool, Nat.is_le(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))), True{}, UL.nat_le_refl(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))))) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), 8n), _), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Nat, B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), Nat.add(8n, B.Octets.len(data)), tp.udp_len(sport, dport, length, checksum, data, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))) : {U.Udp.recv.trim_length(Bool.and(Nat.is_ge(_, 8n), True{}), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(Bool, Nat.is_ge(Nat.add(8n, B.Octets.len(data)), 8n), True{}, tp.ge8(B.Octets.len(data))) : {U.Udp.recv.trim_length(Bool.and(_, True{}), st, src, dst, K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0)))))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))), BL.octets_take_len(K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, NU.UdpHeader.nonzero(K.inet_checksum(B.Octets.append(I4.ipv4_pseudo(src, dst, 17, U32.from_nat(B.Octets.len(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data)))), K.inet_put16(B.Octets.append(NU.UdpHeader.build(NU.UdpHeader{sport, dport, length, checksum}), data), 6n, 0))))))) : {U.Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, _), st, src, dst, _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      %NS.udp_ipv4_build_fill(src, dst, NU.UdpHeader{sport, dport, length, checksum}, data) : {U.Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, _), st, src, dst, _) == U.Udp.receive(st, src, dst, N.NetField.low(16n, sport), N.NetField.low(16n, dport), data) : List<&2, U.UdpAction>}
+      tp.udp_old(st, src, dst, sport, dport, length, checksum, data, hb)
+
 
 def Laws.udp_packet_received(st, src, dst, sport, dport, length, checksum, data, hl):
-  %Equal.sym(Bool, NU.UdpHeader.verify_ipv4(src, dst, {BUILT}), True{{}}, NS.udp_ipv4_build_verifies(src, dst, {H}, data)) : {{U.Udp.recv.go(_, st, src, dst, {BUILT}) == {RHS} : {UL_}}}
-  %Equal.sym(Result<&2, &2, N.NetError, NU.UdpHeader>, NU.UdpHeader.parse(K.inet_put16({DG0}, 6n, {NZ})), Done{{{HN}}}, NS.udp_put_parse(sport, dport, length, checksum, data, {NZ})) : {{U.Udp.recv.header(_, st, src, dst, {BUILT}) == {RHS} : {UL_}}}
-  %Equal.sym(Result<&2, &2, N.NetError, B.Octets>, NU.UdpHeader.payload({HN}, K.inet_put16({DG0}, 6n, {NZ})), Done{{data}}, NS.udp_put_payload(sport, dport, length, checksum, data, {NZ}, hl)) : {{U.Udp.recv.payload(_, st, src, dst, {HN}) == {RHS} : {UL_}}}
-  {{==}}
+  tp.udp_received(st, src, dst, sport, dport, length, checksum, data, tp.nat_eq_twice(U32.to_nat(N.NetField.low(16n, length)), Nat.add(8n, B.Octets.len(data)), hl))
 
 def Laws.udp_packet_received_sat():
-  {{==}}
+  {==}
 """)
 
 out = "".join(P).rstrip() + chr(10)
diff --git a/tcpip/ref/gen_udp.py b/tcpip/ref/gen_udp.py
new file mode 100644
index 0000000..151732c
--- /dev/null
+++ b/tcpip/ref/gen_udp.py
@@ -0,0 +1,78 @@
+#!/usr/bin/env python3
+"""UDP receive vectors from Python's struct and RFC 768 Internet checksum.
+
+Generate wire bytes independently of netheaders, including surplus area bytes
+(RFC 9868 sections 7-9), corruption, absent checksums and invalid lengths.
+"""
+from pathlib import Path
+import struct
+
+
+def checksum(data):
+    data += b"\0" * (len(data) % 2)
+    total = sum(struct.unpack("!%dH" % (len(data) // 2), data))
+    while total >> 16:
+        total = (total & 65535) + (total >> 16)
+    return (~total) & 65535
+
+
+def datagram(payload, length=None, zero=False):
+    length = 8 + len(payload) if length is None else length
+    wire = struct.pack("!HHHH", 1234, 53, length, 0) + payload
+    if not zero:
+        pseudo = struct.pack("!IIBBH", 1, 2, 0, 17, len(wire))
+        ck = checksum(pseudo + wire) or 65535
+        wire = wire[:6] + struct.pack("!H", ck) + wire[8:]
+    return wire
+
+
+def octets(data):
+    return "B.Octets.of_list([%s])" % ", ".join(map(str, data))
+
+
+cases = []
+for size in range(6):
+    payload = bytes(range(65, 65 + size))
+    for surplus in (b"", b"\1", b"\1\2", b"\0\0\xff"):
+        for zero in (False, True):
+            wire = datagram(payload, zero=zero) + surplus
+            cases.append((wire, payload))
+            if not zero:
+                bad = bytearray(wire)
+                bad[8 if payload else 0] ^= 1
+                cases.append((bytes(bad), None))
+# Invalid lengths must fail even with an absent checksum.
+for length in (0, 1, 7, 12, 65535):
+    cases.append((datagram(b"hi!", length, zero=True), None))
+# A truncated header, and a checksum-bearing truncated datagram.
+for size in range(8):
+    cases.append((datagram(b"hi!")[:size], None))
+cases.append((datagram(b"hi!")[:-1], None))
+
+source = """import Base
+import ../../bytes/bytes.bend as B
+import ../udp.bend as U
+
+def matches(actions: List<&2, U.UdpAction>, want: Maybe<&2, B.Octets>) -> Bool:
+  match actions want:
+    case Nil{} None{}:
+      True{}
+    case Con{U.UdpDeliver{tag, src, sport, dport, data}, Nil{}} Some{expected}:
+      Bool.and(U32.is_eq(tag, 9), Bool.and(U32.is_eq(src, 1), Bool.and(U32.is_eq(sport, 1234), Bool.and(U32.is_eq(dport, 53), B.Octets.is_eq(data, expected)))))
+    case _ _:
+      False{}
+
+def received(wire: B.Octets) -> List<&2, U.UdpAction>:
+  st = Pair.fst(U.UdpState, List<&2, U.UdpAction>, U.Udp.bind(U.UdpState.new(2), 53, 9))
+  Pair.snd(U.UdpState, List<&2, U.UdpAction>, U.Udp.recv(st, 1, 2, wire))
+
+def main() -> IO(Unit):
+  do IO<Unit>:
+"""
+for wire, payload in cases:
+    want = "None{}" if payload is None else "Some{%s}" % octets(payload)
+    source += "    IO.print(Bool.show(matches(received(%s), %s)))\n" % (octets(wire), want)
+root = Path(__file__).resolve().parent
+(root / "udp_cases.bend").write_text(source)
+(root / "udp_expected.txt").write_text("True\n" * len(cases))
+print(len(cases))
diff --git a/tcpip/ref/run.sh b/tcpip/ref/run.sh
index e64aa89..76ac676 100644
--- a/tcpip/ref/run.sh
+++ b/tcpip/ref/run.sh
@@ -18,6 +18,13 @@ if [ "$got" != "$(cat expected.txt)" ]; then
   exit 1
 fi
 model="model: $n match"
+u=$(python3 gen_udp.py) || exit 1
+got=$("${bend[@]}" udp_cases.bend 2>&1)
+if [ "$got" != "$(cat udp_expected.txt)" ]; then
+  diff <(cat udp_expected.txt) <(printf '%s\n' "$got") | head -20
+  exit 1
+fi
+model="$model; UDP: $u match"
 if unshare -rn true 2> /dev/null && [ -c /dev/net/tun ] && command -v ip > /dev/null && command -v ping > /dev/null; then
   tmp=$(mktemp -d)
   trap 'rm -rf "$tmp"' EXIT
diff --git a/tcpip/udp.bend b/tcpip/udp.bend
index 830dd47..e37544f 100644
--- a/tcpip/udp.bend
+++ b/tcpip/udp.bend
@@ -113,10 +113,27 @@ def Udp.recv.go(ok: Bool, +st: UdpState, +src: U32, +dst: U32, +dg: B.Octets) ->
     case True{}:
       Udp.recv.header(NU.UdpHeader.parse(dg), st, src, dst, dg)
 
-# a datagram arrives: its checksum must verify (or be zero) and its length
-# field fit
+def Udp.recv.trim_length(ok: Bool, +st: UdpState, +src: U32, +dst: U32, +dg: B.Octets, n: Nat) -> List<&2, UdpAction>:
+  match ok:
+    case False{}:
+      Nil{}
+    case True{}:
+      +trimmed = B.Octets.take(n, dg)
+      Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, trimmed), st, src, dst, trimmed)
+
+def Udp.recv.trim_header(r: Result<&2, &2, N.NetError, NU.UdpHeader>, +st: UdpState, +src: U32, +dst: U32, +dg: B.Octets) -> List<&2, UdpAction>:
+  match r:
+    case Fail{e}:
+      Nil{}
+    case Done{NU.UdpHeader{sp, dp, len, ck}}:
+      +n = U32.to_nat(len)
+      Udp.recv.trim_length(Bool.and(Nat.is_ge(n, 8n), Nat.is_le(n, B.Octets.len(dg))), st, src, dst, dg, n)
+
+# RFC 768: the checksum covers only the declared UDP length. The IPv4
+# payload may contain a surplus area (RFC 9868 sections 7-9); validate the
+# length before trimming, so take cannot hide a truncated datagram.
 def Udp.recv(+st: UdpState, +src: U32, +dst: U32, +dg: B.Octets) -> Pair(UdpState, List<&2, UdpAction>):
-  (st, Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, dg), st, src, dst, dg))
+  (st, Udp.recv.trim_header(NU.UdpHeader.parse(dg), st, src, dst, dg))
 
 # Sending: the header, with its checksum over the pseudo-header from our
 # address to dst; at most 65507 bytes of data fit an IPv4 packet