proofs.rs

Recorded run

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/keiichiw/crate-proofs report-8-source-1
git -C report-8-source-1 checkout --detach 3785357a67f63cc5c25005cdbc8684b20390d5a3
git -C report-8-source-1 submodule update --init --recursive --checkout
cd report-8-source-1/bytes/1.12.1/.work/build/unpatched/aarch64-apple-darwin/proofs

lake build +Proofs.Take

printf '%s' 'import Aeneas
import Proofs.Take
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 := #[`bytes.take_into_inner_spec, `bytes.take_get_ref_spec, `bytes.take_get_mut_spec, `bytes.take_limit_spec, `bytes.take_set_limit_spec]
  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 := `bytes.take_get_mut_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: bytes.take_get_mut_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in bytes.take_get_mut_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:bytes.take_get_mut_spec"

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

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

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

run_cmd do
  let theorem_name := `bytes.take_set_limit_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: bytes.take_set_limit_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in bytes.take_set_limit_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:bytes.take_set_limit_spec"
' | 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 · 5 checks passed · 0 failed

2026-10-25T07:05:11.216299+00:00 · 37.9 seconds · Exit code 0

Recorded on the author’s machine.

CheckResultClaim
Lean checked theorem bytes.take_get_mut_spec; axioms limited to propext, Classical.choice, Quot.sound
bytes.take_get_mut_spec
PassedClaim #1
Lean checked theorem bytes.take_get_ref_spec; axioms limited to propext, Classical.choice, Quot.sound
bytes.take_get_ref_spec
PassedClaim #2
Lean checked theorem bytes.take_into_inner_spec; axioms limited to propext, Classical.choice, Quot.sound
bytes.take_into_inner_spec
PassedClaim #3
Lean checked theorem bytes.take_limit_spec; axioms limited to propext, Classical.choice, Quot.sound
bytes.take_limit_spec
PassedClaim #4
Lean checked theorem bytes.take_set_limit_spec; axioms limited to propext, Classical.choice, Quot.sound
bytes.take_set_limit_spec
PassedClaim #5
Execution details
Started
2026-10-25T07:05:11.216299+00:00
Finished
2026-10-25T07:05:49.073995+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
bytes/1.12.1/.work/build/unpatched/aarch64-apple-darwin/proofs
Environment overrides
None recorded
Git repository
https://github.com/keiichiw/crate-proofs
Git commit
3785357a67f63cc5c25005cdbc8684b20390d5a3
Diagnostics & logs
=== stdout ===
✔ [1796/1797] Built Bytes (7.6s)
✔ [1797/1797] Built Proofs.Take (8.2s)
Build completed successfully (1797 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"view","type":"T → List Aeneas.Std.U8","type_segments":[{"text":"T"},{"text":" → "},{"ref":"List","text":"List"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"s","type":"bytes.buf.take.Take T","type_segments":[{"ref":"bytes.buf.take.Take","text":"bytes.buf.take.Take"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"lim","type":"Aeneas.Std.Usize","type_segments":[{"ref":"Aeneas.Std.Usize","text":"Aeneas.Std.Usize"}]}],"conclusion":"∃ out,\n  s.set_limit lim = Aeneas.Std.Result.ok out ∧\n    out.inner = s.inner ∧ out.limit = lim ∧ bytes.visible view out = List.take (↑lim) (view s.inner)","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.set_limit","text":"set_limit"},{"text":" "},{"text":"lim"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"text":"out"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"},{"ref":"Eq","text":" = "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"},{"ref":"And","text":" ∧ "},{"text":"out"},{"text":"."},{"ref":"bytes.buf.take.Take.limit","text":"limit"},{"ref":"Eq","text":" = "},{"text":"lim"},{"ref":"And","text":" ∧ "},{"ref":"bytes.visible","text":"bytes.visible"},{"text":" "},{"text":"view"},{"text":" "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"(↑"},{"text":"lim"},{"text":")"},{"text":" "},{"text":"("},{"text":"view"},{"text":" "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"},{"text":")"}],"definitions":[{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Bytes","name":"bytes.buf.take.Take","source":{"first_line":23,"last_line":28}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"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":"Bytes","name":"bytes.buf.take.Take.set_limit","source":{"first_line":61,"last_line":68}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bytes","name":"bytes.buf.take.Take.inner","source":{"first_line":27,"last_line":27}},{"module":"Bytes","name":"bytes.buf.take.Take.limit","source":{"first_line":28,"last_line":28}},{"module":"Proofs.Take","name":"bytes.visible","source":{"first_line":6,"last_line":7}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"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}}],"definitions_truncated":false,"first_line":21,"last_line":24,"module":"Proofs.Take","program":null,"program_head":null,"statement":"∀ {T : Type u_1} (view : T → List.{0} Aeneas.Std.U8) (s : bytes.buf.take.Take.{u_1} T) (lim : Aeneas.Std.Usize),\n  @Exists.{u_1 + 1} (bytes.buf.take.Take.{u_1} T) fun (out : bytes.buf.take.Take.{u_1} T) =>\n    And\n      (@Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (bytes.buf.take.Take.{u_1} T))\n        (@bytes.buf.take.Take.set_limit.{u_1} T s lim) (@Aeneas.Std.Result.ok.{u_1} (bytes.buf.take.Take.{u_1} T) out))\n      (And (@Eq.{u_1 + 1} T (@bytes.buf.take.Take.inner.{u_1} T out) (@bytes.buf.take.Take.inner.{u_1} T s))\n        (And (@Eq.{1} Aeneas.Std.Usize (@bytes.buf.take.Take.limit.{u_1} T out) lim)\n          (@Eq.{1} (List.{0} Aeneas.Std.U8) (@bytes.visible.{u_1} T view out)\n            (@List.take.{0} Aeneas.Std.U8 (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize lim)\n              (view (@bytes.buf.take.Take.inner.{u_1} T s))))))","theorem":"bytes.take_set_limit_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"s","type":"bytes.buf.take.Take T","type_segments":[{"ref":"bytes.buf.take.Take","text":"bytes.buf.take.Take"},{"text":" "},{"text":"T"}]}],"conclusion":"∃ out, s.into_inner = Aeneas.Std.Result.ok out ∧ out = s.inner","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.into_inner","text":"into_inner"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"}],"definitions":[{"module":"Bytes","name":"bytes.buf.take.Take","source":{"first_line":23,"last_line":28}},{"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":"Bytes","name":"bytes.buf.take.Take.into_inner","source":{"first_line":30,"last_line":35}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bytes","name":"bytes.buf.take.Take.inner","source":{"first_line":27,"last_line":27}}],"definitions_truncated":false,"first_line":9,"last_line":11,"module":"Proofs.Take","program":null,"program_head":null,"statement":"∀ {T : Type u_1} (s : bytes.buf.take.Take.{u_1} T),\n  @Exists.{u_1 + 1} T fun (out : T) =>\n    And\n      (@Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} T) (@bytes.buf.take.Take.into_inner.{u_1} T s)\n        (@Aeneas.Std.Result.ok.{u_1} T out))\n      (@Eq.{u_1 + 1} T out (@bytes.buf.take.Take.inner.{u_1} T s))","theorem":"bytes.take_into_inner_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"view","type":"T → List Aeneas.Std.U8","type_segments":[{"text":"T"},{"text":" → "},{"ref":"List","text":"List"},{"text":" "},{"ref":"Aeneas.Std.U8","text":"Aeneas.Std.U8"}]},{"binder":"explicit","kind":"variable","name":"s","type":"bytes.buf.take.Take T","type_segments":[{"ref":"bytes.buf.take.Take","text":"bytes.buf.take.Take"},{"text":" "},{"text":"T"}]}],"conclusion":"∃ out,\n  s.get_mut = Aeneas.Std.Result.ok out ∧\n    out.1 = s.inner ∧\n      ∀ (replacement : T),\n        (out.2 replacement).inner = replacement ∧\n          (out.2 replacement).limit = s.limit ∧\n            bytes.visible view (out.2 replacement) = List.take (↑s.limit) (view replacement)","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.get_mut","text":"get_mut"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"text":"out"},{"text":".1"},{"ref":"Eq","text":" = "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"},{"ref":"And","text":" ∧\n      "},{"text":"∀ ("},{"text":"replacement"},{"text":" : "},{"text":"T"},{"text":"),\n        "},{"text":"("},{"text":"out"},{"text":".2"},{"text":" "},{"text":"replacement"},{"text":")"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"},{"ref":"Eq","text":" = "},{"text":"replacement"},{"ref":"And","text":" ∧\n          "},{"text":"("},{"text":"out"},{"text":".2"},{"text":" "},{"text":"replacement"},{"text":")"},{"text":"."},{"ref":"bytes.buf.take.Take.limit","text":"limit"},{"ref":"Eq","text":" = "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.limit","text":"limit"},{"ref":"And","text":" ∧\n            "},{"ref":"bytes.visible","text":"bytes.visible"},{"text":" "},{"text":"view"},{"text":" "},{"text":"("},{"text":"out"},{"text":".2"},{"text":" "},{"text":"replacement"},{"text":")"},{"ref":"Eq","text":" = "},{"ref":"List.take","text":"List.take"},{"text":" "},{"text":"(↑"},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.limit","text":"limit"},{"text":")"},{"text":" "},{"text":"("},{"text":"view"},{"text":" "},{"text":"replacement"},{"text":")"}],"definitions":[{"module":"Init.Prelude","name":"List","source":{"first_line":3096,"last_line":3115}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Bytes","name":"bytes.buf.take.Take","source":{"first_line":23,"last_line":28}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"Prod","source":{"first_line":603,"last_line":618}},{"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":"Bytes","name":"bytes.buf.take.Take.get_mut","source":{"first_line":44,"last_line":52}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Prelude","name":"Prod.fst","source":{"first_line":616,"last_line":616}},{"module":"Bytes","name":"bytes.buf.take.Take.inner","source":{"first_line":27,"last_line":27}},{"module":"Init.Prelude","name":"Prod.snd","source":{"first_line":618,"last_line":618}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"module":"Bytes","name":"bytes.buf.take.Take.limit","source":{"first_line":28,"last_line":28}},{"module":"Proofs.Take","name":"bytes.visible","source":{"first_line":6,"last_line":7}},{"module":"Init.Data.List.Basic","name":"List.take","source":{"first_line":893,"last_line":906}},{"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}}],"definitions_truncated":false,"first_line":26,"last_line":32,"module":"Proofs.Take","program":null,"program_head":null,"statement":"∀ {T : Type u_1} (view : T → List.{0} Aeneas.Std.U8) (s : bytes.buf.take.Take.{u_1} T),\n  @Exists.{u_1 + 1} (Prod.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T))\n    fun (out : Prod.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T)) =>\n    And\n      (@Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} (Prod.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T)))\n        (@bytes.buf.take.Take.get_mut.{u_1} T s)\n        (@Aeneas.Std.Result.ok.{u_1} (Prod.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T)) out))\n      (And\n        (@Eq.{u_1 + 1} T (@Prod.fst.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T) out)\n          (@bytes.buf.take.Take.inner.{u_1} T s))\n        (∀ (replacement : T),\n          And\n            (@Eq.{u_1 + 1} T\n              (@bytes.buf.take.Take.inner.{u_1} T\n                (@Prod.snd.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T) out replacement))\n              replacement)\n            (And\n              (@Eq.{1} Aeneas.Std.Usize\n                (@bytes.buf.take.Take.limit.{u_1} T\n                  (@Prod.snd.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T) out replacement))\n                (@bytes.buf.take.Take.limit.{u_1} T s))\n              (@Eq.{1} (List.{0} Aeneas.Std.U8)\n                (@bytes.visible.{u_1} T view (@Prod.snd.{u_1, u_1} T (T → bytes.buf.take.Take.{u_1} T) out replacement))\n                (@List.take.{0} Aeneas.Std.U8\n                  (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.Usize (@bytes.buf.take.Take.limit.{u_1} T s))\n                  (view replacement))))))","theorem":"bytes.take_get_mut_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"s","type":"bytes.buf.take.Take T","type_segments":[{"ref":"bytes.buf.take.Take","text":"bytes.buf.take.Take"},{"text":" "},{"text":"T"}]}],"conclusion":"∃ out, bytes.buf.take.Take.impl.limit s = Aeneas.Std.Result.ok out ∧ out = s.limit","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"bytes.buf.take.Take.impl.limit","text":"bytes.buf.take.Take.impl.limit"},{"text":" "},{"text":"s"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.limit","text":"limit"}],"definitions":[{"module":"Bytes","name":"bytes.buf.take.Take","source":{"first_line":23,"last_line":28}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize","source":{"first_line":668,"last_line":668}},{"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":"Bytes","name":"bytes.buf.take.Take.impl.limit","source":{"first_line":54,"last_line":59}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bytes","name":"bytes.buf.take.Take.limit","source":{"first_line":28,"last_line":28}}],"definitions_truncated":false,"first_line":17,"last_line":19,"module":"Proofs.Take","program":null,"program_head":null,"statement":"∀ {T : Type u_1} (s : bytes.buf.take.Take.{u_1} T),\n  @Exists.{1} Aeneas.Std.Usize fun (out : Aeneas.Std.Usize) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.Usize) (@bytes.buf.take.Take.impl.limit.{u_1} T s)\n        (@Aeneas.Std.Result.ok.{0} Aeneas.Std.Usize out))\n      (@Eq.{1} Aeneas.Std.Usize out (@bytes.buf.take.Take.limit.{u_1} T s))","theorem":"bytes.take_limit_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"explicit","kind":"variable","name":"s","type":"bytes.buf.take.Take T","type_segments":[{"ref":"bytes.buf.take.Take","text":"bytes.buf.take.Take"},{"text":" "},{"text":"T"}]}],"conclusion":"∃ out, s.get_ref = Aeneas.Std.Result.ok out ∧ out = s.inner","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.get_ref","text":"get_ref"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"s"},{"text":"."},{"ref":"bytes.buf.take.Take.inner","text":"inner"}],"definitions":[{"module":"Bytes","name":"bytes.buf.take.Take","source":{"first_line":23,"last_line":28}},{"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":"Bytes","name":"bytes.buf.take.Take.get_ref","source":{"first_line":37,"last_line":42}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Bytes","name":"bytes.buf.take.Take.inner","source":{"first_line":27,"last_line":27}}],"definitions_truncated":false,"first_line":13,"last_line":15,"module":"Proofs.Take","program":null,"program_head":null,"statement":"∀ {T : Type u_1} (s : bytes.buf.take.Take.{u_1} T),\n  @Exists.{u_1 + 1} T fun (out : T) =>\n    And\n      (@Eq.{u_1 + 1} (Aeneas.Std.Result.{u_1} T) (@bytes.buf.take.Take.get_ref.{u_1} T s)\n        (@Aeneas.Std.Result.ok.{u_1} T out))\n      (@Eq.{u_1 + 1} T out (@bytes.buf.take.Take.inner.{u_1} T s))","theorem":"bytes.take_get_ref_spec","translation_rerun":false,"version":1}

=== stderr ===