feat: complexity theory

[SamuelSchlesinger]

This PR defines complexity classes like P, PSPACE, NP, on top of Turing machines. It also cleans up the Turing machine module a bit.

[SamuelSchlesinger]

I have quite a bit more on my personal fork, I've even got so far as defining cryptographic security notions via games played against computationally bounded adversaries. I'm planning to upstream pieces of it slowly as I tidy them up and finalize the abstraction layers, let me know if this is already too large of a PR.

[chenson2018]

cc @Timeroot and @BoltonBailey who might be interested in reviewing

[SamuelSchlesinger]

I'll take a look at the commit convention and CI stuff.

[SamuelSchlesinger]

I am trying to prove Cook-Levin as a pressure test of these definitions.

[SamuelSchlesinger]

Cook-Levin is incredibly painful in this simple formalization, seems like we'd want something more expressive like #384. This is, however, simple enough for me to define cryptographic security notions, so I might still use it for that.

[SamuelSchlesinger]

Cleaned things up quite a bit. Slowly learning how to write not horrible Lean! The namespace thing was tripping me up.

[Timeroot]

• I feel like "OutputsInSpace" should be defined together with "OutputsInTime". Probably also just "Outputs", with we existential, and a parent "OutputsInSpaceTime" that all specialize from.
• So, PolyTimeComputable is not a Prop: it carries the constructed Turing machine around with it (as well as the time bound function). I assume this is deliberate. In that case, PolyTimeReduces should probably follow that convention too -- or they should *all" be Prop. Separately, I would call the predicate PolyTimeReducible to match.
• The definition of Verifies currently has a TODO suggesting it might not be the best definition. I'm inclined to agree. I think that it's probably not great to accept this definition when we're already aware it has a big deficiency. (There are some easy fixes though.)

I'll probably write more thoughts later...

Thank you for the PR! 😁

[Timeroot]

Could you point to the places you use these definitions in your personal fork? Seeing how they get used in more complex goals would do a lot to motivate them!

[SamuelSchlesinger]

I feel like "OutputsInSpace" should be defined together with "OutputsInTime". Probably also just "Outputs", with we existential, and a parent "OutputsInSpaceTime" that all specialize from.

This sounds sane, I'll take a crack at it and see what it looks like.

So, PolyTimeComputable is not a Prop: it carries the constructed Turing machine around with it (as well as the time bound function). I assume this is deliberate. In that case, PolyTimeReduces should probably follow that convention too -- or they should *all" be Prop. Separately, I would call the predicate PolyTimeReducible to match.

That precedes me unless I am misunderstanding you. I think it should be a prop, probably.

The definition of Verifies currently has a TODO suggesting it might not be the best definition. I'm inclined to agree. I think that it's probably not great to accept this definition when we're already aware it has a big deficiency. (There are some easy fixes though.)

Yeah, I am working in another unreleased repository on a much nicer abstraction for Turing machines that include deterministic, (co-)non-deterministic, and probabilistic TMs all in one definition based on some stuff I wrote in Haskell years ago. Using Lean lets me do way cooler things, here's a teaser:

  class Possible (M : Type → Type) extends Monad M where
    possible : M α → α → Prop
    possible_pure : ∀ (a b : α), possible (pure a) b ↔ a = b
    possible_bind : ∀ (ma : M α) (f : α → M β) (b : β),
      possible (ma >>= f) b ↔ ∃ a, possible ma a ∧ possible (f a) b

so I can reason about reachability while still executing using the Monad instance, and

  structure MultiTapeTM (Symbol : Type) (M : Type → Type) [Possible M] where
    nWork : ℕ                    -- number of work tapes
    State : Type
    q₀ : State
    tr : State
       → Option Symbol                        -- read from input tape head
       → (Fin nWork → Option Symbol)          -- read from work tape heads
       → M ( TapeAction Symbol               -- action on input tape (could restrict to move-only)
           × (Fin nWork → TapeAction Symbol)  -- actions on work tapes
           × TapeAction Symbol               -- action on output tape
           × Option State )                   -- next state (none = halt)

Could you point to the places you use these definitions in your personal fork? Seeing how they get used in more complex goals would do a lot to motivate them!

Sure, the main context is to qualify adversaries, so I am actually really flexible on the underlying representation. As long as I can build a function from Adv -> Prop with it, I am good to go. I am definitely open to bikeshedding these definitions for some time before upstreaming. Here is the security game definition: https://github.com/SamuelSchlesinger/cslib/blob/main/Cslib/Cryptography/Foundations/SecurityGame.lean. Here is a use site: https://github.com/SamuelSchlesinger/cslib/blob/d502e001f49a0017db235da6e51e2b7d68630fd2/Cslib/Cryptography/Reductions/FiatShamirROM.lean#L3017. Reading this all in more detail made me realize that this use site actually uses unconditional security against any adversary instead of just admissible adversaries from some subset, which is a good catch, so I appreciate the discussion.

Edit: thankfully, this was easy to fix.