proposition: Lemma int_ltu_ptrofs_to_int: forall x y, Archi.ptr64 = false -> Int.ltu (Ptrofs.to_int x) (Ptrofs.to_int y) = Ptrofs.ltu x y.
proof: Proof. intros. unfold Int.ltu, Ptrofs.ltu. rewrite <- (Ptrofs.repr_unsigned x), <- (Ptrofs.repr_unsigned y). rewrite !ptrofs_to_int_repr by auto. pose proof Ptrofs.unsigned_range. unfold Ptrofs.max_unsigned in H0. unfold Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize in H0. rewrite H in H0. change (two_power_nat 32) with (Int.max_unsigned + 1) in H0. rewrite !Int.unsigned_repr. 2: specialize (H0 y); lia. 2: specialize (H0 x); lia. rewrite !Ptrofs.unsigned_repr by rep_lia. auto. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)