fix: Add constraint to SHA extension that checks if the appended length is a multiple of 8

[Avaneesh-axiom]

We have a bug where the message length (in bits) that is appended to the message as part of the SHA-256 padding algorithm is not constrained to be a multiple of 8 (and hence being a length in bytes) but rather to be a multiple of 4 here. But we assume that it is a multiple of 8 in another constraint here.

The fix is to correctly constrain that the appended length is a multiple of 8. Since the length is stored in little endian, we check that it's first three bits are zero.

Closes INT-3600

[github-actions]

group	app.proof_time_ms	app.cycles	app.cells_used	leaf.proof_time_ms	leaf.cycles	leaf.cells_used
verify_fibair	(-55 [-3.8%]) 1,393	147,020	8,194,664	-	-	-
fibonacci_program	(+40 [+0.8%]) 5,032	1,500,096	51,485,167	-	-	-
regex_program	(-31 [-0.2%]) 13,982	4,140,164	167,389,450	-	-	-
ecrecover_program	(+10 [+0.4%]) 2,519	295,181	15,586,346	-	-	-

Commit: ba51eb9

Benchmark Workflow

[jonathanpwang]

LGTM