Re: [PATCH 2/4] sha1dc-accel: vectorize the unavoidable-bitconditions check

Hi Scott,

On Tue, 29 Sep 2026, Scott Chacon wrote:

This is quite large. And of course it's essentially a machine-assisted translation of the Rust code, which itself is the output of the solver.

Assuming that we will not only want to be able to confirm the translation easily, but also be able to adapt to future improvements in the Rust code (e.g. if Sam finds another neat trick to dismiss even more candidates even earlier), here is a Perl script to do precisely that:

-- snip -- #!/usr/bin/perl # Convert the generated src/ubc_check/{scalar,sse2,avx2,neon}.rs files at # https://github.com/srijs/sha1dc/tree/426b4afd to C table definitions. # Usage: perl sha1dc-accel/generate-ubc-tables.pl sse2 < path/to/sse2.rs # Output is tables only; retain ubc_check.c's declarations and MIT notice. use strict; use warnings;

my $form = shift // die "usage: $0 scalar|sse2|avx2|neon < form.rs\n"; my %prefix_count = (scalar => 70, sse2 => 26, avx2 => 16, neon => 20); my %tail_count = (scalar => 151, sse2 => 97, avx2 => 77, neon => 137); exists $prefix_count{$form} && !@ARGV or die "unknown form: $form\n"; local $/; my $src = <STDIN> // die "empty input\n"; my ($prefix) = $src =~ /^fn prefix\([^\n]*\) -> u32 \{(.*?)^\}/ms; defined $prefix or die "missing prefix()\n"; $prefix =~ s/\(([^()]*)\)\s+as\s+i32/$1/g; $prefix =~ s/\b(\d+)u32\b/$1/g; my (@out, @rows);

sub table {
	my ($type, $name, $rows) = @_;
	push @out, "static const struct $type ${form}_$name\[\] = {\n",
		map("\t{ $_ },\n", @$rows), "};\n\n";
}

sub condition {
	my ($expr) = @_;
	$expr =~ s/[\s()]//g;
	$expr =~ s/&1$//;
	$expr =~ /\Aw\[(\d+)\](?:>>(\d+))?\^w\[(\d+)\]
		(?:>>(\d+))?(?:\^([01]))?\z/x
		or die "unknown condition: $expr\n";
	return [$1, $2 // 0, $3, $4 // 0, $5 // 0];
}

sub vector {
	my ($expr, $width) = @_;
	my @v;
	if ($expr =~ /(?:_mm(?:256)?_set1_epi32|vdupq_n_u32)\(([^()]*)\)/) {
		@v = ($1) x $width;
	} elsif ($expr =~ /(?:_mm(?:256)?_set_epi32)\(([^()]*)\)/
		|| $expr =~ /splat\(\[([^\]]*)\]\)/s) {
		@v = split /\s*,\s*/, $1;
	} else {
		die "unknown vector: $expr\n";
	}
	@v == $width or die "wrong lane count: $expr\n";
	for (@v) {
		s/^\s+|\s+$//g;
		/\A(?:0|1\s*<<\s*\d+|DV_I{1,2}_\d+_\d+_BIT
			(?:\s*\|\s*DV_I{1,2}_\d+_\d+_BIT)*)\z/x
			or die "unknown lane: $_\n";
		s/\b1\s*<</1u <</;
	}
	# The pinned x86 source lists logical step order, despite set_epi32.
	return "{ " . join(", ", @v) . " }";
}

if ($form eq "scalar") {
	while ($prefix =~ /mask\s*&=\s*(.*?);/sg) {
		my ($expr, $dvs) = $1 =~ /\A(.*?)\s*\|\s*!\(([^()]*)\)\s*\z/s;
		defined $dvs or die "unknown scalar prefix\n";
		$expr =~ s/\s//g;
		my ($bits, $want);
		if ($expr =~ /\A(.*)\.wrapping_sub\(1\)\z/s) {
			($bits, $want) = ($1, 0);
		} elsif ($expr =~ /\A\(0\)\.wrapping_sub\((.*)\)\z/s) {
			($bits, $want) = ($1, 1);
		} else {
			die "unknown scalar mask: $expr\n";
		}
		my $c = condition($bits);
		$c->[4] = $want;
		$dvs =~ s/\s+/ /g;
		push @rows, "{ " . join(", ", @$c) . " }, $dvs";
	}
	table("ubc_prefix_cond", "prefix_conds", \@rows);
} else {
	my $width = $form eq "avx2" ? 8 : 4;
	my %want = (
		"_mm_and_si128(miss,bits)" => 1,
		"_mm_andnot_si128(miss,bits)" => 0,
		"_mm256_and_si256(miss,bits)" => 1,
		"_mm256_andnot_si256(miss,bits)" => 0,
		"vqsubq_u32(bits,set)" => 1,
		"vminq_u32(set,bits)" => 0,
	);
	while ($prefix =~ /\{\s*(let near =.*?)\}/sg) {
		my $g = $1;
		$g =~ s/\s//g;
		my ($lo, $hi, $x, $test, $dvs, $acc) = $g =~
			/\Alet near = load::<(\d+)>\(w\);\s*
			let far = load::<(\d+)>\(w\);\s*let x = (.*?);\s*
			let (?:tested|set) = (.*?);\s*
			(?:let miss = [^;]*;\s*)?let bits = (.*?);\s*
			acc[01] = \w+\(acc[01],\s*(.*?)\);\s*\z/sx;
		defined $acc or die "unknown vector group: $g\n";
		$x =~ s/(?:_mm(?:256)?_xor_si(?:128|256)|veorq_u32)/xor/g;
		$x =~ s/(?:_mm(?:256)?_srli_epi32|vshrq_n_u32)/shr/g;
		$x =~ s/\s//g;
		$x =~ /\Axor\((?:shr\(near,(\d+)\)|near),
			(?:shr\(far,(\d+)\)|far)\)\z/x
			or die "unknown vector XOR: $x\n";
		my ($ls, $hs) = ($1 // 0, $2 // 0);
		$acc =~ s/\s//g;
		exists $want{$acc} or die "unknown predicate: $acc\n";
		push @rows, join(", ", $lo, $ls // 0, $hi, $hs // 0,
			$want{$acc}, vector($test, $width),
			vector($dvs, $width));
	}
	table("ubc_group$width", "groups", \@rows);
}
@rows == $prefix_count{$form} or die "wrong prefix count\n";

if ($form ne "neon") {
	for my $key ("CHECKS", "SPANS") {
		my ($n, $body) = $src =~ /static\s+TAIL_$key:[^\n]*;
			\s*(\d+)\]\s*=\s*\[(.*?)^\];/msx;
		defined $body or die "missing TAIL_$key\n";
		my @tuples = $body =~ /\((\d+(?:\s*,\s*\d+)*)\)/g;
		@tuples == $n && $n == ($key eq "CHECKS" ?
			$tail_count{$form} : 32) or die "wrong tail count\n";
		table($key eq "CHECKS" ? "ubc_cond" : "tail_span",
			"tail_" . lc($key), \@tuples);
	}
} else {
	my @dv;
	my ($tail) = $src =~ /^fn tail\([^\n]*\) -> u32 \{(.*?)^\}/ms;
	defined $tail or die "missing tail()\n";
	$tail =~ s/\s//g;
	while ($tail =~ /if mask & DV_I{1,2}_\d+_\d+_BIT != 0 \{\s*
		let fail = (.*?);\s*out &= !(?:fail|\(fail << (\d+)\));/sgx) {
		my ($expr, $d) = ($1, $2 // 0);
		$d < 32 && !defined $dv[$d] or die "duplicate/invalid DV\n";
		$expr =~ s/[\s()]//g;
		$expr =~ s/&1$// or die "unknown tail mask\n";
		$dv[$d] = [map { join(", ", @{condition($_)}) }
			split /\|/, $expr];
	}
	my (@checks, @spans);
	for my $d (0 .. 31) {
		my $c = $dv[$d] // [];
		push @spans, scalar(@checks) . ", " . scalar(@$c);
		push @checks, @$c;
	}
	@checks == $tail_count{$form} or die "wrong NEON tail count\n";
	table("ubc_cond", "tail_checks", \@checks);
	table("tail_span", "tail_spans", \@spans);
}
print @out;
-- snap --

This Perl script reproduces the tables (although with different formatting, and without the inline comments, I verified it with `--patience --color-words="[A-Za-z0-9_]+|."`).

As is my rule, I only offer code that I wrote with AI assistance if the output is close enough to what I would have written myself if I had the time (and wouldn't need to take care of my arm muscles' health), and this Perl script is no exception. My first draft would probably have used less informative (or no) error messages, and I only learned about that `//` operator during this session.

With all that out of the way, I would like to ask to include this script in the patch (or in a follow-up patch) so that the lengthy `ubc_check.c` file's tables can be validated/regenerated independently.

While this code is correct, I think it is slightly misleading: depending on `want`, it either subtracts `set` from `dvs`, or takes the minimum. But that only happens to be what is desired because each lane of `set` is all ones or all zero. What we actually want is to mask either those lanes or everything but those lanes, i.e. `dvs & ~set` or `dvs & set`, respectively. That would be:

		fail = g->want ? vbicq_u32(dvs, set) : vandq_u32(dvs, set);

This has no speed impact nor does it produce a "more correct" result, but it might improve readability a bit.

I haven't looked very closely whether there are similar issues elsewhere (it is relatively tedious for me to learn all this NEON stuff on the go, this is all new to me). If you're familiar with NEON, it might be worthwhile looking for similarly "correct but misleading" statements.

But then, the proof lies in the pudding, as they say, and the code is probably good enough as-is.

Ciao, Johannes