seL4 Developers:
Consider the following c structure declarations:
struct foo_struct{ uint16_t subfield; };
struct bar_struct{ struct foo foo;
};
I am wondering if anyone has any suggestions on how I might go about proving something like this:
s[Ptr &(bar→[''foo_C'']) := subfield_C_update (λ_. b) (heap_MissionCommand_struct_C s (Ptr &(bar→[''foo_C''])))] = s[Ptr &(bar→[''missioncommand_C''])→subfield := b]
where s of type lifted_globals, bar is of type foo_struct_C, and b is of type word16.
I *think* it should be provable, i.e., "updating all of the foo field with a copy of what was there originally modulo some change to subfield is equivalent to making that change directly to the subfield."
I apologize in for taking this "into the weeds" but some of the definitions being used are buried in the AutoCorres translation and I am unsure how to make my question more abstract.
Thanks in Advance! Dan DaCosta