Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.DenseOverlay.Internal

Dense public input with a sparse mutable overlay -- proof internals #

source
theorem Complexity.RAM.RegisterStore.DenseOverlay.read_empty_internal (input : List Bool) (address : ℕ) :
read input [] address = initRegs input address
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.read_write_internal (input : List Bool) (overlay : Store) (hcanonical : Canonical overlay) (address value : ℕ) :
read input (write overlay address value) = Function.update (read input overlay) address value
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.write_canonical_internal (overlay : Store) (hcanonical : Canonical overlay) (address value : ℕ) :
Canonical (write overlay address value)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.write_coversZero_internal (overlay : Store) (hcanonical : Canonical overlay) (hcovers : CoversZero overlay) (address value : ℕ) :
CoversZero (write overlay address value)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_decode_internal (input : List Bool) :
decode input (initial input) = initCfg input
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_canonical_internal (input : List Bool) :
Canonical (initial input).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_coversZero_internal (input : List Bool) :
CoversZero (initial input).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_valid_internal (input : List Bool) :
Valid (initial input).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode_stepInstr_internal (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
decode input (stepInstr input instruction snapshot) = RAM.stepInstr instruction (decode input snapshot)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr_canonical_internal (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
Canonical (stepInstr input instruction snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr_coversZero_internal (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) :
CoversZero (stepInstr input instruction snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr_valid_internal (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) :
Valid (stepInstr input instruction snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode_step_internal (program : Program) (input : List Bool) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
decode input (step program input snapshot) = RAM.step program (decode input snapshot)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.step_canonical_internal (program : Program) (input : List Bool) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
Canonical (step program input snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.step_valid_internal (program : Program) (input : List Bool) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) :
Valid (step program input snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode_run_internal (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
decode input (run program input fuel snapshot) = RAM.run program fuel (decode input snapshot)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.run_canonical_internal (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
Canonical (run program input fuel snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.run_valid_internal (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) :
Valid (run program input fuel snapshot).overlay
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.write_length_le_internal (overlay : Store) (address value : ℕ) :
List.length (write overlay address value) ≤ List.length overlay + 1
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.length_stepInstr_le_internal (input : List Bool) (instruction : Instr) (snapshot : Snapshot) :
List.length (stepInstr input instruction snapshot).overlay ≤ List.length snapshot.overlay + 1
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.length_run_le_internal (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
List.length (run program input fuel snapshot).overlay ≤ List.length snapshot.overlay + unitTimeUpto program fuel (decode input snapshot)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.encodedStoreLength_write_le_internal (overlay : Store) (address value : ℕ) :
encodedStoreLength (write overlay address value) ≤ encodedStoreLength overlay + (Entry.encode (address, value + 1)).length
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.encodedStoreLength_stepInstr_le_internal (input : List Bool) (instruction : Instr) (snapshot : Snapshot) :
encodedStoreLength (stepInstr input instruction snapshot).overlay ≤ encodedStoreLength snapshot.overlay + 2 * (Instr.staticWidth instruction + instruction.logCost (decode input snapshot) + 1)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.encodedStoreLength_step_le_internal (program : Program) (input : List Bool) (snapshot : Snapshot) :
encodedStoreLength (step program input snapshot).overlay ≤ encodedStoreLength snapshot.overlay + 2 * (programStaticWidth program + stepLogCost program (decode input snapshot) + 1)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.encodedStoreLength_run_le_internal (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) :
encodedStoreLength (run program input fuel snapshot).overlay ≤ encodedStoreLength snapshot.overlay + 2 * (unitTimeUpto program fuel (decode input snapshot) * (programStaticWidth program + 1) + logTimeUpto program fuel (decode input snapshot))
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_length_run_le_internal (program : Program) (input : List Bool) (fuel : ℕ) :
List.length (run program input fuel (initial input)).overlay ≤ 1 + unitTimeUpto program fuel (initCfg input)
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_encodedStoreLength_run_le_internal (program : Program) (input : List Bool) (fuel : ℕ) :
encodedStoreLength (run program input fuel (initial input)).overlay ≤ 2 * bitlen (input.length + 1) + 2 + 2 * (unitTimeUpto program fuel (initCfg input) * (programStaticWidth program + 1) + logTimeUpto program fuel (initCfg input))
source
theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_encode_length_internal (input : List Bool) :
(initial input).encode.length = 2 * bitlen (input.length + 1) + 6