def sv_eq_n

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:529

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

529def sv_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sv(PH.sext(u(a), u(b), u(c))) == u(b) : U32}:
530  match a b c:
531    case 0n 0n 0n:
532      {==}
533    case 0n 0n 1n:
534      {==}
535    case 0n 0n 2n:
536      {==}
537    case 0n 0n 3n:
538      {==}
539    case 0n 1n 0n:
540      {==}
541    case 0n 1n 1n:
542      {==}
543    case 0n 1n 2n:
544      {==}
545    case 0n 1n 3n:
546      {==}
547    case 0n 2n 0n:
548      {==}
549    case 0n 2n 1n:
550      {==}
551    case 0n 2n 2n:
552      {==}
553    case 0n 2n 3n:
554      {==}
555    case 0n 3n 0n:
556      {==}
557    case 0n 3n 1n:
558      {==}
559    case 0n 3n 2n:
560      {==}
561    case 0n 3n 3n:
562      {==}
563    case 1n 0n 0n:
564      {==}
565    case 1n 0n 1n:
566      {==}
567    case 1n 0n 2n:
568      {==}
569    case 1n 0n 3n:
570      {==}
571    case 1n 1n 0n:
572      {==}
573    case 1n 1n 1n:
574      {==}
575    case 1n 1n 2n:
576      {==}
577    case 1n 1n 3n:
578      {==}
579    case 1n 2n 0n:
580      {==}
581    case 1n 2n 1n:
582      {==}
583    case 1n 2n 2n:
584      {==}
585    case 1n 2n 3n:
586      {==}
587    case 1n 3n 0n:
588      {==}
589    case 1n 3n 1n:
590      {==}
591    case 1n 3n 2n:
592      {==}
593    case 1n 3n 3n:
594      {==}
595    case 2n 0n 0n:
596      {==}
597    case 2n 0n 1n:
598      {==}
599    case 2n 0n 2n:
600      {==}
601    case 2n 0n 3n:
602      {==}
603    case 2n 1n 0n:
604      {==}
605    case 2n 1n 1n:
606      {==}
607    case 2n 1n 2n:
608      {==}
609    case 2n 1n 3n:
610      {==}
611    case 2n 2n 0n:
612      {==}
613    case 2n 2n 1n:
614      {==}
615    case 2n 2n 2n:
616      {==}
617    case 2n 2n 3n:
618      {==}
619    case 2n 3n 0n:
620      {==}
621    case 2n 3n 1n:
622      {==}
623    case 2n 3n 2n:
624      {==}
625    case 2n 3n 3n:
626      {==}
627    case 3n 0n 0n:
628      {==}
629    case 3n 0n 1n:
630      {==}
631    case 3n 0n 2n:
632      {==}
633    case 3n 0n 3n:
634      {==}
635    case 3n 1n 0n:
636      {==}
637    case 3n 1n 1n:
638      {==}
639    case 3n 1n 2n:
640      {==}
641    case 3n 1n 3n:
642      {==}
643    case 3n 2n 0n:
644      {==}
645    case 3n 2n 1n:
646      {==}
647    case 3n 2n 2n:
648      {==}
649    case 3n 2n 3n:
650      {==}
651    case 3n 3n 0n:
652      {==}
653    case 3n 3n 1n:
654      {==}
655    case 3n 3n 2n:
656      {==}
657    case 3n 3n 3n:
658      {==}
659    case 4n+r _ _:
660      Empty.absurd({PH.sv(PH.sext(u(4n+r), u(b), u(c))) == u(b) : U32}, N.lt_zero_absurd(r, ha))
661    case 0n 4n+r _:
662      Empty.absurd({PH.sv(PH.sext(u(0n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
663    case 0n 0n 4n+r:
664      Empty.absurd({PH.sv(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
665    case 0n 1n 4n+r:
666      Empty.absurd({PH.sv(PH.sext(u(0n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
667    case 0n 2n 4n+r:
668      Empty.absurd({PH.sv(PH.sext(u(0n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
669    case 0n 3n 4n+r:
670      Empty.absurd({PH.sv(PH.sext(u(0n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
671    case 1n 4n+r _:
672      Empty.absurd({PH.sv(PH.sext(u(1n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
673    case 1n 0n 4n+r:
674      Empty.absurd({PH.sv(PH.sext(u(1n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
675    case 1n 1n 4n+r:
676      Empty.absurd({PH.sv(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
677    case 1n 2n 4n+r:
678      Empty.absurd({PH.sv(PH.sext(u(1n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
679    case 1n 3n 4n+r:
680      Empty.absurd({PH.sv(PH.sext(u(1n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
681    case 2n 4n+r _:
682      Empty.absurd({PH.sv(PH.sext(u(2n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
683    case 2n 0n 4n+r:
684      Empty.absurd({PH.sv(PH.sext(u(2n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
685    case 2n 1n 4n+r:
686      Empty.absurd({PH.sv(PH.sext(u(2n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
687    case 2n 2n 4n+r:
688      Empty.absurd({PH.sv(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
689    case 2n 3n 4n+r:
690      Empty.absurd({PH.sv(PH.sext(u(2n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
691    case 3n 4n+r _:
692      Empty.absurd({PH.sv(PH.sext(u(3n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
693    case 3n 0n 4n+r:
694      Empty.absurd({PH.sv(PH.sext(u(3n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
695    case 3n 1n 4n+r:
696      Empty.absurd({PH.sv(PH.sext(u(3n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
697    case 3n 2n 4n+r:
698      Empty.absurd({PH.sv(PH.sext(u(3n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
699    case 3n 3n 4n+r:
700      Empty.absurd({PH.sv(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))