proposition: Lemma sem_sub_pp_total_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)) (space_start s)) = if Archi.ptr64 then Vlong (Int64.repr (total_space s)) else Vint (Int.repr (total_space s)).
proof: Proof. intros. destruct (space_start s); try contradiction. simpl. destruct (eq_block b b). 2: exfalso; apply n; reflexivity. unfold sem_sub_pp; destruct eq_block; [|easy]. inv_int i. rewrite ptrofs_add_repr, ptrofs_sub_repr. replace (ofs + WORD_SIZE * total_space s - ofs) with (WORD_SIZE * total_space s)%Z by lia. simpl. pose proof (total_space_signed_range s). unfold Ptrofs.divs. rewrite !Ptrofs.signed_repr by rep_lia. rewrite Vptrofs_unfold_true, 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)