def pk.u8.c4
import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
641# the values 128 to 159
642def pk.u8.c4(r: Nat) -> {Nat.is_le(128n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(128n+r))) == 128n+r : Nat}:
643 match r:
644 case 0n:
645 h => {==}
646 case 1n+r1:
647 match r1:
648 case 0n:
649 h => {==}
650 case 1n+r2:
651 match r2:
652 case 0n:
653 h => {==}
654 case 1n+r3:
655 match r3:
656 case 0n:
657 h => {==}
658 case 1n+r4:
659 match r4:
660 case 0n:
661 h => {==}
662 case 1n+r5:
663 match r5:
664 case 0n:
665 h => {==}
666 case 1n+r6:
667 match r6:
668 case 0n:
669 h => {==}
670 case 1n+r7:
671 match r7:
672 case 0n:
673 h => {==}
674 case 1n+r8:
675 match r8:
676 case 0n:
677 h => {==}
678 case 1n+r9:
679 match r9:
680 case 0n:
681 h => {==}
682 case 1n+r10:
683 match r10:
684 case 0n:
685 h => {==}
686 case 1n+r11:
687 match r11:
688 case 0n:
689 h => {==}
690 case 1n+r12:
691 match r12:
692 case 0n:
693 h => {==}
694 case 1n+r13:
695 match r13:
696 case 0n:
697 h => {==}
698 case 1n+r14:
699 match r14:
700 case 0n:
701 h => {==}
702 case 1n+r15:
703 match r15:
704 case 0n:
705 h => {==}
706 case 1n+r16:
707 match r16:
708 case 0n:
709 h => {==}
710 case 1n+r17:
711 match r17:
712 case 0n:
713 h => {==}
714 case 1n+r18:
715 match r18:
716 case 0n:
717 h => {==}
718 case 1n+r19:
719 match r19:
720 case 0n:
721 h => {==}
722 case 1n+r20:
723 match r20:
724 case 0n:
725 h => {==}
726 case 1n+r21:
727 match r21:
728 case 0n:
729 h => {==}
730 case 1n+r22:
731 match r22:
732 case 0n:
733 h => {==}
734 case 1n+r23:
735 match r23:
736 case 0n:
737 h => {==}
738 case 1n+r24:
739 match r24:
740 case 0n:
741 h => {==}
742 case 1n+r25:
743 match r25:
744 case 0n:
745 h => {==}
746 case 1n+r26:
747 match r26:
748 case 0n:
749 h => {==}
750 case 1n+r27:
751 match r27:
752 case 0n:
753 h => {==}
754 case 1n+r28:
755 match r28:
756 case 0n:
757 h => {==}
758 case 1n+r29:
759 match r29:
760 case 0n:
761 h => {==}
762 case 1n+r30:
763 match r30:
764 case 0n:
765 h => {==}
766 case 1n+r31:
767 match r31:
768 case 0n:
769 h => {==}
770 case 1n+r32:
771 pk.u8.c5(r32)