OAI/Computability/WLIdentification/StackCommands.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WLIdentification.StackModel.Command line 11

    Source documentation

    Finite structured source code. Tests and registers have fixed finite range; all unbounded data remain in the explicitly named bit stacks.

    inductive Command (K R : Type) where
…
  2. abbrev OAI.WLIdentification.StackModel.Command.Control line 23
  3. instance OAI.WLIdentification.StackModel.Command.controlFintype line 29
  4. def OAI.WLIdentification.StackModel.Command.entry line 32
  5. def OAI.WLIdentification.StackModel.Instruction.map line 41
  6. theorem OAI.WLIdentification.StackModel.Instruction.map_map line 48
  7. theorem OAI.WLIdentification.StackModel.Instruction.map_id line 50
  8. def OAI.WLIdentification.StackModel.Command.code line 56
  9. def OAI.WLIdentification.StackModel.Command.program line 69
  10. inductive OAI.WLIdentification.StackModel.Command.Exec line 77

    Source documentation

    Execution costs count actual finite-control stack instructions.

    inductive Exec [DecidableEq K] : Command K R → R → (K → Word) → R → (K → Word) → ℕ → Prop
  | skip (s S) : Exec .skip s S s S 1
  | push (k f s S) : Exec (.push k f) s S s (Function.update S k (S k ++ [f s])) 1
  | pop (k f s S) : Exec (.pop k f) s S (f s (S k).getLast?) (Function.update S k (S k).dropLast) 1
  | modify (f s S) : Exec (.modify f) s S (f s) S 1
  | seq {c d s S t T u U a b} : Exec c s S t T a → Exec d t T u U b →
      Exec (.seq c d) s S u U (b + a)
  | branch_true {test c d s S t T n} : test s = true → Exec c s S t T n →
      Exec (.branch test c d) s S t T (n + 1)
  | branch_false {test c d s S t T n} : test s = false → Exec d s S t T n →
      Exec (.branch test c d) s S t T (n + 1)
  | while_false (test c s S) : test s = false → Exec (.while test c) s S s S 1
…

    Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.Word

  11. def OAI.WLIdentification.StackModel.Command.Embeds line 95

    Source documentation

    A compositional (not oracle) embedding of all source control locations.

    def Embeds (P : Program K Λ R) (c : Command K R) (e : Control c → Λ) (next : Λ) : Prop :=
…

    Mentions: OAI.WLIdentification.StackModel.Program, OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.StackModel.Command.Control

  12. theorem OAI.WLIdentification.StackModel.Command.embeds_seq_left line 99
  13. theorem OAI.WLIdentification.StackModel.Command.embeds_seq_right line 110
  14. theorem OAI.WLIdentification.StackModel.Command.embeds_branch_left line 121
  15. theorem OAI.WLIdentification.StackModel.Command.embeds_branch_right line 132
  16. theorem OAI.WLIdentification.StackModel.Command.embeds_while_body line 143
  17. theorem OAI.WLIdentification.StackModel.Command.Exec.execution line 154

    Source documentation

    This induction supplies every control-flow transition, even nested loops.

    theorem Exec.execution {c : Command K R} {s S t T n} (h : Exec c s S t T n)
    (P : Program K Λ R) (e : Control c → Λ) (next : Λ) (he : Embeds P c e next) :
    (StackModel.step P)^[n] ⟨.inr (e c.entry), s, S⟩ = ⟨.inr next, t, T⟩ := by
…

    Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.StackModel.Command.Exec, OAI.WLIdentification.StackModel.Program, OAI.WLIdentification.StackModel.Command.Control, OAI.WLIdentification.StackModel.Command.Embeds, OAI.WLIdentification.StackModel.step

  18. theorem OAI.WLIdentification.StackModel.Command.program_embeds line 197
  19. theorem OAI.WLIdentification.StackModel.Command.Exec.run line 203