proposition: Lemma sem_sub_pp_rest_space: forall s, isptr (space_start s) -> force_val (sem_sub_pp int_or_ptr_type (offset_val (WORD_SIZE * total_space s) (space_start s)) (offset_val (WORD_SIZE * used_space s) (space_start s))) = if Archi.ptr64 then Vlong (Int64.repr (total_space s - used_space s)) else Vint (Int.repr (total_space s - used_space s)).
proof: Proof. intros. destruct (space_start s); try contradiction. simpl. destruct (eq_block b b). 2: exfalso; apply n; reflexivity. inv_int i. unfold sem_sub_pp; destruct eq_block; [|easy]. rewrite !ptrofs_add_repr, ptrofs_sub_repr. replace (ofs + WORD_SIZE * total_space s - (ofs + WORD_SIZE * used_space s)) with (WORD_SIZE * (total_space s - used_space s))%Z by (rewrite Z.mul_sub_distr_l; lia). simpl. pose proof (rest_space_signed_range s). rewrite <- Z.mul_sub_distr_l in H0. rewrite Vptrofs_unfold_true by reflexivity. unfold Ptrofs.divs. rewrite !Ptrofs.signed_repr by rep_lia. rewrite ptrofs_to_int64_repr by reflexivity. do 2 f_equal. unfold WORD_SIZE. rewrite Z.mul_comm, Z.quot_mul by lia. auto. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)