def hex_word_and

qasim-bend-kit@0.1.0.2 · libs/AES256GCM.bend:180

import Base

180# The mask-first implementation keeps zero mask bits visibly false to Bend's
181# checker, which supports the nibble range proofs used by the codec.
182def hex_word_and(n: Nat, mask: Word(n), +value: Word(n)) -> Word(n):
183    match n:
184        case 0n: WNil{}
185        case 1n+p:
186            match mask:
187                case WCon{False{}, mask_tail}:
188                    match value:
189                        case WCon{_, value_tail}:
190                            WCon{False{}, hex_word_and(p, mask_tail, value_tail)}
191                case WCon{True{}, mask_tail}:
192                    match value:
193                        case WCon{bit, value_tail}:
194                            WCon{bit, hex_word_and(p, mask_tail, value_tail)}