diff options
Diffstat (limited to 'src/Compilers/Z/BinaryNotationConstants.v')
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v new file mode 100644 index 000000000..f26364329 --- /dev/null +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -0,0 +1,91 @@ +Require Export Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Z.Syntax. +Require Export Bedrock.Word. +Require Export Crypto.Util.Notations. + +Local Notation Const x := (Op (OpConst x) TT). +(* python: +<< +print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n := (Const %s).''' % (b, d, h, i) + for d, h, b, i in sorted([(eval(bv), hex(eval(bv)), bv, i) + for (bv, i) in (('0b' + i[2:].replace('~', ''), i) + for i in r"""WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0 +WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 +WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 +WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0 +WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0 +WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 +WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 +WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~1~0~0~1~1 +WO~0~0~0~1~1~0~0~1 +WO~0~0~0~1~1~0~1~0 +WO~0~0~0~1~1~0~1~1 +WO~0~0~0~1~1~1~0~0 +WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0 +WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 +WO~0~0~1~1~0~0~1~1 +WO~1~0 +WO~1~0~0~1 +WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~1~0~0~0~1 +WO~0~0~0~1~0~1~1~1 +WO~1~1""".split('\n'))]))) +>> + *) +Notation "'0b10'" (* 2 (0x2) *) + := (Const WO~1~0). +Notation "'0b11'" (* 3 (0x3) *) + := (Const WO~1~1). +Notation "'0b1001'" (* 9 (0x9) *) + := (Const WO~1~0~0~1). +Notation "'0b00010001'" (* 17 (0x11) *) + := (Const WO~0~0~0~1~0~0~0~1). +Notation "'0b00010011'" (* 19 (0x13) *) + := (Const WO~0~0~0~1~0~0~1~1). +Notation "'0b00010111'" (* 23 (0x17) *) + := (Const WO~0~0~0~1~0~1~1~1). +Notation "'0b00011001'" (* 25 (0x19) *) + := (Const WO~0~0~0~1~1~0~0~1). +Notation "'0b00011010'" (* 26 (0x1a) *) + := (Const WO~0~0~0~1~1~0~1~0). +Notation "'0b00011011'" (* 27 (0x1b) *) + := (Const WO~0~0~0~1~1~0~1~1). +Notation "'0b00011100'" (* 28 (0x1c) *) + := (Const WO~0~0~0~1~1~1~0~0). +Notation "'0b00110011'" (* 51 (0x33) *) + := (Const WO~0~0~1~1~0~0~1~1). +Notation "'0b00000000011111111111111111111111'" (* 8388607 (0x7fffff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b00000001111111111111111111111111'" (* 33554431 (0x1ffffff) *) + := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b00000011111111111111111111111110'" (* 67108862 (0x3fffffe) *) + := (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). +Notation "'0b00000011111111111111111111111111'" (* 67108863 (0x3ffffff) *) + := (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b00000111111111111111111111011010'" (* 134217690 (0x7ffffda) *) + := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0). +Notation "'0b00000111111111111111111111101110'" (* 134217710 (0x7ffffee) *) + := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0). +Notation "'0b00000111111111111111111111111110'" (* 134217726 (0x7fffffe) *) + := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). +Notation "'0b00000111111111111111111111111111'" (* 134217727 (0x7ffffff) *) + := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b00001111111111111111111111111110'" (* 268435454 (0xffffffe) *) + := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). +Notation "'0b00001111111111111111111111111111'" (* 268435455 (0xfffffff) *) + := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b00011111111111111111111111111010'" (* 536870906 (0x1ffffffa) *) + := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0). +Notation "'0b00011111111111111111111111111110'" (* 536870910 (0x1ffffffe) *) + := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). +Notation "'0b0000000000000111111111111111111111111111111111111111111111111111'" (* 2251799813685247 (0x7ffffffffffffL) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b0000000000001111111111111111111111111111111111111111111111011010'" (* 4503599627370458 (0xfffffffffffdaL) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0). +Notation "'0b0000000000001111111111111111111111111111111111111111111111111110'" (* 4503599627370494 (0xffffffffffffeL) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). |