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