PROOF.pk_bits: def of bend-osdev-acpi@0.1.1.0 Import: import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF Lines 54-160 of bend-osdev-acpi@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&start_line=54&end_line=160 import Base import bend-osdev-bytes@0.1.1.0/bytes.bend as B import bend-osdev-acpi@0.1.1.0/error.bend as E import bend-osdev-acpi@0.1.1.0/aml_pkglength.bend as K # the bits from the top down, so that they are matched in binder order def pk_bits(+b31: Bool, +b30: Bool, +b29: Bool, +b28: Bool, +b27: Bool, +b26: Bool, +b25: Bool, +b24: Bool, +b23: Bool, +b22: Bool, +b21: Bool, +b20: Bool, +b19: Bool, +b18: Bool, +b17: Bool, +b16: Bool, +b15: Bool, +b14: Bool, +b13: Bool, +b12: Bool, +b11: Bool, +b10: Bool, +b9: Bool, +b8: Bool, +b7: Bool, +b6: Bool, +b5: Bool, +b4: Bool, +b3: Bool, +b2: Bool, +b1: Bool, +b0: Bool, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})), r))) == Done{K.AmlPkgLen{U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}: match b31: case True{}: pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{True{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits)) case False{}: match b30: case True{}: pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits)) case False{}: match b29: case True{}: pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits)) case False{}: match b28: case True{}: pk_abs(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits)) case False{}: match b27: case True{}: {==} case False{}: match b26: case True{}: {==} case False{}: match b25: case True{}: {==} case False{}: match b24: case True{}: {==} case False{}: match b23: case True{}: {==} case False{}: match b22: case True{}: {==} case False{}: match b21: case True{}: {==} case False{}: match b20: case True{}: {==} case False{}: match b19: case True{}: {==} case False{}: match b18: case True{}: {==} case False{}: match b17: case True{}: {==} case False{}: match b16: case True{}: {==} case False{}: match b15: case True{}: {==} case False{}: match b14: case True{}: {==} case False{}: match b13: case True{}: {==} case False{}: match b12: case True{}: {==} case False{}: match b11: case True{}: {==} case False{}: match b10: case True{}: {==} case False{}: match b9: case True{}: {==} case False{}: match b8: case True{}: {==} case False{}: match b7: case True{}: {==} case False{}: match b6: case True{}: {==} case False{}: {==} Uses (17): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=ft_absurd https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pk_abs https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=AmlPkgLen https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=AmlPkgLength.fits https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=pk.dec https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=pk.enc https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_pkglength.bend&name=pk.pub https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/error.bend&name=AcpiError https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask