Recorded run

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)

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 ===