Formal proof with the Coq theorem prover of the correctness of an oracle algorithm for offline analysis of distributed logs against interaction models