saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-03 19:53:49 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
fips205-slhdsa-verified/verification/inventory-allowlist.txt
mrwulf 73a92fad53 Phase 3c: declaration coverage in both directions, and the accounting identity 
Completes the round-8 hardening of this repository. Round-8 review (Claude,
register keys `drv-surface-no-cones` and `accounting-certifies-enumeration`).

WHAT PHASE 3 DID NOT PIN. It proves each certificate's cone is exact and that
no declaration in scope carries a disallowed axiom. It does not pin WHICH
declarations exist: a new one that happens to be clean, and a silently vanished
one, both pass it.

  inventory-allowlist.txt  265 rows — the audited corpus
  driver-allowlist.txt      35 rows — the audit INSTRUMENT's own surface
  both as INV|module|name|kind|CONE, diffed in BOTH directions by
  inventory_gate.sh, the same implementation the ed25519 repositories use,
  with a tag per surface.

The instrument surface carries cones because the reviewer showed enumeration is
not audit: a claim planted in an instrument is counted by an accounting identity
and then examined by nothing, if its row carries no cone and no allowlist
covers it. Here the instrument's 35 declarations are pinned exactly as the
corpus's 265 are.

INTERNAL NAMES ARE NO LONGER EXEMPT from the environment walk. They were
skipped, which was harmless while nothing compared that walk against the
kernel's view — and became a hole the moment something did: Phase 3b reads
object files, which contain the compiler's auxiliaries. Exempting them would
have left the accounting identity permanently short and forced the residual to
be "explained" by a constant. That is the shape of the fudge term four-fork data
refuted in the ed25519 repositories, and it is refused here before it can start.

THE ACCOUNTING IDENTITY, as SET CONTAINMENT and never arithmetic: every constant
the kernel holds must appear in one of the two walks. The kernel gate now emits
KERNEL-NAME rows so the comparison names what is missing rather than reporting a
count that has to be interpreted.

    kernel 300  =  inventory 265  +  instrument 35     residual: none

Negative-tested, all three rejected by name and the tree restored to green:
  · a deleted INV row      -> UNCLASSIFIED: INV|Proofs.ApexSpec|List.allM.eq_1|theorem|
  · a deleted DRV row      -> UNCLASSIFIED: DRV|Proofs.Audit|SlhVerify.Audit.sortNames|def
  · a row with no declaration behind it -> STALE: …|fips205.ghost_that_does_not_exist|…

Both allowlists join the pinned harness set: not executable, so the
executable-bit rule cannot reach them, and an allowlist an attacker may rewrite
pins nothing.

fips205-slhdsa-verified now has the ed25519 repositories' gate set: 0 hygiene,
0d correspondence, 1 model, 2 proofs, 3 in-Lean audit, 3b kernel-side axiom
gate, 3c coverage + accounting.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-03 17:34:00 +02:00

270 lines
25 KiB
Text
Raw Permalink Blame History

# inventory-allowlist.txt — the audited corpus, one row per declaration:
# INV|module|name|kind|cone
# Diffed in BOTH directions by inventory_gate.sh. A row here that is not in
# the environment is STALE; a declaration not here is UNCLASSIFIED. Neither
# passes. Regenerate deliberately and read the diff.
INV|Proofs.ApexSpec|List.allM.eq_1|theorem|
INV|Proofs.ApexSpec|List.allM.eq_2|theorem|
INV|Proofs.ApexSpec|List.allM.eq_def|theorem|
INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_1|theorem|
INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_2|theorem|
INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.splitter|def|
INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_1|theorem|
INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_2|theorem|
INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.splitter|def|
INV|Proofs.ApexSpec|fips205.allM_byteEq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.ApexSpec|fips205.allM_byteEq|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ApexSpec|fips205.arrayEqU8_spec|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ApexSpec|fips205.byteEq|theorem|
INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_1|theorem|propext
INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_2|theorem|propext
INV|Proofs.ApexSpec|fips205.htVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.ApexSpec|fips205.ht_verify_free_split|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_1|theorem|propext
INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_2|theorem|propext
INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_3|theorem|propext
INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_4|theorem|propext
INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_5|theorem|propext
INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_6|theorem|propext
INV|Proofs.ApexSpec|fips205.slhVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
INV|Proofs.ApexSpec|fips205.slh_verify_128s_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
INV|Proofs.ApexSpec|fips205.slh_verify_internal_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
INV|Proofs.ChainSpec|Aeneas.Std.core.cmp.impls.PartialOrdU32.lt.eq_1|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_1|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_2|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.splitter|def|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
INV|Proofs.ChainSpec|fips205.chainFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.chainFoldN._proof_1|theorem|propext
INV|Proofs.ChainSpec|fips205.chainFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.chainFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.chainFoldN.match_1|def|
INV|Proofs.ChainSpec|fips205.chainFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_9|theorem|Quot.sound,propext
INV|Proofs.ChainSpec|fips205.chain_free_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.chain_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.fwd_succ|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ChainSpec|fips205.hbody|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.ChainSpec|fips205.hnext|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ChainSpec|fips205.loop_unfold_bind|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_2|theorem|Quot.sound,propext
INV|Proofs.ChainSpec|fips205.u32_succ|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_1|theorem|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_2|theorem|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.splitter|def|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_1|theorem|propext
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_2|theorem|propext
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_3|theorem|propext
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.match_1|def|
INV|Proofs.ForsInnerSpec|fips205.forsInnerFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsInnerSpec|fips205.fors_inner_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsInnerSpec|fips205.hbody_fi|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_1|theorem|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_2|theorem|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.splitter|def|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_1|theorem|propext
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_2|theorem|propext
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.match_1|def|
INV|Proofs.ForsOuterSpec|fips205.forsOuterFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|fips205.fors_outer_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.ForsOuterSpec|fips205.hbody_fo|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_1|theorem|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_2|theorem|
INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.splitter|def|
INV|Proofs.HtSpec|fips205.hbody_ht|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.HtSpec|fips205.htFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.HtSpec|fips205.htFoldN._proof_1|theorem|propext
INV|Proofs.HtSpec|fips205.htFoldN._proof_2|theorem|propext
INV|Proofs.HtSpec|fips205.htFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.HtSpec|fips205.htFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.HtSpec|fips205.htFoldN.match_1|def|
INV|Proofs.HtSpec|fips205.htFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.HtSpec|fips205.ht_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.HtSpec|fips205.ht_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
INV|Proofs.InputPrepSpec|Aeneas.Std.I32.ofInt.congr_simp|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_1|theorem|propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_2|theorem|propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.splitter|def|propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_1|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_2|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.splitter|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_1|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_2|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.splitter|def|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_1|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_2|theorem|
INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.splitter|def|
INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._f|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._proof_1|theorem|propext
INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._sunfold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.match_1|def|propext
INV|Proofs.InputPrepSpec|fips205.base2bOuterFold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.base2b_outer_step|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.hbody_b2|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.hbody_cs|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.hbody_tb|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.hbody_ti|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toByteFold._f|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_1|theorem|propext
INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_2|theorem|propext
INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_3|theorem|propext
INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_4|theorem|propext
INV|Proofs.InputPrepSpec|fips205.toByteFold._sunfold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toByteFold.eq_def|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toByteFold.match_1|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toByteFold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toIntFold._f|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_1|theorem|propext
INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_2|theorem|propext
INV|Proofs.InputPrepSpec|fips205.toIntFold._sunfold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toIntFold.eq_def|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.toIntFold.match_1|def|
INV|Proofs.InputPrepSpec|fips205.toIntFold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_byte_step|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.to_int_step|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._f|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._sunfold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.eq_def|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.match_1|def|
INV|Proofs.InputPrepSpec|fips205.wotsCsumFold|def|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.InputPrepSpec|fips205.wots_csum_step|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.WotsSpec|Aeneas.Std.core.cmp.impls.PartialOrdUsize.lt.eq_1|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_1|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_2|theorem|
INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.splitter|def|
INV|Proofs.WotsSpec|fips205.fwd_succ_usize|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.WotsSpec|fips205.hbody1|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.WotsSpec|fips205.hnext_usize|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_2|theorem|Quot.sound,propext
INV|Proofs.WotsSpec|fips205.usize_succ|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.WotsSpec|fips205.wotsChainFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_1|theorem|propext
INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_2|theorem|propext
INV|Proofs.WotsSpec|fips205.wotsChainFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.WotsSpec|fips205.wotsChainFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.WotsSpec|fips205.wotsChainFold.match_1|def|
INV|Proofs.WotsSpec|fips205.wotsChainFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_9|theorem|Quot.sound,propext
INV|Proofs.WotsSpec|fips205.wots_loop1_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.WotsSpec|fips205.wots_loop1_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_1|theorem|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_2|theorem|
INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.splitter|def|
INV|Proofs.XmssSpec|fips205.hbody_x|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.XmssSpec|fips205.xmssFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_1|theorem|propext
INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_2|theorem|propext
INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_3|theorem|propext
INV|Proofs.XmssSpec|fips205.xmssFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.XmssSpec|fips205.xmssFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.XmssSpec|fips205.xmssFoldN.match_1|def|
INV|Proofs.XmssSpec|fips205.xmssFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_1|theorem|Quot.sound,propext
INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_5|theorem|Quot.sound,propext
INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_6|theorem|Quot.sound,propext
INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_7|theorem|Quot.sound,propext
INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_8|theorem|Quot.sound,propext
INV|Proofs.XmssSpec|fips205.xmss_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
INV|Proofs.XmssSpec|fips205.xmss_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
Reference in a new issue View git blame Copy permalink