Code

Initial generic FO-U proofs#8

Code

Merged

MM45 merged 11 commits intomainsandbox-quantum/EasyCrypt-KEMs:mainfrom FOsandbox-quantum/EasyCrypt-KEMs:FOCopy head branch name to clipboardJan 8, 2025

+2,094-8

Commits

Commits on Jan 2, 2025

• Name change

  MM45

  committed
  3dff516

  Copy full SHA for 3dff516

Commits on Jan 3, 2025

• fix correctness definition and initial attempt at formalizing FO (might change to operator-based)

  MM45

  committed
  69281e4

  Copy full SHA for 69281e4

• Specification all variants FO-U in standard model and first test proof.

  MM45

  committed
  67589c1

  Copy full SHA for 67589c1

• Think about (and document) properties and proofs for different FO U transforms.

  MM45

  committed
  6edd150

  Copy full SHA for 6edd150

• Most LEAK proofs for explicit Umc transform.

  MM45

  committed
  adcdd7b

  Copy full SHA for adcdd7b

• Rebase and fix

  MM45

  committed
  1b84627

  Copy full SHA for 1b84627

• Add first proof for Umc explicit and part of second (needs more thinking).

  MM45

  committed
  5f61c09

  Copy full SHA for 5f61c09

Commits on Jan 7, 2025

• Main proofs Um explicit.

  MM45

  committed
  4e5ded5

  Copy full SHA for 4e5ded5

Commits on Jan 8, 2025

• Comment out proofs that turn out to be impossible.

  MM45

  committed
  e059667

  Copy full SHA for e059667

• Complete last generic proof LEAK-BIND proof.

  MM45

  committed
  401fa2b

  Copy full SHA for 401fa2b

• Fixing dependencies on old stuff.

  MM45

  committed
  b2838c1

  Copy full SHA for b2838c1