def su_eq_n

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

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

350def su_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.su(PH.sext(u(a), u(b), u(c))) == u(a) : U32}:
351  match a b c:
352    case 0n 0n 0n:
353      {==}
354    case 0n 0n 1n:
355      {==}
356    case 0n 0n 2n:
357      {==}
358    case 0n 0n 3n:
359      {==}
360    case 0n 1n 0n:
361      {==}
362    case 0n 1n 1n:
363      {==}
364    case 0n 1n 2n:
365      {==}
366    case 0n 1n 3n:
367      {==}
368    case 0n 2n 0n:
369      {==}
370    case 0n 2n 1n:
371      {==}
372    case 0n 2n 2n:
373      {==}
374    case 0n 2n 3n:
375      {==}
376    case 0n 3n 0n:
377      {==}
378    case 0n 3n 1n:
379      {==}
380    case 0n 3n 2n:
381      {==}
382    case 0n 3n 3n:
383      {==}
384    case 1n 0n 0n:
385      {==}
386    case 1n 0n 1n:
387      {==}
388    case 1n 0n 2n:
389      {==}
390    case 1n 0n 3n:
391      {==}
392    case 1n 1n 0n:
393      {==}
394    case 1n 1n 1n:
395      {==}
396    case 1n 1n 2n:
397      {==}
398    case 1n 1n 3n:
399      {==}
400    case 1n 2n 0n:
401      {==}
402    case 1n 2n 1n:
403      {==}
404    case 1n 2n 2n:
405      {==}
406    case 1n 2n 3n:
407      {==}
408    case 1n 3n 0n:
409      {==}
410    case 1n 3n 1n:
411      {==}
412    case 1n 3n 2n:
413      {==}
414    case 1n 3n 3n:
415      {==}
416    case 2n 0n 0n:
417      {==}
418    case 2n 0n 1n:
419      {==}
420    case 2n 0n 2n:
421      {==}
422    case 2n 0n 3n:
423      {==}
424    case 2n 1n 0n:
425      {==}
426    case 2n 1n 1n:
427      {==}
428    case 2n 1n 2n:
429      {==}
430    case 2n 1n 3n:
431      {==}
432    case 2n 2n 0n:
433      {==}
434    case 2n 2n 1n:
435      {==}
436    case 2n 2n 2n:
437      {==}
438    case 2n 2n 3n:
439      {==}
440    case 2n 3n 0n:
441      {==}
442    case 2n 3n 1n:
443      {==}
444    case 2n 3n 2n:
445      {==}
446    case 2n 3n 3n:
447      {==}
448    case 3n 0n 0n:
449      {==}
450    case 3n 0n 1n:
451      {==}
452    case 3n 0n 2n:
453      {==}
454    case 3n 0n 3n:
455      {==}
456    case 3n 1n 0n:
457      {==}
458    case 3n 1n 1n:
459      {==}
460    case 3n 1n 2n:
461      {==}
462    case 3n 1n 3n:
463      {==}
464    case 3n 2n 0n:
465      {==}
466    case 3n 2n 1n:
467      {==}
468    case 3n 2n 2n:
469      {==}
470    case 3n 2n 3n:
471      {==}
472    case 3n 3n 0n:
473      {==}
474    case 3n 3n 1n:
475      {==}
476    case 3n 3n 2n:
477      {==}
478    case 3n 3n 3n:
479      {==}
480    case 4n+r _ _:
481      Empty.absurd({PH.su(PH.sext(u(4n+r), u(b), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, ha))
482    case 0n 4n+r _:
483      Empty.absurd({PH.su(PH.sext(u(0n), u(4n+r), u(c))) == u(0n) : U32}, N.lt_zero_absurd(r, hb))
484    case 0n 0n 4n+r:
485      Empty.absurd({PH.su(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
486    case 0n 1n 4n+r:
487      Empty.absurd({PH.su(PH.sext(u(0n), u(1n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
488    case 0n 2n 4n+r:
489      Empty.absurd({PH.su(PH.sext(u(0n), u(2n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
490    case 0n 3n 4n+r:
491      Empty.absurd({PH.su(PH.sext(u(0n), u(3n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
492    case 1n 4n+r _:
493      Empty.absurd({PH.su(PH.sext(u(1n), u(4n+r), u(c))) == u(1n) : U32}, N.lt_zero_absurd(r, hb))
494    case 1n 0n 4n+r:
495      Empty.absurd({PH.su(PH.sext(u(1n), u(0n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
496    case 1n 1n 4n+r:
497      Empty.absurd({PH.su(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
498    case 1n 2n 4n+r:
499      Empty.absurd({PH.su(PH.sext(u(1n), u(2n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
500    case 1n 3n 4n+r:
501      Empty.absurd({PH.su(PH.sext(u(1n), u(3n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
502    case 2n 4n+r _:
503      Empty.absurd({PH.su(PH.sext(u(2n), u(4n+r), u(c))) == u(2n) : U32}, N.lt_zero_absurd(r, hb))
504    case 2n 0n 4n+r:
505      Empty.absurd({PH.su(PH.sext(u(2n), u(0n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
506    case 2n 1n 4n+r:
507      Empty.absurd({PH.su(PH.sext(u(2n), u(1n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
508    case 2n 2n 4n+r:
509      Empty.absurd({PH.su(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
510    case 2n 3n 4n+r:
511      Empty.absurd({PH.su(PH.sext(u(2n), u(3n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
512    case 3n 4n+r _:
513      Empty.absurd({PH.su(PH.sext(u(3n), u(4n+r), u(c))) == u(3n) : U32}, N.lt_zero_absurd(r, hb))
514    case 3n 0n 4n+r:
515      Empty.absurd({PH.su(PH.sext(u(3n), u(0n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
516    case 3n 1n 4n+r:
517      Empty.absurd({PH.su(PH.sext(u(3n), u(1n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
518    case 3n 2n 4n+r:
519      Empty.absurd({PH.su(PH.sext(u(3n), u(2n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
520    case 3n 3n 4n+r:
521      Empty.absurd({PH.su(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))