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 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