Key proof statement

[xhliu]

import "hashes/sha256/sha256" as sha256

def main(private field a, private field b, field h0, field h1):
    field[2] h = sha256([a, b])
    assert(h[0] == h0);
    assert(h[1] == h1);
    return