search

tamarin-prover / manual

Tamarin prover manual: source files
https://tamarin-prover.github.io/manual
24 stars 39 forks source link

Document 'Using an Oracle' with more technical details #82

Closed felixlinker closed 2 years ago

felixlinker commented 2 years ago

I hope my understanding is correct! Please point out any mistake I made. Maybe, I should note what happens if no order is given by the oracle? I guess, the default strategy is applied then.

rsasse commented 2 years ago

Cool! If you could indeed add that this only allows a reordering, and that partial list of indices is allowed, meaning for 4 goals the oracle can answer "4,2", which will result in the actual order 4,2,1,3, as all "unchosen" goals are appended in initial order. This clarifies that if no order is given by oracle, the default one that was output is actually used.

edited: To add to this, it is not actually a manual reordering of all goals, but a template/strategy encoded for reordering, modifying the default heuristic that way. It would often be extremely tedious to encode all steps (just store the proof), and it is more stable for rerunning a proof than that, but does of course have the risk of breaking on major updates.

felixlinker commented 2 years ago

Addressed :) Thanks for the explanation!

rsasse commented 2 years ago

Content looks good! Thank you. 👍

Does anyone know what that failing deploy preview check is? Can we merge this anyway?

rkunnema commented 2 years ago

Does anyone know what that failing deploy preview check is? Can we merge this anyway?

No idea, but I vote for merging anyway.

felixlinker commented 2 years ago

Hey hey! Anything blocking this? We have a student who needs to implement an oracle. It would be great to have a piece of documentation for them.

cascremers commented 2 years ago

I looks like the manual deploy scripts are failing, and need updating. This has nothing to do with this particular PR and is a general thing.

Merging now, and then will try to address the deploy later. This does mean that accepting the PR may not lead to an updated manual PDF on the website.