diff options
author | Jason Gross <jgross@mit.edu> | 2017-02-10 15:58:19 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-02-10 15:58:19 -0500 |
commit | 659693536444e6aeab4feee49996f27afb5d090b (patch) | |
tree | 18c8eacaba0df81e0947ea79261ffc2c61baff43 /src | |
parent | 32849ba878e74064e2bb312ea0a5f2e2e2ed6659 (diff) |
Add files for constant reflective notations
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Z/BinaryNotationConstants.v | 91 | ||||
-rw-r--r-- | src/Reflection/Z/HexNotationConstants.v | 92 |
2 files changed, 183 insertions, 0 deletions
diff --git a/src/Reflection/Z/BinaryNotationConstants.v b/src/Reflection/Z/BinaryNotationConstants.v new file mode 100644 index 000000000..32a993e08 --- /dev/null +++ b/src/Reflection/Z/BinaryNotationConstants.v @@ -0,0 +1,91 @@ +Require Export Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.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). diff --git a/src/Reflection/Z/HexNotationConstants.v b/src/Reflection/Z/HexNotationConstants.v new file mode 100644 index 000000000..6df9b9b2b --- /dev/null +++ b/src/Reflection/Z/HexNotationConstants.v @@ -0,0 +1,92 @@ +Require Import Coq.ZArith.ZArith. +Require Export Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Z.Syntax. +Require Export Bedrock.Word. +Require Export Crypto.Util.Notations. + +Notation Const x := (Op (OpConst x) TT). +(* python: +<< +print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n := (Const %s%%Z).''' % (h, d, h, d) + 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 "'0x2'" (* 2 (0x2) *) + := (Const 2%Z). +Notation "'0x3'" (* 3 (0x3) *) + := (Const 3%Z). +Notation "'0x9'" (* 9 (0x9) *) + := (Const 9%Z). +Notation "'0x11'" (* 17 (0x11) *) + := (Const 17%Z). +Notation "'0x13'" (* 19 (0x13) *) + := (Const 19%Z). +Notation "'0x17'" (* 23 (0x17) *) + := (Const 23%Z). +Notation "'0x19'" (* 25 (0x19) *) + := (Const 25%Z). +Notation "'0x1a'" (* 26 (0x1a) *) + := (Const 26%Z). +Notation "'0x1b'" (* 27 (0x1b) *) + := (Const 27%Z). +Notation "'0x1c'" (* 28 (0x1c) *) + := (Const 28%Z). +Notation "'0x33'" (* 51 (0x33) *) + := (Const 51%Z). +Notation "'0x7fffff'" (* 8388607 (0x7fffff) *) + := (Const 8388607%Z). +Notation "'0x1ffffff'" (* 33554431 (0x1ffffff) *) + := (Const 33554431%Z). +Notation "'0x3fffffe'" (* 67108862 (0x3fffffe) *) + := (Const 67108862%Z). +Notation "'0x3ffffff'" (* 67108863 (0x3ffffff) *) + := (Const 67108863%Z). +Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *) + := (Const 134217690%Z). +Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *) + := (Const 134217710%Z). +Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *) + := (Const 134217726%Z). +Notation "'0x7ffffff'" (* 134217727 (0x7ffffff) *) + := (Const 134217727%Z). +Notation "'0xffffffe'" (* 268435454 (0xffffffe) *) + := (Const 268435454%Z). +Notation "'0xfffffff'" (* 268435455 (0xfffffff) *) + := (Const 268435455%Z). +Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *) + := (Const 536870906%Z). +Notation "'0x1ffffffe'" (* 536870910 (0x1ffffffe) *) + := (Const 536870910%Z). +Notation "'0x7ffffffffffff'" (* 2251799813685247 (0x7ffffffffffff) *) + := (Const 2251799813685247%Z). +Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *) + := (Const 4503599627370458%Z). +Notation "'0xffffffffffffe'" (* 4503599627370494 (0xffffffffffffe) *) + := (Const 4503599627370494%Z). |