Author

Topic: Need mathematical proof for CH and MAJ functions in SHA256 (Read 193 times)

sr. member
Activity: 279
Merit: 435
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
staff
Activity: 4284
Merit: 8808

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 
#include
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;
}
legendary
Activity: 1042
Merit: 2805
Bitcoin and C♯ 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
Jump to: