Closed andrew-appel closed 2 months ago
In case we want to do the latter (get change_compspecs
to handle cstring
), here's the code to do it:
Lemma change_compspecs_cstring: forall cs1 cs2: compspecs, (* put this in Floyd *)
@cstring cs1 = @cstring cs2.
Proof.
intros.
extensionality sh s p.
unfold cstring.
f_equal.
set (u := map _ _). clearbody u.
set (n := Zlength _ + _). clearbody n.
unfold data_at.
unfold field_at.
f_equal.
f_equal.
unfold field_compatible.
f_equal; auto.
f_equal; auto.
f_equal; auto.
f_equal; auto.
unfold align_compatible.
destruct p; simpl; auto.
apply prop_ext; split; intro;
(apply align_compatible_rec_Tarray; intros j ?;
apply align_compatible_rec_Tarray_inv with (i:=j) in H; auto;
inv H; econstructor; eauto).
Qed.
Ltac forward.change_compspecs cs :=
match goal with
| |- context [ ?cs' ] =>
match type of cs' with
| compspecs =>
try (constr_eq cs cs'; fail 1);
first [rewrite !(change_compspecs_cstring cs' cs) (* new! *)
| change_compspecs' cs' cs];
repeat change_compspecs' cs cs'
end
end.
I believe this is a more general issue (and somewhat related to the fact that computational aspects of compspecs are built into floyd rather early), so it would be good if a solution with a minimal (or perhaps even better: arbitrary but not automatically instantiated) compspecs could be realized.
. . . because it doesn't use any struct or union fields, so its internal
data_at
s can use a trivial compspecs. This will help with function calls from one compilation unit to another.The alternative is to leave the compspecs argument of cstring, but instrument the
change_compspecs
tactic to handle cstring.