1	# Proofs of LAWS_gfm.bend: Gfm.elt masks with the field's mask, and masking
2	# twice is masking once (bit by bit)
3	import Base
4	import ./gfm.bend as M
5	import ./LAWS_gfm.bend as Laws
6	
7	def gfm_bool_and_idem(a: Bool, b: Bool) -> {Bool.and(a, b) == Bool.and(a, Bool.and(a, b)) : Bool}:
8	  match a:
9	    case True{}:
10	      {==}
11	    case False{}:
12	      {==}
13	
14	def gfm_word_and_idem(n: Nat, k: Word(n), a: Word(n)) -> {Word.and(n, k, a) == Word.and(n, k, Word.and(n, k, a)) : Word(n)}:
15	  match n:
16	    case 0n:
17	      match k a:
18	        case WNil{} WNil{}:
19	          {==}
20	    case 1n+p:
21	      match k a:
22	        case WCon{kh, kt} WCon{ah, at}:
23	          %gfm_bool_and_idem(kh, ah) : {WCon{Bool.and(kh, ah), Word.and(p, kt, at)} == WCon{_, Word.and(p, kt, Word.and(p, kt, at))} : Word(1n+p)}
24	          %gfm_word_and_idem(p, kt, at) : {WCon{Bool.and(kh, ah), Word.and(p, kt, at)} == WCon{Bool.and(kh, ah), _} : Word(1n+p)}
25	          {==}
26	
27	def gfm_u32_and_idem(k: U32, a: U32) -> {U32.and(k, a) == U32.and(k, U32.and(k, a)) : U32}:
28	  match k a:
29	    case U32{x} U32{y}:
30	      %gfm_word_and_idem(32n, x, y) : {U32{Word.and(32n, x, y)} == U32{_} : U32}
31	      {==}
32	
33	def Laws.gfm_mul_elt(f, a, b):
34	  %gfm_u32_and_idem(M.Gfm.mask(f), a) : {M.gfm.mul.raw(f, _, M.Gfm.elt(f, b)) == M.Gfm.mul(f, a, b) : U32}
35	  {==}