Need mathematical proof for CH and MAJ functions in SHA256

[Coding Enthusiast]

The SHA256 implementation that bitcoin-core is using has a different set of functions for CH and MAJ operations done in this hash function. While they both are nice little optimizations for skipping 1 bitwise operation, I can't figure out the mathematical proof for them being the same.

For reference:

Code:

CH = (x & y) | ((~x) & z)
CH_alt = z ^ (x & (y ^ z))

Code:

MAJ = (x & y) ^ (x & z) ^ (y & z)
MAJ_alt = (x & y) | (z & (x | y))

CH and MAJ are the functions from FIPS 180-3 while CH_alt and MAJ_alt are from bitcoin-core source code

[1714062259]

1714062259

[1714062259]

1714062259

[gmaxwell]

These functions are just simply three-bit input boolean functions (used bitslice style in SHA2).

With only 8 possible inputs exhaustion is a perfectly valid proof technique:

Code:

#include <stdio.h>
#include <stdlib.h>
int CH(int x,int y,int z) { return (x & y) | ((~x) & z); }
int CH_alt(int x,int y,int z) { return z ^ (x & (y ^ z)); }
int MAJ(int x,int y,int z) { return (x & y) ^ (x & z) ^ (y & z);}
int MAJ_alt(int x,int y,int z) { return (x & y) | (z & (x | y));};
int main(void){
  int x,y,z;
  for (x=0; x<2; x++) {
    for (y=0; y<2; y++) {
      for (z=0; z<2; z++) {
        if((CH(x,y,z) != CH_alt(x,y,z)) || (MAJ(x,y,z) != MAJ_alt(x,y,z))) {
          printf("quod est absurdum\n");
          exit(1);
        }
      }
    }
  }
  printf("QED\n");
  return 0;
}

[darosior]

The SHA256 implementation that bitcoin-core is using has a different set of functions for CH and MAJ operations done in this hash function. While they both are nice little optimizations for skipping 1 bitwise operation, I can't figure out the mathematical proof for them being the same.

For reference:

Code:

CH = (x & y) | ((~x) & z)
CH_alt = z ^ (x & (y ^ z))

Code:

MAJ = (x & y) ^ (x & z) ^ (y & z)
MAJ_alt = (x & y) | (z & (x | y))

CH and MAJ are the functions from FIPS 180-3 while CH_alt and MAJ_alt are from bitcoin-core source code

Code:

CH_alt = z ^ (x & (y ^ z))
CH_alt = (~z) & (x & (y ^ z)) | z & ((~x) | ~(y ^ z))  
CH_alt = x & (~z) & (y ^ z) | (z & (~x)) | (z & ~(y ^ z))
CH_alt = x & y | (z & (~x)) | (z & ~(y ^ z))
CH_alt = (x & y) | ((~x) & z)
CH_alt = CH

Hint :

Code:

(~z) & (y ^ z) = 0
z & ~(y ^ z) = 0