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
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
