Mechanise Theorem 4 (delimited release for declassify) in Agda#8
Merged
Merged
Conversation
Machine-checks lambda_if Theorem 4 (relaxed noninterference / delimited release, docs/semantics.md Section 9.7.1) under --safe, with no postulates and no holes. Theorem 3 is unchanged. CapaIF.agda: - releases: the per-expression release log (declassified values, the declassify analogue of the sink output trace). - EAgree / Agree: structural agreement predicates on expressions and on the two big-step derivations. Agree is the faithful operational reading of the paper's released-value agreement, evaluated at the store each declassify is actually reached in. CapaNoninterference.agda: - eagree->releq / releq->eagree: EAgree is equivalent to release log equality, so the agreement hypothesis IS release-log equality, phrased per position so L-Op / L-Declassify decompose without list-append surgery (helpers len, dcount, releases-length, ++-cancel). - lemma1-decl: Lemma 1 re-admitting declassify; the L-Declassify case is discharged by the agreement witness. - theorem4: Theorem 3 clause for clause with declassify allowed; low cases use lemma1-decl, SECRET cases use confinement and never consult the agreement. - worked example sink(declassify(env-get)): covered by Theorem 4, excluded from Theorem 3, agreement reduces to secret equality, so Theorem 4 does not collapse into Theorem 3. Documents deviation D3 (release-log encoding of the agreement hypothesis) in proofs/README.md and docs/semantics.md Section 9.7.1; moves Theorem 4 from "future" to shipped. Checked locally on Agda 2.7.0.1.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Machine-checks lambda_if Theorem 4 (relaxed noninterference / delimited release, docs/semantics.md Section 9.7.1) in Agda under
--safe, with NO postulates and NO holes. Theorem 3 and the existing lemmas are unchanged.What landed
releases(CapaIF.agda): the per-expression release log, thedeclassifyanalogue of thesinkoutput trace.EAgree/Agree(CapaIF.agda): structural agreement predicates on expressions and on the two big-step derivations.Agreeis the faithful operational reading of the paper's released-value agreement, evaluated at the store each declassify is actually reached in.eagree<->releq(CapaNoninterference.agda):EAgreeis proved equivalent to release-log equality, so the agreement hypothesis genuinely IS release-log equality, only phrased per declassify position so theL-Op/L-Declassifycases decompose without list-append surgery.lemma1-decl: Lemma 1 re-admittingdeclassify; the newL-Declassifycase is discharged directly by the agreement witness (the paper's one-line extra case).theorem4: Theorem 3 clause for clause withdeclassifyallowed. Low (PUBLIC) cases uselemma1-decl; SECRET cases use confinement and never consult the agreement (declassifies under SECRET pc are confined).Non-vacuity
A worked example
sink(declassify(env-get))is well-typed, evaluable, covered by Theorem 4, and EXCLUDED from Theorem 3 (noDFStmt). Its agreement hypothesis reduces to secret equalityk1 == k2, so Theorem 4 does not collapse into Theorem 3 and the hypothesis is necessary (without it the two runs emit different public output).Docs
Deviation D3 (release-log encoding of the agreement hypothesis) is documented in
proofs/README.mdanddocs/semantics.mdSection 9.7.1; Theorem 4 moves from "future" to shipped.Checked locally on Agda 2.7.0.1; CI uses 2.6.4.3.