dominique-unruh/qrhl-tool

Proof assistant for qRHL

Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically for quantum and post-quantum security proofs.

• Installation – how to install
• Web page – for more information

Acknowledgments

Development was supported by the Air Force Office of Scientific Research (AOARD Grant FA2386-17-1-4022), by the ERC consolidator grant CerQuS (819317), and by the PRG946 grant from the Estonian Research Council.

qrhl-tool's Issues

Exceptions in theories should always be raised directly when loading theory

Due to Isabelle's futures etc, error can be hidden in isabelle ... command

The following has an error only in rule test2

isabelle TestEx.

lemma x.
rule test2.

theory TestEx
  imports QRHL.QRHL
begin

definition "x == True"

lemma test2: x
      by auto (* FAILS *)


end

Support local variables in programs

Document ISABELLE command

Error while installing on MacOS

The following error appears when I install QRHL on MacOS. It seems that the package only works with Linux, not Darwin.
Thank you very much for considering this issue.

Support multiple wp in one

Example: wp left 5 right 6.

Support for subscript/superscript in Isabelle terms

Currently, sub/superscript letters are rendered like this: x⇧2.

• Render them properly
• Read properly rendered sub/superscript letters back
• Add input method support for entering sub/superscript

Binary installation documentation bugs

I just managed to get qrhl-tool running. In doing so, I ran into a couple of issues with the installation instructions in README.md.

First, the github downloads directory does not seem to have a binary development snapshot as the README suggests. I succeeded at installing qrhl-0.6.zip using Isabelle 2019.

Second, the README claims that the path to AFP should be set in qrhl-tool.conf as afp-home, but this results in AFP not being found. It seems to need to be set as afp-root instead.

Document focusing in manual

Document focusing subgoals with {, }, +, etc.

Theories should be loaded with quick_and_dirty mode

Currently, if we have isabelle X in the qrhl file, then X.thy is executed in quick_and_dirty mode, but if X imports Y, then Y.thy is executed with quick_and_dirty = false.

Have qrhl-tool.conf in a per-user dir, in /etc, in current dir

Use only Isabelle-special subscript symbols in output (otherwise copy&paste to jEdit may not work)

Update terse teleportation proof in manual (does not use isa thy anymore)

Get rid of "head of empty list" exception

In dominique-unruh/compressed-oracle-formalization@5a802547b0a129a17a758d7876b46034cf5ec9d8

Replace by proper error message.


Update `symbols` table

Use the table from Isabelle2021-1 once released.

When theory file changes, automatically retract in proofgeneral

Currently just issues a warning.
Instead, it might automatically retract (together with a message why).
Or even better, retract and rerun to current point?

Exceptions should be rendered prettily

At least Par_Exn [CONTEXT (<context>, ERROR "Failed to apply initial proof method <markup>:\n<markup>")]

See the example code from #6 which raises this exception.

Documentation updates

• qrhl-tool.conf not searched for in current directory
• no options session-dir, session in config
• directory of isabelle command is session dir
• isabelle command syntax [session]

Enable ket-syntax described in the manual

Recreate proofgeneral.bat or explain different approach to run PG on Windows

Methods that does wp, skip, rnd, simp automatically

Rough algo:

• For assignments, do wp.
• For <$ on both sides with everything the same, do rnd.
• For identical call on both sides, to equal.
• For skip on both sides, do skip.
• For result of skip, do simp (with the lemmas that are given to the method)
• Repeat till it doesn't work.

Phase out overloaded syntaxes

• $\cdot$ for operator applications
• $\otimes$ for tensor product (also unify tensorOp and tensor_op)
• $&gt;&gt;$ only for operators (at least document the =q variant
• Input method syntax for those
• Document

Procedure calls with parameters

Depends on #11 probably

When opening a .qrhl file in a different directory, ProofGeneral should inform qrhl-tool

Update example files (document, make more useful) where needed

`bin/qrhl` should finish in success case with something nicer than `EOF`

When an error happens in replay, adjust error message to say so more clearly

Also suggest to revert or rewind.

Isabelle theories should be reloaded when they change

Currently, qrhl-tool notices when they change and asks Isabelle for the theory again, but apparently this does not trigger a re-reading of the theory.

In rule-tactic, don't dump large raw error on user

Print Isabelle exceptions including extra arguments

E.g., if TERM ("text", terms) is raised, then text is printed when the exception is forwarded to qrhl-tool, but terms are not printed.
In contrast, in jEdit, those arguments are always printed, so there is a way to translate such exceptions to text!

Tool should recognize if dependent theory changes

E.g., if we load isabelle Test and Test.thy loads Bla.thy and blubb.ML, then a change in those should also lead to a warning about changed files. (But files included in the QRHL session should not.)

Adapt TeX input method

The TeX input method should have nicer keystrokes for some symbols (e.g. \frqq, or quantum equality, or [[).
Also, it should not interpret _ to create a small letter.

Include git revision in qrhl-tool startup output (even without debug logging)

Allow program variables that are non ASCII

Integrate qrhl-tool support in upstream proofgeneral

• Get it integrated
• Document how to use it

QRHL 0.5 is not working on my Ubuntu VPS

I hope you can consider the following error that occurs while I try to build Isabelle on VPS

• Ubuntu 20.04 and Java 11.
  

Thank you so much in advanced!

Printing/parsing ambiguity

On Isabelle level: both (A *⇩S B) ⊓ C and A *⇩S (B ⊓ C) print as A *⇩S B ⊓ C which fails to parse.


Document `frame` tactic in manual

Search for qrhl-tool.conf in the "intended" current dir

E.g., if we run run-isabelle.sh path/X.thy or qrhl path/x.qrhl, path should be seen as the current directory.

In manual, check if the examples use old syntax

Add ! to isa-tactic.

Same behavior as with simp!.


Check if pqfo still works

qrhl-tool should check whether a sufficiently new AFP version is used

Allow loading of different session than QRHL.QRHL

bin/qrhl should abort on error

Currently, bin/qrhl file.qrhl, if there is an error in file.qrhl, will throw an exception and then wait forever.
It should return with nonzero return code instead.

make qrhl.zip does not include */fake-session-dir/*

At least on f97188c

This makes the qrhl.zip unusable.

Update manual

Read manual and see what updates are needed

Fix syntactic sugar in goal-state-display

For example:
probability (expression 〚var_b〛 (λb. b = 1)) enc_fixed rho = probability (expression 〚var_b〛 (λb. b = 1)) random rho
should be
Pr[b=1 : enc_fixed(rho)] = Pr[b=1: random(rho)]

Choose better name for ISABELLE command

Update example files to various new constant syntaxes

Change notation \otimes_s -> \otimes_l