DropBug.lean

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [drop_bug]
import Aeneas
open Aeneas Aeneas.Std Result ControlFlow Error
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
set_option maxHeartbeats 1000000

/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
set_option maxRecDepth 2048

/- You can remove the following line by using the CLI option `-all-computable`: -/
noncomputable section

namespace drop_bug

/-- Trait declaration: [core::ops::drop::Drop]
    Source: '/rustc/library/core/src/ops/drop.rs', lines 209:0-209:20
    Name pattern: [core::ops::drop::Drop]
    Visibility: public -/
@[rust_trait "core::ops::drop::Drop"]
structure core.ops.drop.Drop (Self : Type) where
  drop : Self → Result Self

/-- [core::ops::drop::Drop::drop]:
    Source: '/rustc/library/core/src/ops/drop.rs', lines 243:4-243:22
    Name pattern: [core::ops::drop::Drop::drop]
    Visibility: public -/
@[rust_fun "core::ops::drop::Drop::drop"]
axiom core.ops.drop.Drop.drop.default
  {Self : Type} (DropInst : core.ops.drop.Drop Self) : Self → Result Self

/-- [drop_bug::wipe_slice]:
    Source: 'tests/src/drop_bug.rs', lines 20:0-24:1 -/
axiom wipe_slice {T : Type} : Slice T → Result (Slice T)

/-- [drop_bug::Inner]
    Source: 'tests/src/drop_bug.rs', lines 26:0-28:1 -/
structure Inner where
  buf : Array Std.U8 4#usize

/-- [drop_bug::{impl core::ops::drop::Drop for drop_bug::Inner}::drop]:
    Source: 'tests/src/drop_bug.rs', lines 31:4-33:5
    Visibility: public -/
def Inner.Insts.CoreOpsDropDrop.drop (self : Inner) : Result Inner := do
  let (s, to_slice_mut_back) ← lift (Array.to_slice_mut self.buf)
  let s1 ← wipe_slice s
  let a := to_slice_mut_back s1
  ok { buf := a }

/-- Trait implementation: [drop_bug::{impl core::ops::drop::Drop for drop_bug::Inner}]
    Source: 'tests/src/drop_bug.rs', lines 30:0-34:1 -/
@[reducible]
def Inner.Insts.CoreOpsDropDrop : core.ops.drop.Drop Inner := {
  drop := Inner.Insts.CoreOpsDropDrop.drop
}

/-- [drop_bug::{drop_bug::Inner}::init]:
    Source: 'tests/src/drop_bug.rs', lines 37:4-39:5 -/
def Inner.init
  (self : Inner) (block_size : Std.U32) (pad_value : Std.U8) :
  Result Inner
  := do
  let (s, to_slice_mut_back) ← lift (Array.to_slice_mut self.buf)
  let s1 ← wipe_slice s
  let a := to_slice_mut_back s1
  ok { buf := a }

/-- [drop_bug::Outer]
    Source: 'tests/src/drop_bug.rs', lines 42:0-46:1 -/
structure Outer where
  inner : Inner
  block_size : Std.U32
  pad_value : Std.U8

/-- [drop_bug::{drop_bug::Outer}::get_block_size]:
    Source: 'tests/src/drop_bug.rs', lines 49:4-51:5 -/
def Outer.get_block_size (self : Outer) : Result Std.U32 := do
  ok self.block_size

/-- [drop_bug::{drop_bug::Outer}::get_pad_value]:
    Source: 'tests/src/drop_bug.rs', lines 53:4-55:5 -/
def Outer.get_pad_value (self : Outer) : Result Std.U8 := do
  ok self.pad_value

/-- [drop_bug::{drop_bug::Outer}::init]:
    Source: 'tests/src/drop_bug.rs', lines 60:4-62:5 -/
def Outer.init (self : Outer) : Result Outer := do
  let i ← Outer.get_block_size self
  let i1 ← Outer.get_pad_value self
  let i2 ← Inner.init self.inner i i1
  ok { self with inner := i2 }

/-- [drop_bug::InnerNoDrop]
    Source: 'tests/src/drop_bug.rs', lines 67:0-69:1 -/
structure InnerNoDrop where
  buf : Array Std.U8 4#usize

/-- [drop_bug::{drop_bug::InnerNoDrop}::init]:
    Source: 'tests/src/drop_bug.rs', lines 72:4-74:5 -/
def InnerNoDrop.init
  (self : InnerNoDrop) (block_size : Std.U32) (pad_value : Std.U8) :
  Result InnerNoDrop
  := do
  let (s, to_slice_mut_back) ← lift (Array.to_slice_mut self.buf)
  let s1 ← wipe_slice s
  let a := to_slice_mut_back s1
  ok { buf := a }

/-- [drop_bug::OuterNoDrop]
    Source: 'tests/src/drop_bug.rs', lines 77:0-81:1 -/
structure OuterNoDrop where
  inner : InnerNoDrop
  block_size : Std.U32
  pad_value : Std.U8

/-- [drop_bug::{drop_bug::OuterNoDrop}::get_block_size]:
    Source: 'tests/src/drop_bug.rs', lines 84:4-86:5 -/
def OuterNoDrop.get_block_size (self : OuterNoDrop) : Result Std.U32 := do
  ok self.block_size

/-- [drop_bug::{drop_bug::OuterNoDrop}::get_pad_value]:
    Source: 'tests/src/drop_bug.rs', lines 88:4-90:5 -/
def OuterNoDrop.get_pad_value (self : OuterNoDrop) : Result Std.U8 := do
  ok self.pad_value

/-- [drop_bug::{drop_bug::OuterNoDrop}::init]:
    Source: 'tests/src/drop_bug.rs', lines 92:4-94:5 -/
def OuterNoDrop.init (self : OuterNoDrop) : Result OuterNoDrop := do
  let i ← OuterNoDrop.get_block_size self
  let i1 ← OuterNoDrop.get_pad_value self
  let ind ← InnerNoDrop.init self.inner i i1
  ok { self with inner := ind }

end drop_bug