PROOF_gfm.bend

bend-osdev-gf@0.1.2.0 · 35 lines · 0 definitions

1# Proofs of LAWS_gfm.bend: Gfm.elt masks with the field's mask, and masking
2# twice is masking once (bit by bit)
3import Base
4import bend-osdev-gf@0.1.2.0/gfm.bend as M
5import bend-osdev-gf@0.1.2.0/LAWS_gfm.bend as Laws
6
7def 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
14def 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
27def 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
33def 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  {==}