rocq/glibc/StrlenBits.v

The bit facts glibc's word-at-a-time strlen rests on (StrlenLogic.v, docs/glibc-ir.md).

glibc's __strlen loads whole 64-bit words and finds a zero byte in each with two masks, then the zero byte's index with a population count. Each fact is stated over byte_of, the model's little-endian byte i of a word:

byte_of_land, byte_of_lor, byte_of_lxor: bitwise ops work on each byte apart; byte_of_mod64 and byte_of_div: the model's wrap to 64 bits keeps the low eight bytes, and a shift right by whole bytes moves them down;
byte_of_add: a sum whose bytes do not carry adds byte by byte; byte_of_sub: a difference with no borrow below byte j subtracts byte by byte through byte j;
first_word_byte: the first word's mask marks exactly the zero bytes from the string's start, with 128 each;
loop_word_low: the loop's mask is 0 below the word's first zero byte and 128 at it;
tail_first: the population count of a mask whose bytes are 0 or 128 finds its first 128, each such mask computed.

Every claim about all bytes is reduced to one about a byte, and the byte claims are checked on all 256 bytes by computation.

From Stdlib Require Import ZArith Lia List Bool

From Nanofil Require Import Memory

Import ListNotations

Open Scope Z_scope

Bytes of a word

Bit n of byte i of x is bit 8i + n of x, for n below 8.

32Lemma byte_of_bits

∀ x i n

0 ≤ i

0 ≤ n

Z.testbitbyte_ofx i n = n <? 8 && Z.testbitx n + 8 × i

Proof 7 steps Qed

intros Hi Hn

unfold byte_of

change 256 with 2 ^ 8

rewrite Z.testbit_mod_pow2 by lia

rewrite <- Z.shiftr_div_pow2 by lia

rewrite Z.shiftr_spec by lia

reflexivity

A byte of a bitwise and is the and of the bytes.

41Lemma byte_of_land

∀ x y i

0 ≤ i

byte_ofZ.landx y i = Z.landbyte_ofx i byte_ofy i

Proof 5 steps Qed

intros Hi

apply Z.bits_inj'

intros n Hn

rewrite Z.land_spec , ! byte_of_bits , Z.land_spec by lia

destruct n <? 8 ; reflexivity

A byte of a bitwise or is the or of the bytes.

48Lemma byte_of_lor

∀ x y i

0 ≤ i

byte_ofZ.lorx y i = Z.lorbyte_ofx i byte_ofy i

Proof 5 steps Qed

intros Hi

apply Z.bits_inj'

intros n Hn

rewrite Z.lor_spec , ! byte_of_bits , Z.lor_spec by lia

destruct n <? 8 ; reflexivity

A byte of a bitwise xor is the xor of the bytes.

55Lemma byte_of_lxor

∀ x y i

0 ≤ i

byte_ofZ.lxorx y i = Z.lxorbyte_ofx i byte_ofy i

Proof 5 steps Qed

intros Hi

apply Z.bits_inj'

intros n Hn

rewrite Z.lxor_spec , ! byte_of_bits , Z.lxor_spec by lia

destruct n <? 8 ; reflexivity

The wrap to 64 bits keeps the low eight bytes.

62Lemma byte_of_mod64

∀ z i

0 ≤ i < 8

byte_ofz mod 2 ^ 64 i = byte_ofz i

Proof 8 steps Qed

intros Hi

apply Z.bits_inj'

intros n Hn

rewrite ! byte_of_bits , Z.testbit_mod_pow2 by lia

destruct n <? 8 eqn: E ; | reflexivity

apply Z.ltb_lt in E

replace n + 8 × i <? 64 with true by symmetry ; apply Z.ltb_lt ; lia

reflexivity

A shift right by k whole bytes moves byte i + k to byte i.

71Lemma byte_of_div

∀ z k i

0 ≤ k

0 ≤ i

byte_ofz / 2 ^ 8 × k i = byte_ofz i + k

Proof 6 steps Qed

intros Hk Hi

unfold byte_of

rewrite Z.div_div by apply Z.pow_nonzero || apply Z.pow_pos_nonneg ; lia

rewrite <- Z.pow_add_r by lia

do 3 f_equal

lia

A 64-bit word has no bytes above its eighth.

78Lemma byte_of_high

∀ z i

0 ≤ z < 2 ^ 64

8 ≤ i

byte_ofz i = 0

Proof 6 steps Qed

intros Hz Hi

unfold byte_of

rewrite Z.div_small ; reflexivity |

split ; lia |

apply Z.lt_le_trans_ 2 ^ 64 ; lia |

apply Z.pow_le_mono_r ; lia

A byte is in [0, 256).

85Lemma byte_of_range

∀ z i

0 ≤ byte_ofz i < 256

Proof 3 steps Qed

unfold byte_of

apply Z.mod_pos_bound

lia

The low n + 1 bytes are the low n bytes and byte n above them.

89Lemma low_step

∀ z n

0 ≤ n

z mod 2 ^ 8 × n + 1 = z mod 2 ^ 8 × n + 2 ^ 8 × n × byte_ofz n

Proof 4 steps Qed

intros Hn

replace 2 ^ 8 × n + 1 with 2 ^ 8 × n × 256 by rewrite Z.mul_add_distr_l , Z.pow_add_r by lia ; reflexivity

rewrite Z.rem_mul_r by lia || pose proof Z.pow_pos_nonneg2 8 × n ; lia

reflexivity

Sums and differences byte by byte

Where no byte pair of u and v sums past 255, no low part of them carries.

101Lemma add_low

∀ u v n

0 ≤ n ≤ 8

∀i, 0 ≤ i < 8 → byte_ofu i + byte_ofv i < 256

u mod 2 ^ 8 × n + v mod 2 ^ 8 × n < 2 ^ 8 × n

Proof 15 steps Qed

intros H₀ H₈ Hb

revert H8

pattern n

apply natlike_ind ; | | exact H0

–intros _

rewrite Z.mul_0_r , Z.pow_0_r , ! Z.mod_1_r

lia

–intros k Hk IH H₈

unfold Z.succ in *

rewrite ! low_step by lia

assert Hp : 0 < 2 ^ 8 × k by apply Z.pow_pos_nonneg ; lia

replace 2 ^ 8 × k + 1 with 2 ^ 8 × k × 256 by rewrite Z.mul_add_distr_l , Z.pow_add_r by lia ; reflexivity

specialize IHltac:lia

specialize Hbk ltac:lia

nia

A byte of a sum with no carries is the sum of the bytes.

115Lemma byte_of_add

∀ u v i

∀i, 0 ≤ i < 8 → byte_ofu i + byte_ofv i < 256

0 ≤ i < 8

byte_ofu + v i = byte_ofu i + byte_ofv i

Proof 21 steps Qed

intros Hb Hi

pose proof add_lowu v i ltac:lia Hb as Hl

assert Hp : 0 < 2 ^ 8 × i by apply Z.pow_pos_nonneg ; lia

assert E : u + v / 2 ^ 8 × i = u / 2 ^ 8 × i + v / 2 ^ 8 × i

{symmetry

apply Z.div_unique with r := u mod 2 ^ 8 × i + v mod 2 ^ 8 × i

–left

pose proof Z.mod_pos_boundu 2 ^ 8 × i Hp

pose proof Z.mod_pos_boundv 2 ^ 8 × i Hp

lia

–pose proof Z.div_modu 2 ^ 8 × i ltac:lia

pose proof Z.div_modv 2 ^ 8 × i ltac:lia

lia

unfold byte_of at 1

rewrite E , Z.add_mod by lia

fold byte_ofu i byte_ofv i

apply Z.mod_small

pose proof byte_of_rangeu i

pose proof byte_of_rangev i

specialize Hbi Hi

lia

Where c's bytes below j are at most x's, no low part of x - c through byte j borrows.

131Lemma sub_low

∀ x c j n

0 ≤ n ≤ j

j ≤ 8

∀i, 0 ≤ i < j → byte_ofc i ≤ byte_ofx i

c mod 2 ^ 8 × n ≤ x mod 2 ^ 8 × n

Proof 14 steps Qed

intros H₀ Hj H₈ Hb

revert Hj

pattern n

apply natlike_ind ; | | exact H0

–intros _

rewrite Z.mul_0_r , Z.pow_0_r , ! Z.mod_1_r

lia

–intros k Hk IH Hj

unfold Z.succ in *

rewrite ! low_step by lia

assert Hp : 0 < 2 ^ 8 × k by apply Z.pow_pos_nonneg ; lia

specialize IHltac:lia

specialize Hbk ltac:lia

nia

A byte i at or below j of x - c, where c's bytes below j are at most x's, is the difference of the bytes, wrapped to a byte.

144Lemma byte_of_sub

∀ x c j i

j ≤ 8

∀i, 0 ≤ i < j → byte_ofc i ≤ byte_ofx i

0 ≤ i ≤ j

byte_ofx − c i = byte_ofx i − byte_ofc i mod 256

Proof 16 steps Qed

intros H₈ Hb Hi

pose proof sub_lowx c j i ltac:lia H8 Hb as Hl

assert Hp : 0 < 2 ^ 8 × i by apply Z.pow_pos_nonneg ; lia

assert E : x − c / 2 ^ 8 × i = x / 2 ^ 8 × i − c / 2 ^ 8 × i

{symmetry

apply Z.div_unique with r := x mod 2 ^ 8 × i − c mod 2 ^ 8 × i

–left

pose proof Z.mod_pos_boundx 2 ^ 8 × i Hp

pose proof Z.mod_pos_boundc 2 ^ 8 × i Hp

lia

–pose proof Z.div_modx 2 ^ 8 × i ltac:lia

pose proof Z.div_modc 2 ^ 8 × i ltac:lia

lia

unfold byte_of at 1

rewrite E , Zminus_mod

reflexivity

A word from its bytes

The little-endian integer of the bytes cs.

160Fixpoint of_bytescs : listZ : Z ≔

match cs with

[ ]

⇒

c :: cs

⇒

c + 256 × of_bytescs

The eight byte indices of a word.

164Definition idx8: listZ ≔

0; 1; 2; 3; 4; 5; 6; 7

A 64-bit word is the integer of its eight bytes.

167Lemma of_bytes_byte_of

∀ z

0 ≤ z < 2 ^ 64

of_bytesmapbyte_ofz idx8 = z

Proof 20 steps Qed

intros Hz

transitivity z mod 2 ^ 8 × 7 + 1 ; | apply Z.mod_small ; exact Hz

rewrite low_step by lia

change 8 × 7 with 8 × 6 + 1

rewrite low_step by lia

change 8 × 6 with 8 × 5 + 1

rewrite low_step by lia

change 8 × 5 with 8 × 4 + 1

rewrite low_step by lia

change 8 × 4 with 8 × 3 + 1

rewrite low_step by lia

change 8 × 3 with 8 × 2 + 1

rewrite low_step by lia

change 8 × 2 with 8 × 1 + 1

rewrite low_step by lia

change 8 × 1 with 8 × 0 + 1

rewrite low_step by lia

rewrite Z.mul_0_r , Z.pow_0_r , Z.mod_1_r

cbn [ of_bytes map idx8 ]

lia

Each of the eight byte indices is one of idx8's.

181Lemma idx8_cases

∀ i

0 ≤ i < 8

Ini idx8

Proof 3 steps Qed

intros Hi

cbn

lia

Byte i of a constant, for each i below 8, by computing it.

185Ltac byte_cases i ≔

let H ≔ fresh in assert H : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7 by lia ; repeat destruct H as H | H ; subst i

A property of bytes, checked by computing it on all 256.

191Lemma all_bytes

∀ P : Z → bool b

forallbP mapZ.of_nat seq0 256 = true

0 ≤ b < 256

Pb = true

Proof 8 steps Qed

intros H b Hb

rewrite forallb_forall in H

apply H

apply in_map_iff

exists Z.to_natb

split ; lia |

apply in_seq

lia

The masks

0x7f in every byte.

201Definition ones7: Z ≔

9187201950435737471

0x80 in every byte.

203Definition highs: Z ≔

9259542123273814144

0x01 in every byte.

205Definition lows: Z ≔

72340172838076673

All 64 bits.

207Definition all64: Z ≔

18446744073709551615

The bytes of 0x7f in every byte.

210Lemma byte_ones7

∀ i

0 ≤ i < 8

byte_ofones7 i = 127

Proof 2 steps Qed

intros Hi

byte_cases i ; reflexivity

The bytes of 0x80 in every byte.

213Lemma byte_highs

∀ i

0 ≤ i < 8

byte_ofhighs i = 128

Proof 2 steps Qed

intros Hi

byte_cases i ; reflexivity

The bytes of 0x01 in every byte.

216Lemma byte_lows

∀ i

0 ≤ i < 8

byte_oflows i = 1

Proof 2 steps Qed

intros Hi

byte_cases i ; reflexivity

The bytes of all 64 bits.

219Lemma byte_all64

∀ i

0 ≤ i < 8

byte_ofall64 i = 255

Proof 2 steps Qed

intros Hi

byte_cases i ; reflexivity

glibc's find_zero_all (string-fza.h) on the first word x, as nanofil's IR computes it, every read wrapped to 64 bits: 128 in each zero byte of x, 0 in each other.

225Definition first_maskx : Z : Z ≔

Z.lxorZ.lorZ.lorZ.landx mod 2 ^ 64 ones7 mod 2 ^ 64 + ones7 mod 2 ^ 64 mod 2 ^ 64 x mod 2 ^ 64 mod 2 ^ 64 ones7 mod 2 ^ 64 all64

The first mask's byte, on one byte.

232Lemma first_mask_on_byte

∀ b

0 ≤ b < 256

Z.lxorZ.lorZ.lorZ.landb 127 + 127 b 127 255

b =? 0

→

128

else

Proof 3 steps Qed

intros Hb

apply Z.eqb_eq

apply all_bytesλb ⇒ Z.lxorZ.lorZ.lorZ.landb 127 + 127 b 127 255 =? if b =? 0 then 128 else 0 ; vm_compute ; reflexivity | exact Hb

A byte's low seven bits are at most 127.

241Lemma land127

∀ b

0 ≤ b < 256

0 ≤ Z.landb 127 ≤ 127

Proof 4 steps Qed

intros Hb

pose proof all_bytesλb ⇒ 0 ≤? Z.landb 127 && Z.landb 127 ≤? 127 ltac:vm_compute ; reflexivity b Hb as H

apply andb_true_iff in H as H₁ H₂

lia

Byte i of the first mask is 128 if byte i of x is zero, else 0.

248Lemma first_mask_byte

∀ x i

0 ≤ i < 8

byte_offirst_maskx i

byte_ofx i =? 0

→

128

else

Proof 6 steps Qed

intros Hi

unfold first_mask

repeat rewrite ?byte_of_mod₆₄ , ?byte_of_lxor , ?byte_of_lor , ?byte_all₆₄ , ?byte_ones₇ by lia

rewrite byte_of_add by lia || intros j Hj ; rewrite byte_of_mod64 , byte_of_land , byte_of_mod64 , byte_ones7 by lia ; pose proof land127byte_ofx j byte_of_rangex j ; lia

rewrite byte_of_mod64 , byte_of_land , byte_of_mod64 , byte_ones7 by lia

apply first_mask_on_byte , byte_of_range

glibc's find_zero_low (string-fzb.h) on a loop word x, as nanofil's IR computes it: (x - 0x01...) & ~x & 0x80..., every read wrapped. Exact below x's first zero byte, and 128 at it.

262Definition loop_maskx : Z : Z ≔

Z.landZ.landx mod 2 ^ 64 − lows mod 2 ^ 64 mod 2 ^ 64 Z.lxorx mod 2 ^ 64 all64 mod 2 ^ 64 mod 2 ^ 64 highs

The loop mask's byte, on one nonzero byte: 0.

269Lemma loop_mask_on_byte

∀ b

0 < b < 256

Z.landZ.landb − 1 mod 256 Z.lxorb 255 128 = 0

Proof 4 steps Qed

intros Hb

apply Z.eqb_eq

pose proof all_bytesλb ⇒ b =? 0 || Z.landZ.landb − 1 mod 256 Z.lxorb 255 128 =? 0 ltac:vm_compute ; reflexivity b ltac:lia as H

apply orb_true_iff in H as H | H ; apply Z.eqb_eq in H ; lia | exact H

Byte i at or below j of the loop mask, where x's bytes below j are nonzero: the loop mask's byte of x's byte i, with no borrow.

279Lemma loop_mask_byte'

∀ x j i

j ≤ 8

∀i, 0 ≤ i < j → byte_ofx i ≠ 0

0 ≤ i ≤ j

i < 8

byte_ofloop_maskx i = Z.landZ.landbyte_ofx i − 1 mod 256 Z.lxorbyte_ofx i 255 128

Proof 11 steps Qed

intros Hj Hnz Hi H₈

unfold loop_mask

rewrite byte_of_land , byte_highs , ! byte_of_mod64 , byte_of_land , ! byte_of_mod64 , byte_of_lxor , byte_of_mod64 , byte_all64 by lia

rewrite byte_of_sub_ _ j i Hj ; | | lia

–rewrite byte_lows , byte_of_mod64 by lia

reflexivity

–intros k Hk

rewrite byte_lows , byte_of_mod64 by lia

pose proof byte_of_rangex k

specialize Hnzk Hk

lia

Below x's first zero byte j, the loop mask's bytes are 0.

292Lemma loop_mask_below

∀ x j i

j ≤ 8

∀i, 0 ≤ i < j → byte_ofx i ≠ 0

0 ≤ i < j

byte_ofloop_maskx i = 0

Proof 6 steps Qed

intros Hj Hnz Hi

rewrite loop_mask_byte'x j i Hj Hnz by lia

apply loop_mask_on_byte

pose proof byte_of_rangex i

specialize Hnzi Hi

lia

At x's first zero byte j, the loop mask's byte is 128.

300Lemma loop_mask_at

∀ x j

0 ≤ j < 8

∀i, 0 ≤ i < j → byte_ofx i ≠ 0

byte_ofx j = 0

byte_ofloop_maskx j = 128

Proof 4 steps Qed

intros Hj Hnz Hz

rewrite loop_mask_byte'x j j ltac:lia Hnz by lia

rewrite Hz

reflexivity

Every byte of the loop mask is 0 or 128.

305Lemma loop_mask_01

∀ x i

0 ≤ i < 8

byte_ofloop_maskx i = 0 ∨ byte_ofloop_maskx i = 128

Proof 5 steps Qed

intros Hi

unfold loop_mask

rewrite byte_of_land , byte_highs by lia

match goal with|- context [Z.landbyte_of?y i 128]⇒pose proof all_bytesλb ⇒ Z.landb 128 =? 0 || Z.landb 128 =? 128 ltac:vm_compute ; reflexivity byte_ofy i byte_of_rangey i as Hend

apply orb_true_iff in H as H | H ; apply Z.eqb_eq in H ; auto

Words in range

A word in range has no bits from 64 up.

317Lemma bits64

∀ z n

0 ≤ z < 2 ^ 64

64 ≤ n

Z.testbitz n = false

Proof 4 steps Qed

intros Hz Hn

rewrite <- Z.mod_smallz 2 ^ 64 by lia

apply Z.mod_pow2_bits_high

lia

An and of words in range is in range.

321Lemma land_range

∀ a b

0 ≤ a < 2 ^ 64

0 ≤ b < 2 ^ 64

0 ≤ Z.landa b < 2 ^ 64

Proof 12 steps Qed

intros Ha Hb

assert E : Z.landa b mod 2 ^ 64 = Z.landa b

{apply Z.bits_inj'

intros n Hn

rewrite Z.testbit_mod_pow2 , Z.land_spec by lia

destruct n <? 64 eqn: E ; reflexivity |

apply Z.ltb_ge in E

rewrite bits64a n Ha E

reflexivity

rewrite <- E

apply Z.mod_pos_bound

lia

A word in range whose bytes are all 0 is 0.

330Lemma zero_word

∀ z

0 ≤ z < 2 ^ 64

∀i, 0 ≤ i < 8 → byte_ofz i = 0

z = 0

Proof 5 steps Qed

intros Hz H

rewrite <- of_bytes_byte_ofz Hz

cbn [ map idx8 ]

rewrite ! H by lia

reflexivity

The population count

glibc's index_first (string-fzi.h) as nanofil inlines it on the mask r: the population count of the bits below r's lowest set bit, (r & -r) - 1, every read wrapped.

341Definition tailr : Z : Z ≔

let v₈ ≔ −r mod 2 ^ 64 mod 2 ^ 64 in

let v₉ ≔ Z.landr mod 2 ^ 64 v₈ mod 2 ^ 64 in

let v₁₀ ≔ v₉ mod 2 ^ 64 − 1 mod 2 ^ 64 in

let v₁₁ ≔ v₁₀ mod 2 ^ 64 / 2 ^ 1 mod 64 in

let v₁₂ ≔ Z.landv₁₁ mod 2 ^ 64 6148914691236517205 in

let v₁₃ ≔ v₁₀ mod 2 ^ 64 − v₁₂ mod 2 ^ 64 mod 2 ^ 64 in

let v₁₄ ≔ Z.landv₁₃ mod 2 ^ 64 3689348814741910323 in

let v₁₅ ≔ v₁₃ mod 2 ^ 64 / 2 ^ 2 mod 64 in

let v₁₆ ≔ Z.landv₁₅ mod 2 ^ 64 3689348814741910323 in

let v₁₇ ≔ v₁₄ mod 2 ^ 64 + v₁₆ mod 2 ^ 64 mod 2 ^ 64 in

let v₁₈ ≔ v₁₇ mod 2 ^ 64 / 2 ^ 4 mod 64 in

let v₁₉ ≔ v₁₇ mod 2 ^ 64 + v₁₈ mod 2 ^ 64 mod 2 ^ 64 in

let v₂₀ ≔ Z.landv₁₉ mod 2 ^ 64 1085102592571150095 in

let v₂₁ ≔ v₂₀ mod 2 ^ 64 × 72340172838076673 mod 2 ^ 64 in

v₂₁ mod 2 ^ 64 / 2 ^ 56 mod 64

On a mask in range whose bytes are 0 or 128, with the first 128 at byte j: the count is 8j + 7, so its eighth is j. Each of the 255 masks with a first 128 at some byte is computed.

361Lemma tail_first

∀ r j

0 ≤ r < 2 ^ 64

∀i, 0 ≤ i < 8 → byte_ofr i = 0 ∨ byte_ofr i = 128

0 ≤ j < 8

byte_ofr j = 128

∀i, 0 ≤ i < j → byte_ofr i = 0

tailr = 8 × j + 7

Proof 4 steps Qed

intros Hr H₀₁ Hj Hjb Hlow

rewrite <- of_bytes_byte_ofr Hr

cbn [ map idx8 ]

byte_cases j;repeat match goal with|- context [byte_ofr ?i]⇒first rewrite Hlowi by lia | rewrite Hjb | let E ≔ fresh in destruct H01i ltac:lia as E | E ; rewrite Eend;vm_compute;reflexivity

The first word, from the string's start

The first word's mask shifted right by the string's offset k in its word, k * 8 bits, as nanofil's IR computes it from the address a: the zero bytes of x from byte k on, moved down to byte 0.

381Definition first_shiftx a : Z : Z ≔

first_maskx mod 2 ^ 64 / 2 ^ Z.landa mod 2 ^ 64 7 mod 2 ^ 64 × 8 mod 2 ^ 64 mod 2 ^ 32 mod 64

The shift is the offset of a in its word, in bytes.

385Lemma first_shift_amount

∀ a

0 ≤ a

Z.landa mod 2 ^ 64 7 mod 2 ^ 64 × 8 mod 2 ^ 64 mod 2 ^ 32 mod 64 = 8 × a mod 8

Proof 8 steps Qed

intros Ha

change 7 with Z.ones3

rewrite Z.land_ones by lia

change 2 ^ 3 with 8

assert E : a mod 2 ^ 64 mod 8 = a mod 8 by rewrite <- Znumtheory.Zmod_div_mod ; reflexivity | lia | lia | exists 2 ^ 61 ; reflexivity

rewrite E

pose proof Z.mod_pos_bounda 8 ltac:lia

rewrite Z.mod_smalla mod 8 , Z.mod_smalla mod 8 × 8 , Z.mod_smalla mod 8 × 8 , Z.mod_small ; lia

Byte i of the shifted mask: 128 where byte i + k of x is zero, for i + k inside the word, else 0.

398Lemma first_shift_byte

∀ x a i

0 ≤ a

0 ≤ i

byte_offirst_shiftx a i

i + a mod 8 <? 8

→

byte_ofx i + a mod 8 =? 0

→

128

else

Proof 10 steps Qed

intros Ha Hi

pose proof Z.mod_pos_bounda 8 ltac:lia

unfold first_shift

rewrite first_shift_amount , byte_of_div by lia

destruct i + a mod 8 <? 8 eqn: E

–apply Z.ltb_lt in E

rewrite byte_of_mod64 , first_mask_byte by lia

reflexivity

–apply Z.ltb_ge in E

apply byte_of_high ; apply Z.mod_pos_bound ; lia | exact E

The shifted mask is in range.

410Lemma first_shift_range

∀ x a

0 ≤ first_shiftx a < 2 ^ 64

Proof 6 steps Qed

unfold first_shift

pose proof Z.mod_pos_boundfirst_maskx 2 ^ 64 ltac:lia

match goal with|- context [_ / 2 ^ ?e]⇒assert 0 < 2 ^ e by apply Z.pow_pos_nonneg ; lia | apply Z.mod_pos_bound ; liaend

split ; apply Z.div_pos ; lia |

apply Z.le_lt_trans_ first_maskx mod 2 ^ 64 ; | lia

apply Z.div_le_upper_bound ; nia

The loop mask is in range.

420Lemma loop_mask_range

∀ x

0 ≤ loop_maskx < 2 ^ 64

Proof 2 steps Qed

unfold loop_mask

apply land_range ; apply Z.mod_pos_bound ; lia | vm_compute ; split ; congruence

Rounding a 64-bit address down to its word, as nanofil's IR does it: an and with ~7.

425Lemma land_align

∀ a

0 ≤ a < 2 ^ 64

Z.landa 18446744073709551608 mod 2 ^ 64 = a − a mod 8

Proof 20 steps Qed

intros Ha

change 18446744073709551608 mod 2 ^ 64 with Z.lxorZ.ones64 Z.ones3

assert E : Z.landa Z.lxorZ.ones64 Z.ones3 + Z.landa Z.ones3 = a

{rewrite Z.add_nocarry_lxor

–apply Z.bits_inj'

intros n Hn

rewrite Z.lxor_spec , ! Z.land_spec , Z.lxor_spec , ! Z.testbit_ones by lia

rewrite proj2Z.leb_le0 n Hn

destruct Z.testbita n eqn: E ; | reflexivity

destruct Z.ltb_specn 3 , Z.ltb_specn 64 ; cbn ; try reflexivity ; try lia

rewrite bits64a n Ha ltac:lia in E

discriminate

–apply Z.bits_inj'

intros n Hn

rewrite Z.bits_0 , ! Z.land_spec , Z.lxor_spec , ! Z.testbit_ones by lia

rewrite proj2Z.leb_le0 n Hn

destruct Z.testbita n , Z.ltb_specn 3 , Z.ltb_specn 64 ; cbn ; try reflexivity ; lia

rewrite Z.land_ones in E by lia

change 2 ^ 3 with 8 in E

lia