The new bane of my existence, uncommented Coq code.
Axiom ef_deterministic_fun:
forall ef,
ef_deterministic ef = true ->
forall ge args m t1 t2 vres1 vres2 m1 m2,
Events.external_call ef ge args m t1 vres1 m1 ->
Events.external_call ef ge args m t2 vres2 m2 ->
(vres1,t1,m1) = (vres2,t2,m2).
Gee thanks... Not only is one of the most conceptually complex languages mankind has come up with, it has that single letter fetishism that mathematicians tend to have.
From here
https://github.com/PrincetonUniversity/VST
What I can guess is that:
ef_deterministic_fun is a rule for external functions that are deterministic to tell if they are equivalent. This is for software that is used to formally prove that C programs are doing what we think they are.
Not sure why 'fun' is added at the end. It is common shorthand for function. But anyway, next bit:
This is the function ef, if this boolean function comes back true, these other conditions are true.
Definition ef_deterministic (ef: external_function) : bool :=
match ef with
| EF_external name sg => false
| EF_builtin name sg => true
| EF_runtime name sg => false
| EF_vload chunk => false
| EF_vstore chunk => false
| EF_malloc => true
| EF_free => true
| EF_memcpy sz al => true
| EF_annot kind text targs => true
| EF_annot_val kind Text rg => true
| EF_inline_asm text sg clob => false
| EF_debug kind text targs => true
end.
- What is 'ge'? Global environment?
- args are probably arguments
- m, m1, m2 are a mystery, I am guessing either a stack or a heap
- t1, t2 maybe stack or heap
- vres maybe a command of some sort
Thankfully Inria people are better at things. Probably because they are selling the C compiler, and can have professionals instead of students.
ef external function
ge global environment?
args to the function
m for memory state before call
t1?
vres is result value
m1 for memory state after call
