zeekay df342b8bce proofs: Lean <-> EC bridge map + check-lean-bridge.sh CI guard ...

5-axiom Lean-to-EasyCrypt correspondence for Corona, mirroring Pulsar's
structure:

  lagrange_inverse_eval (Corona_N1.ec)
    -> Crypto.Corona.Shamir.shamir_correct_at_target

  threshold_partial_response_identity (Corona_N1.ec)
    -> Crypto.Threshold.Lagrange.threshold_partial_response_identity

  add_share_zeroR (Corona_N4.ec)
    -> Mathlib AddCommMonoid instance

  reconstruct_linear (Corona_N4.ec)
    -> Crypto.Threshold.Lagrange.combine_distributes_over_sum

  shamir_correct (Corona_N4.ec)
    -> Crypto.Corona.Shamir.shamir_correct_at_target

CI guard `scripts/check-lean-bridge.sh` verifies for every EC axiom
that (1) the axiom still exists as `axiom` (not silently demoted to
`lemma`), (2) it carries an inline citation comment naming the Lean
theorem, (3) the Lean theorem still exists at the named path. It also
checks that every EC file mentioned in the bridge doc exists on disk.

Auto-detects the Lean repo at ~/work/lux/proofs/lean or sibling
locations. Skips Lean-side existence checks if no Lean repo is on disk.

Mirrors ~/work/lux/pulsar/scripts/check-lean-bridge.sh exactly.

2026-05-19 08:38:08 -07:00

..

easycrypt

proofs: write EC theories (Corona_N1, N4, refinement chain) -- admit budget 0/13

2026-05-19 08:37:57 -07:00

lean-easycrypt-bridge.md

proofs: Lean <-> EC bridge map + check-lean-bridge.sh CI guard

2026-05-19 08:38:08 -07:00