def le32_len

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2286

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL

2286def le32_len(+v: U32) -> {B.Octets.len(B.Octets.le32(v)) == 4n : Nat}:
2287  match v:
2288    case U32{w}:
2289      %Equal.sym(Nat, B.Octets.len(B.Octets.le32(U32{w})), B.len(B.Octets.to_list(B.Octets.le32(U32{w}))), BL.octets_len_list(B.Octets.le32(U32{w}))) : {_ == 4n : Nat}
2290      %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(B.le32(U32{w}))), B.mask(B.le32(U32{w})), BL.octets_to_of(B.le32(U32{w}))) : {B.len(_) == 4n : Nat}
2291      {==}