Skip to content
Permalink

Comparing changes

This is a direct comparison between two commits made in this repository or its related repositories. View the default comparison for this range or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: mit-plv/fiat-crypto
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 9f314d0701779276f981ba7094e6846243446ba3
Choose a base ref
..
head repository: mit-plv/fiat-crypto
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: cdb1c27b340b168396aea79898e7303dade97b26
Choose a head ref
196 changes: 145 additions & 51 deletions fiat-amd64/gentest.py
View file
Original file line number Diff line number Diff line change
@@ -7,52 +7,65 @@
import os
from collections import OrderedDict


# in Python 3.9 and newer, this is primitive as str.removesuffix
def removesuffix(s, suffix):
if s.endswith(suffix): return s[:-len(suffix)]
if s.endswith(suffix):
return s[: -len(suffix)]
return s


def removeprefix(s, prefix):
if s.startswith(prefix): return s[len(prefix):]
if s.startswith(prefix):
return s[len(prefix) :]
return s


# grep -oP "src/.*square" fiat-c/src/*64*.c

#unsaturated_solinas
solinasprimes = dict( # num limbs, prime
curve25519=('5', '2^255 - 19'),
p448_solinas=('8', '2^448 - 2^224 - 1'),
p521=('9', '2^521 - 1'),
poly1305=('3', '2^130 - 5'))
# unsaturated_solinas
solinasprimes = dict( # num limbs, prime
curve25519=("5", "2^255 - 19"),
p448_solinas=("8", "2^448 - 2^224 - 1"),
p521=("9", "2^521 - 1"),
poly1305=("3", "2^130 - 5"),
)

montgomeryprimes = dict(
curve25519_scalar='2^252 + 27742317777372353535851937790883648493',
p224='2^224 - 2^96 + 1',
p256='2^256 - 2^224 + 2^192 + 2^96 - 1',
p256_scalar='2^256 - 2^224 + 2^192 - 89188191075325690597107910205041859247',
p384='2^384 - 2^128 - 2^96 + 2^32 - 1',
p384_scalar='2^384 - 1388124618062372383947042015309946732620727252194336364173',
p434='2^216 * 3^137 - 1',
secp256k1_montgomery='2^256 - 2^32 - 977',
secp256k1_scalar='2^256 - 432420386565659656852420866394968145599')
curve25519_scalar="2^252 + 27742317777372353535851937790883648493",
p224="2^224 - 2^96 + 1",
p256="2^256 - 2^224 + 2^192 + 2^96 - 1",
p256_scalar="2^256 - 2^224 + 2^192 - 89188191075325690597107910205041859247",
p384="2^384 - 2^128 - 2^96 + 2^32 - 1",
p384_scalar="2^384 - 1388124618062372383947042015309946732620727252194336364173",
p434="2^216 * 3^137 - 1",
secp256k1_montgomery="2^256 - 2^32 - 977",
secp256k1_scalar="2^256 - 432420386565659656852420866394968145599",
)

saturatedsolinasprimes = dict(
curve25519_solinas=('2^255 - 19'))
saturatedsolinasprimes = dict(curve25519_solinas=("2^255 - 19"))

dettmanprimes = dict( # last limb width, limbs, last reduction, prime
secp256k1_dettman=('48', '5', '2', '2^256 - 4294968273'))
dettmanprimes = dict( # last limb width, limbs, last reduction, prime
secp256k1_dettman=("48", "5", "2", "2^256 - 4294968273")
)

output_makefile = ('--makefile' in sys.argv[1:])
directories = tuple(i for i in sys.argv[1:] if i not in ('--makefile',))
output_makefile = "--makefile" in sys.argv[1:]
directories = tuple(i for i in sys.argv[1:] if i not in ("--makefile",))

asm_op_names = OrderedDict()

regex = re.compile(r'fiat_(?P<name>[^_]+(_(solinas|montgomery|dettman))?)_(?P<op>(carry_)?(square|mul))')
regex = re.compile(
r"fiat_(?P<name>[^_]+(_(solinas|montgomery|dettman))?)_(?P<op>(carry_)?(square|mul|from_bytes|to_bytes|add|sub|opp))"
)
for dirname in directories:
m = regex.match(os.path.basename(dirname))
if m:
for fname in os.listdir(dirname):
groups = m.groupdict()
asm_op_names.setdefault((groups['name'], groups['op']), []).append(os.path.join(dirname,fname))
asm_op_names.setdefault((groups["name"], groups["op"]), []).append(
os.path.join(dirname, fname)
)


def asm_op_names_key(val):
(name, op), fnames = val
@@ -74,26 +87,36 @@ def asm_op_names_key(val):
kind = 3
n, prime = solinasprimes[name]

else:
assert False, name

return (kind, n, prime, op, name, fnames)


def is_small(val):
(kind, n, prime, op, name, fnames) = asm_op_names_key(val)
prime = eval(prime.replace('^', '**'))
prime = eval(prime.replace("^", "**"))
return math.log2(prime) / 64 <= 4


asm_op_names_items = tuple(sorted(asm_op_names.items(), key=asm_op_names_key))
small_asm_op_names_items = tuple(val for val in asm_op_names_items if is_small(val))

status_file_stems = [f'fiat-amd64/{name}-{op}' for (name, op), _fnames in asm_op_names_items]
small_status_file_stems = [f'fiat-amd64/{name}-{op}' for (name, op), _fnames in small_asm_op_names_items]
status_file_stems = [
f"fiat-amd64/{name}-{op}" for (name, op), _fnames in asm_op_names_items
]
small_status_file_stems = [
f"fiat-amd64/{name}-{op}" for (name, op), _fnames in small_asm_op_names_items
]

status_files = [stem + '.status' for stem in status_file_stems]
only_status_files = [stem + '.only-status' for stem in status_file_stems]
small_status_files = [stem + '.status' for stem in small_status_file_stems]
small_only_status_files = [stem + '.only-status' for stem in small_status_file_stems]
status_files = [stem + ".status" for stem in status_file_stems]
only_status_files = [stem + ".only-status" for stem in status_file_stems]
small_status_files = [stem + ".status" for stem in small_status_file_stems]
small_only_status_files = [stem + ".only-status" for stem in small_status_file_stems]

if output_makefile:
print(f'''
print(
f"""
# Allow SLOWEST_FIRST=1 to be passed to test files in reverse order.
# When testing interactively, we probably want to test quicker files
@@ -106,34 +129,104 @@ def is_small(val):
AMD64_ASM_SMALL_STATUS_FILES := $(if $(SLOWEST_FIRST),{' '.join(reversed(small_status_files))},{' '.join(small_status_files)})
AMD64_ASM_SMALL_ONLY_STATUS_FILES := $(if $(SLOWEST_FIRST),{' '.join(reversed(small_only_status_files))},{' '.join(small_only_status_files)})
''')
"""
)

for item in asm_op_names_items:
(kind, n, prime, op, name, fnames) = asm_op_names_key(item)
if kind == 0:
binary = 'src/ExtractionOCaml/dettman_multiplication'
binary_descr = 'Dettman Multiplication'
binary = "src/ExtractionOCaml/dettman_multiplication"
binary_descr = "Dettman Multiplication"
limbwidth, _n, last_reduction, _prime = dettmanprimes[name]
invocation = ' '.join([binary, name, '64', n, limbwidth, last_reduction, shlex.quote(prime), op, '--no-wide-int', '--shiftr-avoid-uint1'] + [item for fname in fnames for item in ('--hints-file', shlex.quote(fname))])
invocation = " ".join(
[
binary,
name,
"64",
n,
limbwidth,
last_reduction,
shlex.quote(prime),
op,
"--no-wide-int",
"--shiftr-avoid-uint1",
]
+ [
item
for fname in fnames
for item in ("--hints-file", shlex.quote(fname))
]
)
elif kind == 1:
binary = 'src/ExtractionOCaml/solinas_reduction'
binary_descr = 'Saturated Solinas'
invocation = ' '.join([binary, name, '64', shlex.quote(prime), op, '--no-wide-int', '--shiftr-avoid-uint1'] + [item for fname in fnames for item in ('--hints-file', shlex.quote(fname))])
binary = "src/ExtractionOCaml/solinas_reduction"
binary_descr = "Saturated Solinas"
invocation = " ".join(
[
binary,
name,
"64",
shlex.quote(prime),
op,
"--no-wide-int",
"--shiftr-avoid-uint1",
]
+ [
item
for fname in fnames
for item in ("--hints-file", shlex.quote(fname))
]
)
elif kind == 2:
binary = 'src/ExtractionOCaml/word_by_word_montgomery'
binary_descr = 'Word-by-Word Montgomery'
invocation = ' '.join([binary, name, '64', shlex.quote(prime), op, '--no-wide-int', '--shiftr-avoid-uint1'] + [item for fname in fnames for item in ('--hints-file', shlex.quote(fname))])
binary = "src/ExtractionOCaml/word_by_word_montgomery"
binary_descr = "Word-by-Word Montgomery"
invocation = " ".join(
[
binary,
name,
"64",
shlex.quote(prime),
op,
"--no-wide-int",
"--shiftr-avoid-uint1",
]
+ [
item
for fname in fnames
for item in ("--hints-file", shlex.quote(fname))
]
)
elif kind == 3:
binary = 'src/ExtractionOCaml/unsaturated_solinas'
binary_descr = 'Unsaturated Solinas'
invocation = ' '.join([binary, name, '64', n, shlex.quote(prime), op, '--no-wide-int', '--shiftr-avoid-uint1', '--tight-bounds-mul-by', '1.000001'] + [item for fname in fnames for item in ('--hints-file', shlex.quote(fname))])
binary = "src/ExtractionOCaml/unsaturated_solinas"
binary_descr = "Unsaturated Solinas"
invocation = " ".join(
[
binary,
name,
"64",
n,
shlex.quote(prime),
op,
"--no-wide-int",
"--shiftr-avoid-uint1",
"--tight-bounds-mul-by",
"1.000001",
]
+ [
item
for fname in fnames
for item in ("--hints-file", shlex.quote(fname))
]
)
else:
assert False, name
if output_makefile:
short_fnames = [removesuffix(os.path.basename(fname),'.asm') for fname in fnames]
short_fnames = [
removesuffix(os.path.basename(fname), ".asm") for fname in fnames
]
description = f'{name} {prime.replace(" ", "")} ({op}) ({binary_descr}) ({" ".join(short_fnames)})'
output_name = f'fiat-amd64/{name}-{op}'
print(f'''
output_name = f"fiat-amd64/{name}-{op}"
print(
f"""
only-test-amd64-files-print-report:: {output_name}.only-status
\t@ test $$(cat $<) -eq 0 || echo 'TEST AMD64 {description} ... \t$(RED)$(BOLD)FAILED$(NORMAL)$(NC)'
@@ -159,6 +252,7 @@ def is_small(val):
\t cat {output_name}.stdout; \\
\t echo '============================================'; \\
\t exit 1; }}
''')
"""
)
else:
print(invocation, '-o', '/dev/null', '--output-asm', '/dev/null')
print(invocation, "-o", "/dev/null", "--output-asm", "/dev/null")
4 changes: 3 additions & 1 deletion src/Assembly/Equality.v
View file
Original file line number Diff line number Diff line change
@@ -273,6 +273,7 @@ Definition RawLine_beq (x y : RawLine) : bool
| INSTR x, INSTR y => NormalInstruction_beq x y
| ALIGN x, ALIGN y => String.eqb x y
| DIRECTIVE x, DIRECTIVE y => String.eqb x y
| ASCII_ z x, ASCII_ z' y => Bool.eqb z z' && String.eqb x y
| SECTION _, _
| GLOBAL _, _
| LABEL _, _
@@ -281,8 +282,9 @@ Definition RawLine_beq (x y : RawLine) : bool
| ALIGN _, _
| DEFAULT_REL, _
| DIRECTIVE _, _
| ASCII_ _ _, _
=> false
end.
end%bool.
Global Arguments RawLine_beq !_ !_ / .

Infix "=?" := RawLine_beq : RawLine_scope.
21 changes: 11 additions & 10 deletions src/Assembly/Equivalence.v
View file
Original file line number Diff line number Diff line change
@@ -421,18 +421,19 @@ Definition describe_idx_from_state
| ExprApp (old _ _, _) => true
| _ => false
end in
match is_old, description_from_state, show_full with
| true, Some descr, _
| _, Some descr, true
match is_old, description_from_state, show_full, dag.lookup st.(dag_state) idx with
| true, Some descr, false, _
| _, Some descr, _, None
=> [show idx ++ " is " ++ descr ++ "."]
| true, None, _
| _, Some descr, true, Some e
=> [show idx ++ " is " ++ descr ++ " (" ++ show_node_lite e ++ ")."]
| true, None, _, _
=> [show idx ++ " is a special value no longer present in the symbolic machine state at the end of execution."]
| _, _, false => []
| _, None, true
=> [show idx ++ " is " ++ match dag.lookup st.(dag_state) idx with
| Some e => show_node_lite e
| None => "not in the dag"
end]
| _, _, false, _ => []
| _, None, true, Some e
=> [show idx ++ " is " ++ show_node_lite e ++ "."]
| _, None, true, None
=> [show idx ++ " is not in the dag."]
end%string.

Definition iteratively_describe_idxs_after
Loading