Report #15 — Selected raw padding behavior in block-padding 0.4.2

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

12 verified claims · 1 finding

Recorded by the author; proofs.rs has not re-run it. How to read a report

MasWag · 2026-11-03 11:41 UTC

Revision v1

Overview

The selected raw padding contracts describe every byte of the resulting block. For ZeroPadding and NoPadding, the message position may equal the block length; ZeroPadding fills the remaining bytes with zero, while NoPadding leaves the block unchanged. For Pkcs7, Iso10126, and AnsiX923, the position must be less than the block length and the length at most 255. Pkcs7 fills the suffix with its length; Iso10126 uses the same deterministic padding; AnsiX923 uses zeros followed by the suffix length. Iso7816 requires the position to be less than the block length and writes 0x80 followed by zeros. In each case the original prefix is preserved and the selected extracted call succeeds on the stated domain.

For every input slice, NoPadding returns the entire input and ZeroPadding removes the maximal trailing run of zeros. Iso7816 accepts exactly a final 0x80 byte followed only by zeros and returns the prefix before it; otherwise it returns an error. For Pkcs7, Iso10126, and AnsiX923, decoding is established for block lengths from 1 through 255. The last byte must give a count between 1 and the block length. Pkcs7 also requires all counted bytes to equal that count; AnsiX923 requires the preceding counted bytes to be zero; Iso10126 accepts arbitrary preceding padding bytes. A valid block returns the prefix before the padding, and an invalid block returns an error.

Findings (1)

Empty input panics in three raw unpadding implementations

Found in Report #15 v1 · Updated 2026-11-03 11:41 UTC

APIs (12)

Recorded callables

<block_padding::AnsiX923 as block_padding::Padding>::raw_pad recorded callable · signature and safety not recorded

Claim #4

<block_padding::AnsiX923 as block_padding::Padding>::raw_unpad recorded callable · signature and safety not recorded

Claim #12

<block_padding::Iso10126 as block_padding::Padding>::raw_pad recorded callable · signature and safety not recorded

Claim #3

<block_padding::Iso10126 as block_padding::Padding>::raw_unpad recorded callable · signature and safety not recorded

Claim #11

<block_padding::Iso7816 as block_padding::Padding>::raw_pad recorded callable · signature and safety not recorded

Claim #5

<block_padding::Iso7816 as block_padding::Padding>::raw_unpad recorded callable · signature and safety not recorded

Claim #9

<block_padding::NoPadding as block_padding::Padding>::raw_pad recorded callable · signature and safety not recorded

Claim #6

<block_padding::NoPadding as block_padding::Padding>::raw_unpad recorded callable · signature and safety not recorded

Claim #7

<block_padding::Pkcs7 as block_padding::Padding>::raw_pad recorded callable · signature and safety not recorded

Claim #2

<block_padding::Pkcs7 as block_padding::Padding>::raw_unpad recorded callable · signature and safety not recorded

Claim #10

<block_padding::ZeroPadding as block_padding::Padding>::raw_pad recorded callable · signature and safety not recorded

Claim #1

<block_padding::ZeroPadding as block_padding::Padding>::raw_unpad recorded callable · signature and safety not recorded

Claim #8

Evidence

https://github.com/MasWag/crate-proofs/tree/8ffde6cb60a5f280528cc3759b03663db8e0b7d6

Reproduce

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/MasWag/crate-proofs report-15-source-1
git -C report-15-source-1 checkout --detach 8ffde6cb60a5f280528cc3759b03663db8e0b7d6
git -C report-15-source-1 submodule update --init --recursive --checkout
cd report-15-source-1/block-padding/0.4.2/.work/build/default/aarch64-apple-darwin/proofs

lake build +AnsiUnpadProofs +CountUnpadProofs +Proofs +UnpadProofs

printf '%s' 'import Aeneas
import AnsiUnpadProofs
import CountUnpadProofs
import Proofs
import UnpadProofs
set_option pp.all true
set_option pp.universes true
set_option pp.explicit true
set_option pp.fullNames true
set_option pp.notation false
set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 10000000
-- proofs.rs adapter for Lean 4.35.0 / Aeneas be86ab0f.
-- Uses Lean'\''s environment, Meta telescope and pretty-printer, never source parsing.
open Lean Meta Elab Command
namespace ProofsProbe
meta def moduleOf (env : Environment) (n : Name) : String :=
  match env.getModuleIdxFor? n with
  | some idx => env.header.moduleNames[idx.toNat]!.toString
  | none => ""
meta def pretty (e : Expr) : MetaM String := do
  let s := (← ppExpr e).pretty
  if s.contains '\''⋯'\'' then
    throwError "Lean display contains an omission marker (or literal ⋯); refusing an incomplete proposition"
  if s.utf8ByteSize > 1000000 then throwError "Proposition exceeds 1,000,000-byte recording limit"
  return s
-- The full statement stays explicit; the inspection view uses Lean notation.
meta def readable (e : Expr) : MetaM String :=
  withOptions (fun o =>
    let o := o.setBool `pp.all false
    let o := o.setBool `pp.explicit false
    let o := o.setBool `pp.universes false
    o.setBool `pp.notation true) (pretty e)
-- Only a constant'\''s own tag grants a link; names in plain text are never guessed.
partial def segments (code : Widget.CodeWithInfos) (ref : Option Name := none) : Array Json :=
  match code with
  | .text text => #[Json.mkObj (([("text", toJson text)]) ++
      (ref.toList.map fun n => ("ref", toJson n.toString)))]
  | .append parts => parts.foldl (fun acc part => acc ++ segments part ref) #[]
  | .tag info part =>
    let ref := match info.info.val.info with
      | .ofTermInfo ti => ti.expr.constName?
      | _ => none
    segments part ref
meta def readableFields (key : String) (e : Expr) : MetaM (List (String × Json)) := do
  let text ← readable e
  let base := [(key, toJson text)]
  try
    let code ← withOptions (fun o =>
      let o := o.setBool `pp.all false
      let o := o.setBool `pp.explicit false
      let o := o.setBool `pp.universes false
      let o := o.setBool `pp.notation true
      o.setBool `pp.tagAppFns true) (Widget.ppExprTagged e)
    let parts := segments code
    let joined := String.join (parts.toList.map fun j =>
      (j.getObjValAs? String "text").toOption.getD "")
    if joined != text || parts.size > 10000 || joined.utf8ByteSize > 1000000 then
      return base
    return base ++ [(key ++ "_segments", toJson parts)]
  catch _ => return base
meta def inspect (n : Name) (ty : Expr) (manual : Bool) : MetaM (Option Json) := do
  let env ← getEnv
  forallTelescope ty fun xs conclusion => do
    let programExpr ← try
      let normalized ← Aeneas.Utils.normalizeLetBindings conclusion
      let (expr, _) ← Aeneas.Step.getStepSpecFunArgsExpr normalized
      pure (some expr)
    catch _ => pure none
    if programExpr.isNone && !manual then return none
    let full ← pretty ty
    let program ← match programExpr with
      | some expr => pure (toJson (← readable expr))
      | none => pure Json.null
    let head := toJson (programExpr.bind (·.getAppFn.constName?) |>.map Name.toString)
    let mut binders := #[]
    for x in xs do
      let d ← x.fvarId!.getDecl
      let prop ← isProp d.type
      binders := binders.push (Json.mkObj ((← readableFields "type" d.type) ++ [
        ("name", toJson d.userName.toString),
        ("kind", toJson (if d.binderInfo.isInstImplicit then "instance" else if prop then "hypothesis" else "variable")),
        ("binder", toJson (if d.binderInfo.isInstImplicit then "instance" else if d.binderInfo.isExplicit then "explicit" else "implicit"))]))
    if binders.size > 1000 then throwError "More than 1000 binders"
    let some ranges ← findDeclarationRanges? n | throwError "Missing theorem source range: {n}"
    let axioms ← Lean.collectAxioms n
    let constants := ty.getUsedConstants
    let mut definitions := #[]
    for nm in constants.extract 0 100 do
      let ranges ← findDeclarationRanges? nm
      definitions := definitions.push (Json.mkObj [
        ("name", toJson nm.toString), ("module", toJson (moduleOf env nm)),
        ("source", match ranges with
          | some r => Json.mkObj [("first_line", toJson r.range.pos.line), ("last_line", toJson r.range.endPos.line)]
          | none => Json.null)])
    return some (Json.mkObj ((← readableFields "conclusion" conclusion) ++ [
      ("version", toJson (1 : Nat)), ("theorem", toJson n.toString),
      ("module", toJson (moduleOf env n)), ("statement", toJson full),
      ("binders", toJson binders),
      ("program", program), ("program_head", head),
      ("axioms", toJson (axioms.map Name.toString)),
      ("first_line", toJson ranges.range.pos.line), ("last_line", toJson ranges.range.endPos.line),
      ("definitions", toJson definitions), ("definitions_truncated", toJson (decide (constants.size > 100))),
      ("translation_rerun", toJson false)]))
end ProofsProbe

run_cmd do
  let manual : Array Name := #[`BlockPadding.Proof.zero_pad_total, `BlockPadding.Proof.pkcs_pad_total, `BlockPadding.Proof.iso10126_pad_total, `BlockPadding.Proof.ansi_pad_total, `BlockPadding.Proof.iso7816_pad_total, `BlockPadding.Proof.no_pad, `BlockPadding.Proof.no_unpad, `BlockPadding.UnpadProof.zero_unpad_total, `BlockPadding.UnpadProof.iso_unpad_total, `BlockPadding.CountUnpadProof.pkcs_unpad_total, `BlockPadding.CountUnpadProof.iso10126_unpad_total, `BlockPadding.AnsiUnpadProof.ansi_unpad_total]
  let localModules : Array String := #[]
  let roots : Array Name := #[]
  let env ← getEnv
  let mut closure : Array Name := #[]
  let mut pending := roots.toList
  while !pending.isEmpty do
    let m := pending.head!
    pending := pending.tail!
    if !closure.contains m then
      closure := closure.push m
      if let some idx := env.header.moduleNames.findIdx? (· == m) then
        pending := (env.header.moduleData[idx]!.imports.toList.map (·.module)) ++ pending
  let scope := closure.filter (fun m => localModules.contains m.toString)
  for n in manual do
    match env.find? n with
    | some (.thmInfo _) => pure ()
    | _ => throwError "Expected a theorem: {n}"
  for (n, ci) in env.constants.toList do
    let explicit := manual.contains n
    if explicit || scope.contains (ProofsProbe.moduleOf env n).toName then
      if let .thmInfo th := ci then
        let result ← liftTermElabM <| ProofsProbe.inspect n th.type explicit
        if let some value := result then
          liftIO <| IO.println ("proofs.rs:formal:" ++ value.compress)

run_cmd do
  let theorem_name := `BlockPadding.Proof.ansi_pad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.ansi_pad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.ansi_pad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.ansi_pad_total"

run_cmd do
  let theorem_name := `BlockPadding.AnsiUnpadProof.ansi_unpad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.AnsiUnpadProof.ansi_unpad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.AnsiUnpadProof.ansi_unpad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.AnsiUnpadProof.ansi_unpad_total"

run_cmd do
  let theorem_name := `BlockPadding.Proof.iso10126_pad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.iso10126_pad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.iso10126_pad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.iso10126_pad_total"

run_cmd do
  let theorem_name := `BlockPadding.CountUnpadProof.iso10126_unpad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.CountUnpadProof.iso10126_unpad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.CountUnpadProof.iso10126_unpad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.CountUnpadProof.iso10126_unpad_total"

run_cmd do
  let theorem_name := `BlockPadding.Proof.iso7816_pad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.iso7816_pad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.iso7816_pad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.iso7816_pad_total"

run_cmd do
  let theorem_name := `BlockPadding.UnpadProof.iso_unpad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.UnpadProof.iso_unpad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.UnpadProof.iso_unpad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.UnpadProof.iso_unpad_total"

run_cmd do
  let theorem_name := `BlockPadding.Proof.no_pad
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.no_pad"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.no_pad: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.no_pad"

run_cmd do
  let theorem_name := `BlockPadding.Proof.no_unpad
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.no_unpad"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.no_unpad: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.no_unpad"

run_cmd do
  let theorem_name := `BlockPadding.Proof.pkcs_pad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.pkcs_pad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.pkcs_pad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.pkcs_pad_total"

run_cmd do
  let theorem_name := `BlockPadding.CountUnpadProof.pkcs_unpad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.CountUnpadProof.pkcs_unpad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.CountUnpadProof.pkcs_unpad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.CountUnpadProof.pkcs_unpad_total"

run_cmd do
  let theorem_name := `BlockPadding.Proof.zero_pad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.Proof.zero_pad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.Proof.zero_pad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.Proof.zero_pad_total"

run_cmd do
  let theorem_name := `BlockPadding.UnpadProof.zero_unpad_total
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BlockPadding.UnpadProof.zero_unpad_total"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BlockPadding.UnpadProof.zero_unpad_total: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BlockPadding.UnpadProof.zero_unpad_total"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 12 checks passed · 0 failed

2026-11-03T11:36:59.328536+00:00 · 58.1 seconds · Exit code 0

Recorded on the author’s machine.

Check	Result	Claim
Lean checked theorem BlockPadding.Proof.ansi_pad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.ansi_pad_total`	Passed	Claim #4
Lean checked theorem BlockPadding.AnsiUnpadProof.ansi_unpad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.AnsiUnpadProof.ansi_unpad_total`	Passed	Claim #12
Lean checked theorem BlockPadding.Proof.iso10126_pad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.iso10126_pad_total`	Passed	Claim #3
Lean checked theorem BlockPadding.CountUnpadProof.iso10126_unpad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.CountUnpadProof.iso10126_unpad_total`	Passed	Claim #11
Lean checked theorem BlockPadding.Proof.iso7816_pad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.iso7816_pad_total`	Passed	Claim #5
Lean checked theorem BlockPadding.UnpadProof.iso_unpad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.UnpadProof.iso_unpad_total`	Passed	Claim #9
Lean checked theorem BlockPadding.Proof.no_pad; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.no_pad`	Passed	Claim #6
Lean checked theorem BlockPadding.Proof.no_unpad; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.no_unpad`	Passed	Claim #7
Lean checked theorem BlockPadding.Proof.pkcs_pad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.pkcs_pad_total`	Passed	Claim #2
Lean checked theorem BlockPadding.CountUnpadProof.pkcs_unpad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.CountUnpadProof.pkcs_unpad_total`	Passed	Claim #10
Lean checked theorem BlockPadding.Proof.zero_pad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.Proof.zero_pad_total`	Passed	Claim #1
Lean checked theorem BlockPadding.UnpadProof.zero_unpad_total; axioms limited to propext, Classical.choice, Quot.sound `BlockPadding.UnpadProof.zero_unpad_total`	Passed	Claim #8

Execution details

Started: 2026-11-03T11:36:59.328536+00:00
Finished: 2026-11-03T11:37:57.458378+00:00
Platform: macos aarch64
Rust compiler: rustc 1.91.1 (ed61e7d7e 2025-11-07) binary: rustc commit-hash: ed61e7d7e242494fb7057f2657300d9e77bb4fcb commit-date: 2025-11-07 host: aarch64-apple-darwin release: 1.91.1 LLVM version: 21.1.2
Working directory: block-padding/0.4.2/.work/build/default/aarch64-apple-darwin/proofs
Environment overrides: None recorded
Git repository: https://github.com/MasWag/crate-proofs
Git commit: 8ffde6cb60a5f280528cc3759b03663db8e0b7d6

Diagnostics & logs

=== stdout ===
✔ [1796/1801] Built BlockPadding.Specs (2.0s)
✔ [1797/1801] Built BlockPaddingVerificationApi (7.4s)
⚠ [1798/1801] Built Proofs (9.0s)
warning: Proofs.lean:22:31: This simp argument is unused:
  UScalar.le_equiv

Hint: Omit it from the simp argument list.
  [apply] simp [NoPadding.Insts.Block_padding_verification_apiPadding.raw_pad, Slice.len, massert, UScalar.lt_equiv, h]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:37:69: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:37:69: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Proofs.lean:77:107: This simp argument is unused:
  hd

Hint: Omit it from the simp argument list.
  [apply] simp [bytes, Spec.Padded, hout, hback, Slice.set, Slice.setAtNat, Slice.setSlice!, hs', hlen, hlast, hn,
    List.setSlice!, hmin, hp, List.set_append, hsum, Nat.mod_eq_of_lt hsmall]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Proofs.lean:77:160: This simp argument is unused:
  Nat.mod_eq_of_lt hsmall

Hint: Omit it from the simp argument list.
  [apply] simp [bytes, Spec.Padded, hout, hback, Slice.set, Slice.setAtNat, Slice.setSlice!, hs', hlen, hlast, hn, hd,
    List.setSlice!, hmin, hp, List.set_append, hsum]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [1799/1801] Built UnpadProofs (9.3s)
warning: UnpadProofs.lean:165:4: `Iso7816.Insts.Block_padding_verification_apiPadding.raw_unpad_loop.body.match_1` refers to an auto-generated auxiliary declaration. These are not stable across refactors; consider using a different approach.

Note: This linter can be disabled with `set_option linter.auxLemma false`
⚠ [1800/1801] Built CountUnpadProofs (4.0s)
warning: CountUnpadProofs.lean:170:12: This simp argument is unused:
  List.getElem?_append

Hint: Omit it from the simp argument list.
  [apply] simp [hhead] at he

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [1801/1801] Built AnsiUnpadProofs (4.1s)
Build completed successfully (1801 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"p","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"↑p < b.length","type_segments":[{"text":"↑"},{"text":"p"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_pad b p =\n      Aeneas.Std.Result.ok out ∧\n    BlockPadding.Proof.bytes out =\n      BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.iso7816 (BlockPadding.Proof.bytes b) ↑p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_pad","text":"block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_pad"},{"text":" "},{"text":"b"},{"text":" "},{"text":"p"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" =\n      "},{"ref":"BlockPadding.Spec.Padded","text":"BlockPadding.Spec.Padded"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.iso7816","text":"BlockPadding.Spec.Algorithm.iso7816"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.Usize","source":{"first_line":32,"last_line":32}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_pad","source":{"first_line":298,"last_line":312}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Padded","source":{"first_line":20,"last_line":28}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.iso7816","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":128,"last_line":131,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)\n  (h :\n    @LT.lt.{0} Nat instLTNat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n        (block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_pad b p)\n        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))\n      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.iso7816 (BlockPadding.Proof.bytes b)\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))","theorem":"BlockPadding.Proof.iso7816_pad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_unpad b =\n      Aeneas.Std.Result.ok (Aeneas.Std.core.result.Result.Ok out) ∧\n    BlockPadding.Proof.bytes out = List.take (BlockPadding.Proof.bytes b).length (BlockPadding.Proof.bytes b) ∧\n      BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.none (BlockPadding.Proof.bytes b)\n        (BlockPadding.Proof.bytes b).length","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_unpad","text":"block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_unpad"},{"text":" "},{"text":"b"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"("},{"ref":"Aeneas.Std.core.result.Result.Ok","text":"Aeneas.Std.core.result.Result.Ok"},{"text":" "},{"text":"out"},{"text":")"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":"."},{"ref":"List.length","text":"length"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"ref":"And","text":" ∧\n      "},{"ref":"BlockPadding.Spec.Accepted","text":"BlockPadding.Spec.Accepted"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.none","text":"BlockPadding.Spec.Algorithm.none"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":"\n        "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":"."},{"ref":"List.length","text":"length"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result","source":{"first_line":7,"last_line":10}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Error","source":{"first_line":37,"last_line":41}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_unpad","source":{"first_line":381,"last_line":388}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result.Ok","source":{"first_line":9,"last_line":9}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"module":"Init.Prelude","name":"List.length","source":{"first_line":3182,"last_line":3195}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Accepted","source":{"first_line":41,"last_line":58}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.none","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":24,"last_line":28,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1}\n        (Aeneas.Std.Result.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error))\n        (block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_unpad b)\n        (@Aeneas.Std.Result.ok.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error)\n          (@Aeneas.Std.core.result.Result.Ok.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error out)))\n      (And\n        (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n          (@List.take.{0} Nat (@List.length.{0} Nat (BlockPadding.Proof.bytes b)) (BlockPadding.Proof.bytes b)))\n        (BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.none (BlockPadding.Proof.bytes b)\n          (@List.length.{0} Nat (BlockPadding.Proof.bytes b))))","theorem":"BlockPadding.Proof.no_unpad","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"p","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"↑p ≤ b.length","type_segments":[{"text":"↑"},{"text":"p"},{"ref":"LE.le","text":" ≤ "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad b p =\n      Aeneas.Std.Result.ok out ∧\n    BlockPadding.Proof.bytes out =\n      BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.zero (BlockPadding.Proof.bytes b) ↑p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad","text":"block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad"},{"text":" "},{"text":"b"},{"text":" "},{"text":"p"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" =\n      "},{"ref":"BlockPadding.Spec.Padded","text":"BlockPadding.Spec.Padded"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.zero","text":"BlockPadding.Spec.Algorithm.zero"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.Usize","source":{"first_line":32,"last_line":32}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad","source":{"first_line":23,"last_line":35}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Padded","source":{"first_line":20,"last_line":28}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.zero","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":108,"last_line":111,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)\n  (h :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n        (block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_pad b p)\n        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))\n      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.zero (BlockPadding.Proof.bytes b)\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))","theorem":"BlockPadding.Proof.zero_pad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"hypothesis","name":"hpos","type":"0 < b.length","type_segments":[{"text":"0"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]},{"binder":"explicit","kind":"hypothesis","name":"hb","type":"b.length ≤ 255","type_segments":[{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"},{"ref":"LE.le","text":" ≤ "},{"text":"255"}]}],"conclusion":"∃ r,\n  block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_unpad b =\n      Aeneas.Std.Result.ok r ∧\n    match r with\n    | Aeneas.Std.core.result.Result.Ok out =>\n      ∃ p,\n        BlockPadding.Proof.bytes out = List.take p (BlockPadding.Proof.bytes b) ∧\n          BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.ansiX923 (BlockPadding.Proof.bytes b) p\n    | Aeneas.Std.core.result.Result.Err a =>\n      BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.ansiX923 (BlockPadding.Proof.bytes b)","conclusion_segments":[{"text":"∃ "},{"text":"r"},{"text":",\n  "},{"ref":"block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_unpad","text":"block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_unpad"},{"text":" "},{"text":"b"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"r"},{"ref":"And","text":" ∧\n    "},{"text":"match "},{"text":"r"},{"text":" with\n    | "},{"ref":"Aeneas.Std.core.result.Result.Ok","text":"Aeneas.Std.core.result.Result.Ok"},{"text":" "},{"text":"out"},{"text":" =>\n      "},{"text":"∃ "},{"text":"p"},{"text":",\n        "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"p"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"ref":"And","text":" ∧\n          "},{"ref":"BlockPadding.Spec.Accepted","text":"BlockPadding.Spec.Accepted"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.ansiX923","text":"BlockPadding.Spec.Algorithm.ansiX923"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"p"},{"text":"\n    | "},{"ref":"Aeneas.Std.core.result.Result.Err","text":"Aeneas.Std.core.result.Result.Err"},{"text":" "},{"text":"a"},{"text":" =>\n      "},{"ref":"BlockPadding.Spec.Rejected","text":"BlockPadding.Spec.Rejected"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.ansiX923","text":"BlockPadding.Spec.Algorithm.ansiX923"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result","source":{"first_line":7,"last_line":10}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Error","source":{"first_line":37,"last_line":41}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_unpad","source":{"first_line":275,"last_line":296}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"AnsiUnpadProofs","name":"BlockPadding.AnsiUnpadProof.ansi_loop.match_1","source":null},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Accepted","source":{"first_line":41,"last_line":58}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.ansiX923","source":{"first_line":9,"last_line":9}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Rejected","source":{"first_line":60,"last_line":60}}],"definitions_truncated":false,"first_line":180,"last_line":187,"module":"AnsiUnpadProofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n  (hpos :\n    @LT.lt.{0} Nat instLTNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b))\n  (hb :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)\n      (@OfNat.ofNat.{0} Nat (nat_lit 255) (instOfNatNat (nat_lit 255)))),\n  @Exists.{1}\n    (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) block_padding_verification_api.Error)\n    fun\n      (r :\n        Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n          block_padding_verification_api.Error) =>\n    And\n      (@Eq.{1}\n        (Aeneas.Std.Result.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error))\n        (block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_unpad b)\n        (@Aeneas.Std.Result.ok.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error)\n          r))\n      (BlockPadding.AnsiUnpadProof.ansi_loop.match_1.{1}\n        (fun\n            (r :\n              Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n                block_padding_verification_api.Error) =>\n          Prop)\n        r\n        (fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n          @Exists.{1} Nat fun (p : Nat) =>\n            And\n              (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n                (@List.take.{0} Nat p (BlockPadding.Proof.bytes b)))\n              (BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.ansiX923 (BlockPadding.Proof.bytes b) p))\n        fun (a : block_padding_verification_api.Error) =>\n        BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.ansiX923 (BlockPadding.Proof.bytes b))","theorem":"BlockPadding.AnsiUnpadProof.ansi_unpad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"p","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"↑p < b.length","type_segments":[{"text":"↑"},{"text":"p"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]},{"binder":"explicit","kind":"hypothesis","name":"hb","type":"b.length ≤ 255","type_segments":[{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"},{"ref":"LE.le","text":" ≤ "},{"text":"255"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_pad b p =\n      Aeneas.Std.Result.ok out ∧\n    BlockPadding.Proof.bytes out =\n      BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.iso10126 (BlockPadding.Proof.bytes b) ↑p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_pad","text":"block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_pad"},{"text":" "},{"text":"b"},{"text":" "},{"text":"p"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" =\n      "},{"ref":"BlockPadding.Spec.Padded","text":"BlockPadding.Spec.Padded"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.iso10126","text":"BlockPadding.Spec.Algorithm.iso10126"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.Usize","source":{"first_line":32,"last_line":32}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_pad","source":{"first_line":201,"last_line":206}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Padded","source":{"first_line":20,"last_line":28}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.iso10126","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":118,"last_line":121,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)\n  (h :\n    @LT.lt.{0} Nat instLTNat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b))\n  (hb :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)\n      (@OfNat.ofNat.{0} Nat (nat_lit 255) (instOfNatNat (nat_lit 255)))),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n        (block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_pad b p)\n        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))\n      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.iso10126 (BlockPadding.Proof.bytes b)\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))","theorem":"BlockPadding.Proof.iso10126_pad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"p","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"↑p < b.length","type_segments":[{"text":"↑"},{"text":"p"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]},{"binder":"explicit","kind":"hypothesis","name":"hb","type":"b.length ≤ 255","type_segments":[{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"},{"ref":"LE.le","text":" ≤ "},{"text":"255"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_pad b p =\n      Aeneas.Std.Result.ok out ∧\n    BlockPadding.Proof.bytes out =\n      BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.ansiX923 (BlockPadding.Proof.bytes b) ↑p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_pad","text":"block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_pad"},{"text":" "},{"text":"b"},{"text":" "},{"text":"p"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" =\n      "},{"ref":"BlockPadding.Spec.Padded","text":"BlockPadding.Spec.Padded"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.ansiX923","text":"BlockPadding.Spec.Algorithm.ansiX923"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.Usize","source":{"first_line":32,"last_line":32}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_pad","source":{"first_line":217,"last_line":236}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Padded","source":{"first_line":20,"last_line":28}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.ansiX923","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":123,"last_line":126,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)\n  (h :\n    @LT.lt.{0} Nat instLTNat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b))\n  (hb :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)\n      (@OfNat.ofNat.{0} Nat (nat_lit 255) (instOfNatNat (nat_lit 255)))),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n        (block_padding_verification_api.AnsiX923.Insts.Block_padding_verification_apiPadding.raw_pad b p)\n        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))\n      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.ansiX923 (BlockPadding.Proof.bytes b)\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))","theorem":"BlockPadding.Proof.ansi_pad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"hypothesis","name":"hpos","type":"0 < b.length","type_segments":[{"text":"0"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]},{"binder":"explicit","kind":"hypothesis","name":"hb","type":"b.length ≤ 255","type_segments":[{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"},{"ref":"LE.le","text":" ≤ "},{"text":"255"}]}],"conclusion":"∃ r,\n  block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_unpad b =\n      Aeneas.Std.Result.ok r ∧\n    match r with\n    | Aeneas.Std.core.result.Result.Ok out =>\n      ∃ p,\n        BlockPadding.Proof.bytes out = List.take p (BlockPadding.Proof.bytes b) ∧\n          BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.pkcs7 (BlockPadding.Proof.bytes b) p\n    | Aeneas.Std.core.result.Result.Err a =>\n      BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.pkcs7 (BlockPadding.Proof.bytes b)","conclusion_segments":[{"text":"∃ "},{"text":"r"},{"text":",\n  "},{"ref":"block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_unpad","text":"block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_unpad"},{"text":" "},{"text":"b"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"r"},{"ref":"And","text":" ∧\n    "},{"text":"match "},{"text":"r"},{"text":" with\n    | "},{"ref":"Aeneas.Std.core.result.Result.Ok","text":"Aeneas.Std.core.result.Result.Ok"},{"text":" "},{"text":"out"},{"text":" =>\n      "},{"text":"∃ "},{"text":"p"},{"text":",\n        "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"p"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"ref":"And","text":" ∧\n          "},{"ref":"BlockPadding.Spec.Accepted","text":"BlockPadding.Spec.Accepted"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.pkcs7","text":"BlockPadding.Spec.Algorithm.pkcs7"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"p"},{"text":"\n    | "},{"ref":"Aeneas.Std.core.result.Result.Err","text":"Aeneas.Std.core.result.Result.Err"},{"text":" "},{"text":"a"},{"text":" =>\n      "},{"ref":"BlockPadding.Spec.Rejected","text":"BlockPadding.Spec.Rejected"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.pkcs7","text":"BlockPadding.Spec.Algorithm.pkcs7"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result","source":{"first_line":7,"last_line":10}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Error","source":{"first_line":37,"last_line":41}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_unpad","source":{"first_line":192,"last_line":199}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"CountUnpadProofs","name":"BlockPadding.CountUnpadProof.pkcs_loop.match_1","source":null},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Accepted","source":{"first_line":41,"last_line":58}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.pkcs7","source":{"first_line":9,"last_line":9}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Rejected","source":{"first_line":60,"last_line":60}}],"definitions_truncated":false,"first_line":212,"last_line":219,"module":"CountUnpadProofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n  (hpos :\n    @LT.lt.{0} Nat instLTNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b))\n  (hb :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)\n      (@OfNat.ofNat.{0} Nat (nat_lit 255) (instOfNatNat (nat_lit 255)))),\n  @Exists.{1}\n    (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) block_padding_verification_api.Error)\n    fun\n      (r :\n        Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n          block_padding_verification_api.Error) =>\n    And\n      (@Eq.{1}\n        (Aeneas.Std.Result.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error))\n        (block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_unpad b)\n        (@Aeneas.Std.Result.ok.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error)\n          r))\n      (BlockPadding.CountUnpadProof.pkcs_loop.match_1.{1}\n        (fun\n            (r :\n              Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n                block_padding_verification_api.Error) =>\n          Prop)\n        r\n        (fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n          @Exists.{1} Nat fun (p : Nat) =>\n            And\n              (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n                (@List.take.{0} Nat p (BlockPadding.Proof.bytes b)))\n              (BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.pkcs7 (BlockPadding.Proof.bytes b) p))\n        fun (a : block_padding_verification_api.Error) =>\n        BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.pkcs7 (BlockPadding.Proof.bytes b))","theorem":"BlockPadding.CountUnpadProof.pkcs_unpad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"p","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"↑p < b.length","type_segments":[{"text":"↑"},{"text":"p"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]},{"binder":"explicit","kind":"hypothesis","name":"hb","type":"b.length ≤ 255","type_segments":[{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"},{"ref":"LE.le","text":" ≤ "},{"text":"255"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_pad b p =\n      Aeneas.Std.Result.ok out ∧\n    BlockPadding.Proof.bytes out =\n      BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.pkcs7 (BlockPadding.Proof.bytes b) ↑p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_pad","text":"block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_pad"},{"text":" "},{"text":"b"},{"text":" "},{"text":"p"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" =\n      "},{"ref":"BlockPadding.Spec.Padded","text":"BlockPadding.Spec.Padded"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.pkcs7","text":"BlockPadding.Spec.Algorithm.pkcs7"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.Usize","source":{"first_line":32,"last_line":32}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_pad","source":{"first_line":173,"last_line":190}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Padded","source":{"first_line":20,"last_line":28}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.pkcs7","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":113,"last_line":116,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)\n  (h :\n    @LT.lt.{0} Nat instLTNat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b))\n  (hb :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)\n      (@OfNat.ofNat.{0} Nat (nat_lit 255) (instOfNatNat (nat_lit 255)))),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n        (block_padding_verification_api.Pkcs7.Insts.Block_padding_verification_apiPadding.raw_pad b p)\n        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))\n      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.pkcs7 (BlockPadding.Proof.bytes b)\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))","theorem":"BlockPadding.Proof.pkcs_pad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]}],"conclusion":"∃ r,\n  block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_unpad b =\n      Aeneas.Std.Result.ok r ∧\n    match r with\n    | Aeneas.Std.core.result.Result.Ok out =>\n      ∃ p,\n        BlockPadding.UnpadProof.bytes out = List.take p (BlockPadding.UnpadProof.bytes b) ∧\n          BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.iso7816 (BlockPadding.UnpadProof.bytes b) p\n    | Aeneas.Std.core.result.Result.Err a =>\n      BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.iso7816 (BlockPadding.UnpadProof.bytes b)","conclusion_segments":[{"text":"∃ "},{"text":"r"},{"text":",\n  "},{"ref":"block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_unpad","text":"block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_unpad"},{"text":" "},{"text":"b"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"r"},{"ref":"And","text":" ∧\n    "},{"text":"match "},{"text":"r"},{"text":" with\n    | "},{"ref":"Aeneas.Std.core.result.Result.Ok","text":"Aeneas.Std.core.result.Result.Ok"},{"text":" "},{"text":"out"},{"text":" =>\n      "},{"text":"∃ "},{"text":"p"},{"text":",\n        "},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"p"},{"text":" "},{"text":"("},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"ref":"And","text":" ∧\n          "},{"ref":"BlockPadding.Spec.Accepted","text":"BlockPadding.Spec.Accepted"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.iso7816","text":"BlockPadding.Spec.Algorithm.iso7816"},{"text":" "},{"text":"("},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"p"},{"text":"\n    | "},{"ref":"Aeneas.Std.core.result.Result.Err","text":"Aeneas.Std.core.result.Result.Err"},{"text":" "},{"text":"a"},{"text":" =>\n      "},{"ref":"BlockPadding.Spec.Rejected","text":"BlockPadding.Spec.Rejected"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.iso7816","text":"BlockPadding.Spec.Algorithm.iso7816"},{"text":" "},{"text":"("},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"b"},{"text":")"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result","source":{"first_line":7,"last_line":10}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Error","source":{"first_line":37,"last_line":41}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_unpad","source":{"first_line":357,"last_line":370}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"UnpadProofs","name":"BlockPadding.UnpadProof.iso_loop.match_1","source":null},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"UnpadProofs","name":"BlockPadding.UnpadProof.bytes","source":{"first_line":8,"last_line":8}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Accepted","source":{"first_line":41,"last_line":58}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.iso7816","source":{"first_line":9,"last_line":9}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Rejected","source":{"first_line":60,"last_line":60}}],"definitions_truncated":false,"first_line":263,"last_line":269,"module":"UnpadProofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8),\n  @Exists.{1}\n    (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) block_padding_verification_api.Error)\n    fun\n      (r :\n        Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n          block_padding_verification_api.Error) =>\n    And\n      (@Eq.{1}\n        (Aeneas.Std.Result.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error))\n        (block_padding_verification_api.Iso7816.Insts.Block_padding_verification_apiPadding.raw_unpad b)\n        (@Aeneas.Std.Result.ok.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error)\n          r))\n      (BlockPadding.UnpadProof.iso_loop.match_1.{1}\n        (fun\n            (r :\n              Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n                block_padding_verification_api.Error) =>\n          Prop)\n        r\n        (fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n          @Exists.{1} Nat fun (p : Nat) =>\n            And\n              (@Eq.{1} (List.{0} Nat) (BlockPadding.UnpadProof.bytes out)\n                (@List.take.{0} Nat p (BlockPadding.UnpadProof.bytes b)))\n              (BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.iso7816 (BlockPadding.UnpadProof.bytes b) p))\n        fun (a : block_padding_verification_api.Error) =>\n        BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.iso7816 (BlockPadding.UnpadProof.bytes b))","theorem":"BlockPadding.UnpadProof.iso_unpad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"hypothesis","name":"hpos","type":"0 < b.length","type_segments":[{"text":"0"},{"ref":"LT.lt","text":" < "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]},{"binder":"explicit","kind":"hypothesis","name":"hb","type":"b.length ≤ 255","type_segments":[{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"},{"ref":"LE.le","text":" ≤ "},{"text":"255"}]}],"conclusion":"∃ r,\n  block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_unpad b =\n      Aeneas.Std.Result.ok r ∧\n    match r with\n    | Aeneas.Std.core.result.Result.Ok out =>\n      ∃ p,\n        BlockPadding.Proof.bytes out = List.take p (BlockPadding.Proof.bytes b) ∧\n          BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.iso10126 (BlockPadding.Proof.bytes b) p\n    | Aeneas.Std.core.result.Result.Err a =>\n      BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.iso10126 (BlockPadding.Proof.bytes b)","conclusion_segments":[{"text":"∃ "},{"text":"r"},{"text":",\n  "},{"ref":"block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_unpad","text":"block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_unpad"},{"text":" "},{"text":"b"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"r"},{"ref":"And","text":" ∧\n    "},{"text":"match "},{"text":"r"},{"text":" with\n    | "},{"ref":"Aeneas.Std.core.result.Result.Ok","text":"Aeneas.Std.core.result.Result.Ok"},{"text":" "},{"text":"out"},{"text":" =>\n      "},{"text":"∃ "},{"text":"p"},{"text":",\n        "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"p"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"ref":"And","text":" ∧\n          "},{"ref":"BlockPadding.Spec.Accepted","text":"BlockPadding.Spec.Accepted"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.iso10126","text":"BlockPadding.Spec.Algorithm.iso10126"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"p"},{"text":"\n    | "},{"ref":"Aeneas.Std.core.result.Result.Err","text":"Aeneas.Std.core.result.Result.Err"},{"text":" "},{"text":"a"},{"text":" =>\n      "},{"ref":"BlockPadding.Spec.Rejected","text":"BlockPadding.Spec.Rejected"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.iso10126","text":"BlockPadding.Spec.Algorithm.iso10126"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Prelude","name":"LT.lt","source":{"first_line":1407,"last_line":1407}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLTNat","source":{"first_line":2037,"last_line":2038}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result","source":{"first_line":7,"last_line":10}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Error","source":{"first_line":37,"last_line":41}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_unpad","source":{"first_line":208,"last_line":215}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"CountUnpadProofs","name":"BlockPadding.CountUnpadProof.pkcs_loop.match_1","source":null},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Accepted","source":{"first_line":41,"last_line":58}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.iso10126","source":{"first_line":9,"last_line":9}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Rejected","source":{"first_line":60,"last_line":60}}],"definitions_truncated":false,"first_line":221,"last_line":228,"module":"CountUnpadProofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n  (hpos :\n    @LT.lt.{0} Nat instLTNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b))\n  (hb :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)\n      (@OfNat.ofNat.{0} Nat (nat_lit 255) (instOfNatNat (nat_lit 255)))),\n  @Exists.{1}\n    (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) block_padding_verification_api.Error)\n    fun\n      (r :\n        Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n          block_padding_verification_api.Error) =>\n    And\n      (@Eq.{1}\n        (Aeneas.Std.Result.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error))\n        (block_padding_verification_api.Iso10126.Insts.Block_padding_verification_apiPadding.raw_unpad b)\n        (@Aeneas.Std.Result.ok.{0}\n          (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n            block_padding_verification_api.Error)\n          r))\n      (BlockPadding.CountUnpadProof.pkcs_loop.match_1.{1}\n        (fun\n            (r :\n              Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n                block_padding_verification_api.Error) =>\n          Prop)\n        r\n        (fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n          @Exists.{1} Nat fun (p : Nat) =>\n            And\n              (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n                (@List.take.{0} Nat p (BlockPadding.Proof.bytes b)))\n              (BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.iso10126 (BlockPadding.Proof.bytes b) p))\n        fun (a : block_padding_verification_api.Error) =>\n        BlockPadding.Spec.Rejected BlockPadding.Spec.Algorithm.iso10126 (BlockPadding.Proof.bytes b))","theorem":"BlockPadding.CountUnpadProof.iso10126_unpad_total","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"p","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"↑p ≤ b.length","type_segments":[{"text":"↑"},{"text":"p"},{"ref":"LE.le","text":" ≤ "},{"text":"b"},{"text":"."},{"ref":"Aeneas.Std.Slice.length","text":"length"}]}],"conclusion":"∃ out,\n  block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_pad b p =\n      Aeneas.Std.Result.ok out ∧\n    BlockPadding.Proof.bytes out =\n      BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.none (BlockPadding.Proof.bytes b) ↑p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_pad","text":"block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_pad"},{"text":" "},{"text":"b"},{"text":" "},{"text":"p"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" =\n      "},{"ref":"BlockPadding.Spec.Padded","text":"BlockPadding.Spec.Padded"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.none","text":"BlockPadding.Spec.Algorithm.none"},{"text":" "},{"text":"("},{"ref":"BlockPadding.Proof.bytes","text":"BlockPadding.Proof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"↑"},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Init.Prelude","name":"LE.le","source":{"first_line":1402,"last_line":1402}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instLENat","source":{"first_line":2026,"last_line":2027}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalar.val","source":{"first_line":76,"last_line":76}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.UScalarTy.Usize","source":{"first_line":32,"last_line":32}},{"module":"Aeneas.Std.Slice","name":"Aeneas.Std.Slice.length","source":{"first_line":34,"last_line":35}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_pad","source":{"first_line":372,"last_line":379}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Proofs","name":"BlockPadding.Proof.bytes","source":{"first_line":8,"last_line":8}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Padded","source":{"first_line":20,"last_line":28}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.none","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":17,"last_line":22,"module":"Proofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8) (p : Aeneas.Std.Usize)\n  (h :\n    @LE.le.{0} Nat instLENat (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)\n      (@Aeneas.Std.Slice.length.{0} Aeneas.Std.U8 b)),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8))\n        (block_padding_verification_api.NoPadding.Insts.Block_padding_verification_apiPadding.raw_pad b p)\n        (@Aeneas.Std.Result.ok.{0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) out))\n      (@Eq.{1} (List.{0} Nat) (BlockPadding.Proof.bytes out)\n        (BlockPadding.Spec.Padded BlockPadding.Spec.Algorithm.none (BlockPadding.Proof.bytes b)\n          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize p)))","theorem":"BlockPadding.Proof.no_pad","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"b","type":"Aeneas.Std.Slice Aeneas.Std.U8","type_segments":[{"ref":"Aeneas.Std.Slice","text":"Aeneas.Std.Slice"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]}],"conclusion":"∃ out p,\n  block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_unpad b =\n      Aeneas.Std.Result.ok (Aeneas.Std.core.result.Result.Ok out) ∧\n    BlockPadding.UnpadProof.bytes out = List.take p (BlockPadding.UnpadProof.bytes b) ∧\n      BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.zero (BlockPadding.UnpadProof.bytes b) p","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":" "},{"text":"p"},{"text":",\n  "},{"ref":"block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_unpad","text":"block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_unpad"},{"text":" "},{"text":"b"},{"ref":"Eq","text":" =\n      "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"("},{"ref":"Aeneas.Std.core.result.Result.Ok","text":"Aeneas.Std.core.result.Result.Ok"},{"text":" "},{"text":"out"},{"text":")"},{"ref":"And","text":" ∧\n    "},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"p"},{"text":" "},{"text":"("},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"ref":"And","text":" ∧\n      "},{"ref":"BlockPadding.Spec.Accepted","text":"BlockPadding.Spec.Accepted"},{"text":" "},{"ref":"BlockPadding.Spec.Algorithm.zero","text":"BlockPadding.Spec.Algorithm.zero"},{"text":" "},{"text":"("},{"ref":"BlockPadding.UnpadProof.bytes","text":"BlockPadding.UnpadProof.bytes"},{"text":" "},{"text":"b"},{"text":")"},{"text":" "},{"text":"p"}],"definitions":[{"module":"Aeneas.Std.SliceDef","name":"Aeneas.Std.Slice","source":{"first_line":15,"last_line":19}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result","source":{"first_line":7,"last_line":10}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.Error","source":{"first_line":37,"last_line":41}},{"module":"BlockPaddingVerificationApi","name":"block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_unpad","source":{"first_line":91,"last_line":107}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Aeneas.Std.Core.Result","name":"Aeneas.Std.core.result.Result.Ok","source":{"first_line":9,"last_line":9}},{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"UnpadProofs","name":"BlockPadding.UnpadProof.bytes","source":{"first_line":8,"last_line":8}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Accepted","source":{"first_line":41,"last_line":58}},{"module":"BlockPadding.Specs","name":"BlockPadding.Spec.Algorithm.zero","source":{"first_line":9,"last_line":9}}],"definitions_truncated":false,"first_line":256,"last_line":261,"module":"UnpadProofs","program":null,"program_head":null,"statement":"∀ (b : Aeneas.Std.Slice.{0} Aeneas.Std.U8),\n  @Exists.{1} (Aeneas.Std.Slice.{0} Aeneas.Std.U8) fun (out : Aeneas.Std.Slice.{0} Aeneas.Std.U8) =>\n    @Exists.{1} Nat fun (p : Nat) =>\n      And\n        (@Eq.{1}\n          (Aeneas.Std.Result.{0}\n            (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n              block_padding_verification_api.Error))\n          (block_padding_verification_api.ZeroPadding.Insts.Block_padding_verification_apiPadding.raw_unpad b)\n          (@Aeneas.Std.Result.ok.{0}\n            (Aeneas.Std.core.result.Result.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n              block_padding_verification_api.Error)\n            (@Aeneas.Std.core.result.Result.Ok.{0, 0} (Aeneas.Std.Slice.{0} Aeneas.Std.U8)\n              block_padding_verification_api.Error out)))\n        (And\n          (@Eq.{1} (List.{0} Nat) (BlockPadding.UnpadProof.bytes out)\n            (@List.take.{0} Nat p (BlockPadding.UnpadProof.bytes b)))\n          (BlockPadding.Spec.Accepted BlockPadding.Spec.Algorithm.zero (BlockPadding.UnpadProof.bytes b) p))","theorem":"BlockPadding.UnpadProof.zero_unpad_total","translation_rerun":false,"version":1}

=== stderr ===

Environment

The managed default profile passed on aarch64-apple-darwin using extraction Rust nightly-2026-09-17, native Rust 1.91.1, Lean 4.35.0, Aeneas be86ab0f and Charon 08d7c9d; the full revisions are in the workspace tool lock. Aeneas and Charon are unpatched. The run checked the twelve named public-model theorems and their registered helpers, regenerated the selected model, and checked the derived source. The coverage ledger records the run and remaining work. Charon fell back to rustc's default sysroot after Miri sysroot setup failed.

Publication used the service-supported recorded-API fallback after the server rustdoc import failed with unresolved_public_reexport. API bindings originate from the recorded run, not an independent rustdoc catalogue; missing rustdoc signatures or safety metadata are not inferred. The original SARIF is unchanged.

What is trusted

The claims rely on the pinned Charon and Aeneas translation, their Rust slice and integer models, and the Lean kernel. Source correspondence is based on review rather than a formal equivalence proof. The two decoder iterator checks were rewritten as explicit loops in the verification harness: each scans the same suffix and rejects upon the first byte that differs from the required value. This source reasoning has been independently reviewed, but equivalence of the adapted bodies to the published release has not been formally proved.

Technical limitations

These are selected raw-method contracts, not verification of the entire crate. They do not establish behavior outside the stated domains or prove the panic boundaries. Typed array methods, detached padding, block-list unpadding, and the hybrid-array representation bridge remain unproved. Generic extraction attempts encountered translation or model boundaries; these attempts do not establish that verification is impossible. Native tests are separate from the formal claims. In particular, empty input causes three raw decoders to panic despite the trait documentation's malformed-padding error statement, as described in the finding.

Tool limitations

Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Dependencies (1)

CrateReports

hybrid-array ^0.4.3—

Comments (0)

No comments.