inductive reasoning & reference counting

Stream: new members

[Alex Mobius]

Good day, unfortunately don't have an #nwe since this is an advance worry, but bsically, I'm designing an algorithm (based on DFS) nad based on what I've read in the libs, I came up with the following structure:

namespace TLState
structure Raw where
  .. -- a bunch of vectors

structure SmallStepWF (state: Raw): Prop where
  .. -- a bunch of invariants

def small_step_raw (..params..): StateM Raw VLabel := ...

def SmallStepState := {state: Raw // SmallStepWF state}

def small_step (..params..): StateM SmallStepState VLabel
  | .mk state, wf => let state := small_step_raw params.. state; let wf1 := by ...; .mk state1, wf1
end TLState

I'm worrying that this introduces additional references to my state, and therefore the access stops being linear and there's a bunch of copying going on. Am I correct in my assumptions? How would I proceed to avoid that?