# SPDX-License-Identifier: MIT

# pqc — what to move off quantum-vulnerable cryptography first, and why.
#
# This module supplies the REASONING. You supply the facts: where your systems
# use cryptography (`pqc.Use`), how each algorithm stands against a quantum
# computer (`pqc.Algorithm`), how long each kind of data must stay protected
# (`pqc.Data`), how long each system takes to migrate (`pqc.System`), the year
# you plan against (`pqc.Horizon`), and the deadlines you are held to
# (`pqc.Deadline`). Import this module and the standing rules and the queries
# below apply to whatever you have loaded.
#
#     import pqc
#
# The reasoning is Mosca's inequality. A use of a quantum-vulnerable algorithm
# is a problem when the time what it protects must stay protected, plus the
# time it takes to migrate, reaches past the time a quantum computer can break
# it. Data recorded now can be decrypted then, so the deadline is earlier than
# the horizon by the data's shelf life.
#
# YEARS. Every year here is a calendar year, written as an `int`, and every
# boundary means the first year WITHOUT something:
#
# - `Horizon.year` is the first year you assume a quantum computer able to
#   break the vulnerable algorithms exists.
# - `Use.migrated` is the first year the use no longer relies on its algorithm,
#   planned or done. A use that ends because its system is switched off records
#   the year it is switched off.
# - `Deadline.year` is the first year an algorithm the deadline covers may not
#   be used.
# - Data protected in year t, with a shelf life of x years, still needs
#   protection in year t + x. So the first year a use must no longer rely on a
#   vulnerable algorithm is the horizon less the shelf life, and the last year
#   to start moving it is that less the migration time.
#
# The store keeps no clock. Every conclusion is a year, and a question that
# depends on the present takes the year as its argument, so you get the same
# answer every time you ask about that year.
#
# DISAGREEMENT. Two sources may record different values for one field: a
# scanner and a system's owner on an algorithm, two policies on a shelf life.
# The store keeps both, and so does this module. A use is late, exposed or
# remaining if any value on record makes it so, and it is placed by the
# earliest year it must start. Its deadline is the earliest year of any value
# of any deadline that covers its algorithm: one source's year, never two
# added. `unsettled()` names every use where a value of its own, or of the
# horizon, shelf life or migration time it is reasoned about with, disagrees,
# so you can settle it. A deadline's year is not among them; `why` on the
# use's deadline names the year that placed it, beside every year it was
# chosen from.

class Horizon:
    # The first year you assume a quantum computer able to break the vulnerable
    # algorithms exists. Record one horizon. Two are read as two assumptions
    # held at once, and every use is reasoned about under both.
    year: int

class Algorithm:
    # One algorithm, as the subject your uses name. `quantum` is "vulnerable"
    # for an algorithm a quantum computer breaks: RSA, finite-field and
    # elliptic-curve Diffie-Hellman, ECDSA and EdDSA among them. Any other value
    # is not vulnerable. `strength` is its classical security strength in bits,
    # which is what a deadline is stated against.
    quantum: string
    strength: int

class Data:
    # What a use protects. `shelf_life` is how many years after it is protected
    # it must stay protected. For a key exchange or an encryption that is how
    # long the data must stay secret. For a signature it is how long the
    # signature must be trusted: zero for an authentication checked once, years
    # for a signed document or firmware.
    shelf_life: int

class System:
    # What uses the cryptography. `migration` is how many years moving it off a
    # vulnerable algorithm takes.
    migration: int

class Deadline:
    # A deadline you are held to: from `year` on, a quantum-vulnerable algorithm
    # of at most `strength` bits may not be used. A deadline for every strength
    # names a strength no algorithm exceeds.
    year: int
    strength: int

class Use:
    # One use of an algorithm by a system, protecting one kind of data.
    # `migrated` is the first year it no longer relies on the algorithm, and a
    # use with none has no plan.
    system: string
    algorithm: string
    protects: string
    migrated: int
    # The rules below copy these three onto each vulnerable use. You never
    # write them.
    horizon: int
    shelf_life: int
    migration: int
    # The first year the use must no longer rely on its algorithm, and the last
    # year to start moving it.
    migrate_by: int = horizon - shelf_life
    start_by: int = migrate_by - migration

# ── Standing rules ───────────────────────────────────────────────────────────
#
# A rule holds continuously: its conclusion is in force exactly while its
# condition holds, and withdraws itself when the condition stops holding. You
# never write these; the engine maintains them.

@rule
def vulnerable():
    for u in Use, a in Algorithm:
        if u.algorithm == a and a.quantum == "vulnerable":
            u.vulnerable = True

@rule
def use_horizon():
    for u in Use, h in Horizon:
        if u.vulnerable == True:
            u.horizon = h.year

@rule
def use_shelf_life():
    for u in Use, d in Data:
        if u.vulnerable == True and u.protects == d:
            u.shelf_life = d.shelf_life

@rule
def use_migration():
    for u in Use, s in System:
        if u.vulnerable == True and u.system == s:
            u.migration = s.migration

@rule
def late():
    # The plan has the use still relying on its algorithm in a year whose data
    # will still need protection at the horizon.
    for u in Use:
        if u.migrated > u.migrate_by:
            u.late = True

@rule
def unplanned():
    for u in Use:
        if u.vulnerable == True and absent(u.migrated):
            u.unplanned = True

@rule
def deadline():
    # The first year any deadline you recorded stops the use's algorithm,
    # under any value of that year.
    for u in Use, a in Algorithm, d in Deadline:
        if u.algorithm == a and a.quantum == "vulnerable" and a.strength <= d.strength:
            u.deadline = min(d.year)

@rule
def deadline_name():
    # Which deadline that is. Two falling in the same year give the first in
    # name order.
    for u in Use, a in Algorithm, d in Deadline:
        if u.algorithm == a and a.quantum == "vulnerable" and a.strength <= d.strength:
            u.deadline_name = argmin(d.year)

@rule
def misses():
    for u in Use:
        if u.migrated > u.deadline:
            u.misses = True

# ── Standing constraints ─────────────────────────────────────────────────────
#
# `checkup()` reports each of these that does not hold, naming the uses that
# breach it. Neither refuses a write.

@constraint
def no_late_plan():
    for u in Use:
        if u.late == True:
            violated

@constraint
def no_missed_deadline():
    for u in Use:
        if u.misses == True:
            violated

# ── Queries ──────────────────────────────────────────────────────────────────
#
# Each answers use names.

def priority() -> list<string>:
    # Every vulnerable use with a start year, the earliest first, and uses
    # starting the same year in name order. A use whose start years disagree is
    # placed by the earliest of them.
    first: dict<string, int> = {}
    vs = list_values(Use.start_by)
    for v in vs:
        parts = v.path.split(".")
        s = parts[len(parts) - 2]
        match v.value:
            case int as y:
                if s not in first or y < first[s]:
                    first[s] = y
            case default:
                pass
    keyed = []
    for s in first:
        keyed = keyed + [(first[s], s)]
    out = []
    for k in sorted(keyed):
        out = out + [k[1]]
    return out


def exposed() -> list<string>:
    # Every use whose plan is late, and every vulnerable use with no plan whose
    # migrate-by year is known: what it protects from that year on can be
    # recorded now and read at the horizon.
    seen: dict<string, bool> = {}
    late_uses = subjects(Use.late, True)
    for s in late_uses:
        seen[s] = True
    known: dict<string, bool> = {}
    bys = list_subjects(Use.migrate_by)
    for s in bys:
        known[s] = True
    unplanned_uses = subjects(Use.unplanned, True)
    for s in unplanned_uses:
        if s in known:
            seen[s] = True
    out = []
    for s in seen:
        out = out + [s]
    return sorted(out)


def noncompliant() -> list<string>:
    # Every use whose plan misses its deadline, and every vulnerable use with no
    # plan that a deadline covers.
    seen: dict<string, bool> = {}
    missing = subjects(Use.misses, True)
    for s in missing:
        seen[s] = True
    covered: dict<string, bool> = {}
    ds = list_subjects(Use.deadline)
    for s in ds:
        covered[s] = True
    unplanned_uses = subjects(Use.unplanned, True)
    for s in unplanned_uses:
        if s in covered:
            seen[s] = True
    out = []
    for s in seen:
        out = out + [s]
    return sorted(out)


def remaining(at: int) -> list<string>:
    # Every vulnerable use still relying on its algorithm in year `at`: it has
    # no plan, or a plan has it migrated after `at`.
    last: dict<string, int> = {}
    vs = list_values(Use.migrated)
    for v in vs:
        parts = v.path.split(".")
        s = parts[len(parts) - 2]
        match v.value:
            case int as y:
                if s not in last or y > last[s]:
                    last[s] = y
            case default:
                pass
    out = []
    us = subjects(Use.vulnerable, True)
    for s in us:
        if s not in last or last[s] > at:
            out = out + [s]
    return sorted(out)


def unclassified() -> list<string>:
    # Every use with no algorithm, or naming an algorithm whose standing against
    # a quantum computer is not recorded. The rules conclude nothing about such
    # a use, so an inventory with one in it is not yet a safe inventory.
    classified: dict<string, bool> = {}
    qs = list_values(Algorithm.quantum)
    for q in qs:
        parts = q.path.split(".")
        classified[parts[len(parts) - 2]] = True
    named: dict<string, bool> = {}
    found: dict<string, bool> = {}
    vs = list_values(Use.algorithm)
    for v in vs:
        parts = v.path.split(".")
        s = parts[len(parts) - 2]
        named[s] = True
        if str(v.value) not in classified:
            found[s] = True
    us = list_subjects(Use)
    for s in us:
        if s not in named:
            found[s] = True
    out = []
    for s in found:
        out = out + [s]
    return sorted(out)


def unassessed() -> list<string>:
    # Every vulnerable use with no start year: what it protects, that data's
    # shelf life, its system's migration time or a horizon is not recorded.
    started: dict<string, bool> = {}
    ss = list_subjects(Use.start_by)
    for s in ss:
        started[s] = True
    out = []
    us = subjects(Use.vulnerable, True)
    for s in us:
        if s not in started:
            out = out + [s]
    return sorted(out)


def unsettled() -> list<string>:
    # Every use for which the store holds more than one value of its algorithm,
    # its plan, or the horizon, shelf life or migration time it is reasoned
    # about with. Each value is reasoned about; this is where to settle them.
    found: dict<string, bool> = {}
    for f in ["algorithm", "migrated", "horizon", "shelf_life", "migration"]:
        held: dict<string, string> = {}
        vs = list_values(Use.f)
        for v in vs:
            parts = v.path.split(".")
            s = parts[len(parts) - 2]
            w = str(v.value)
            if s in held and held[s] != w:
                found[s] = True
            held[s] = w
    out = []
    for s in found:
        out = out + [s]
    return sorted(out)