package engines

import (
	"fmt"
	"sort"
	"strings"
)

// fail records a violation of invariant inv, once per invariant id: the
// first message is the one the sweep reports and the later ones are the same
// fault again. The stored text begins "<inv>: ", which invariantOf reads back.
func (w *world) fail(inv, format string, args ...any) {
	for _, v := range w.violations {
		if invariantOf(v) == inv {
			return
		}
	}
	w.violations = append(w.violations, inv+": "+fmt.Sprintf(format, args...))
}

// invariantOf is the invariant id a violation string was recorded under.
func invariantOf(violation string) string {
	if i := strings.Index(violation, ": "); i >= 0 {
		return violation[:i]
	}
	return violation
}

// The invariants of Task 2 (spec §5.1, §6.3):
//
//   - INV-P (event, recorded in deliver): a public request is never delivered
//     to a process whose build declares doc_engine.
//   - INV-I1: no process of a declaring build runs unless its group is fenced
//     as internal. Checked when each process starts, on every launch path
//     (systemd and socket starts included), and again at every step boundary
//     for every running process, since a later change can unfence a group
//     under a process already running. It is two conditions:
//     1. the fence itself, as the spec states I1: the edge's fenced counter
//     has reached the registry change that set the group's mark to 1, and
//     nothing later cleared it (fencedTruth). A group open, NULL but never
//     loaded (a new row), unloaded or written but not yet fenced fails here.
//     2. the fact the fence stands for: no row of the group is served 0 by
//     the edge's map. This catches a counter advanced without a swap, which
//     condition 1 cannot see because it reads that counter.

// i1Broken reports why process p breaks I1, or "" when it does not.
func (w *world) i1Broken(b *box, p *proc) string {
	if !w.builds[p.Ver].Declares {
		return ""
	}
	if !w.fencedTruth(b, p.Group) {
		at := "never"
		if w.recorded(b, p.Group) {
			at = fmt.Sprint(b.SetAt[p.Group])
		}
		return fmt.Sprintf("the group is not fenced (registry %v, fenced %d, set at %s)", w.groupMark(b, p.Group), b.Fenced, at)
	}
	hosts := make([]string, 0, len(b.EdgeRows))
	for h := range b.EdgeRows {
		hosts = append(hosts, h)
	}
	sort.Strings(hosts)
	for _, h := range hosts {
		if edgeGroup(b, h) == p.Group && b.Serving[h] == markPublic {
			return fmt.Sprintf("the edge serves %s public", h)
		}
	}
	return ""
}

// checkStart is I1 at the moment process p starts.
func (w *world) checkStart(b *box, p *proc) {
	if why := w.i1Broken(b, p); why != "" {
		w.failProc(b, p, "INV-I1", true, "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
	}
}

// check runs the state invariants over every running process. doStep calls
// it after every action; a witness calls it at each of its step boundaries.
// Task 5 adds INV-ARM (checkArm); its event invariants INV-ID and INV-G are
// recorded when an engine call reaches a process (checkCall).
func (w *world) check() {
	w.endResidualWindows()
	for _, b := range w.boxes {
		for _, p := range b.Procs {
			if why := w.i1Broken(b, p); why != "" {
				w.failProc(b, p, "INV-I1", true, "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
			}
		}
	}
	w.checkArm()
}

// edgeGroup is group over the edge's loaded rows.
func edgeGroup(b *box, host string) string {
	if r, ok := b.EdgeRows[host]; ok && r.Kind == "instance" && r.Owner != "" {
		return r.Owner
	}
	return host
}

// INV-AV (liveness, Task 3): at the end of the calm phase, every row of a
// group whose mark is 0 answers a public request. It is what catches the
// rules that only protect availability (static-minted-public,
// owner-nonempty-unique), which no safety invariant can see. Checked in
// final() only, after every edge has polled with its faults cleared.
//
// The truth, not the model's resolution, decides which rows must answer:
//   - a static or service row is 0 by construction (spec §5.1, "The column"),
//     minted or not;
//   - an instance row answers when its group's mark is 0: the registry mark
//     of its own row, or for a minted row, of the row it was minted from
//     (Source);
//   - alias rows are skipped: they answer as their target does.
//
// Not counted, as the spec's fail-closed choices or another rule's stated
// refusal: a minted row whose owner the correct fallback cannot find
// uniquely (refused and logged until the reconciler records its owner), and
// any row an avExemption names.
func (w *world) checkAV() {
	for _, b := range w.boxes {
		hosts := make([]string, 0, len(b.Rows))
		for h := range b.Rows {
			hosts = append(hosts, h)
		}
		sort.Strings(hosts)
		for _, h := range hosts {
			r := b.Rows[h]
			switch r.Kind {
			case "alias":
				continue
			case "instance":
				owner := h
				if r.Platform {
					if _, ok := b.resolveOwnerWith(r, true); !ok {
						w.logf("box%d: final: minted row %s has no unique owner; refused by design, not counted", b.ID, h)
						continue
					}
					owner = r.Source
				}
				if b.Mark[owner] != markPublic {
					continue
				}
			}
			if why := w.avExempt(b, h); why != "" {
				w.logf("box%d: final: %s exempt from INV-AV: %s", b.ID, h, why)
				continue
			}
			req, outcome := w.admit(b, h, "/")
			switch outcome {
			case admitted:
				w.deliver(req)
			case answered:
			default:
				w.fail("INV-AV", "box%d: row %s (%s) of a public group is %s a public request at the end of the calm phase (registry %v, edge %v)", b.ID, h, r.Kind, outcome, b.Mark[h], b.Serving[h])
			}
		}
	}
}

// avExemptions are later tasks' stated refusals of a public row (each
// returns why, or ""), which INV-AV must not count.
var avExemptions []func(w *world, b *box, host string) string

func (w *world) avExempt(b *box, host string) string {
	for _, f := range avExemptions {
		if why := f(w, b, host); why != "" {
			return why
		}
	}
	return ""
}

// ---------- Task 5: INV-ID, INV-G, INV-ARM (calls_test.go) ----------

// checkCall is INV-ID and INV-G for an engine call that reached process q on
// home, sent by process p (nil: a public client) on box from through the
// engine socket or door key of instance via.
//
//   - INV-ID: the caller the engine box records is the app whose code made
//     the call. The flat-era residual covers only a call whose recorded
//     caller is the compromised instance itself (compromisedItself).
//   - INV-G: the call reaches the engine's exact route, and grantBreach finds
//     no breach of the grant's freshness.
func (w *world) checkCall(home, from *box, mark caller, via, real string, p, q *proc) {
	if mark.app() != real {
		msg := fmt.Sprintf("box%d: the engine box records caller %s for a call made by %q (process %v)", home.ID, mark.app(), real, procID(p))
		if w.flatEraTamper && w.compromisedItself(from, mark, via, p) {
			w.residual("flatEraTamper", "%s: code planted before the box was armed", msg)
		} else {
			w.fail("INV-ID", "%s", msg)
		}
	}
	exact, _ := w.exactRoute(home, engineHosts[mark.Engine])
	if want := truthGroup(home, exact.Host); q.Group != want {
		w.fail("INV-G", "box%d: an engine call for %s reached process %d of %s, not the engine's exact route %s", home.ID, mark.key(), q.ID, q.Group, want)
	}
	if why := w.grantBreach(home, from, mark.key()); why != "" {
		w.fail("INV-G", "box%d: an engine call for %s reached process %d of %s; %s", home.ID, mark.key(), q.ID, q.Group, why)
	}
}

// compromisedItself: the flat-era residual's own case, from facts no rule
// changes. Process p is the instance via's own process, in via's own slice,
// running the code planted in via's directory, and the caller recorded is
// via's own app. Planted code that borrows another instance's socket or
// forges a hop caller is a violation like any other.
func (w *world) compromisedItself(from *box, mark caller, via string, p *proc) bool {
	if p == nil || p.Code == "" || p.Unisolated || via == "" {
		return false
	}
	r := from.Rows[via]
	return r != nil && p.Group == via && p.Slice == "inst:"+via && from.Tampered[via] == p.Code && mark.app() == r.App
}

// grantBreach is INV-G's grant clauses for key on a call admitted by the
// tables of from and home, each from facts no rule changes (spec §5.3, §6.4,
// ruling R5). It returns the first breach, or "".
//
//  1. Expiry: a key the newest record grants is granted by no table once that
//     record has expired (every older record expired first), at once.
//  2. Revoke age: a key the newest record does not grant is granted by no
//     table more than ten minutes plus one poll after the revoke, whatever
//     was replayed (every record that grants it was signed before the
//     revoke, and is stale ten minutes after its signing). A key no record
//     ever granted is never granted.
//  3. The admitting tables: neither box admits on a table that was never
//     read, holds an expired record, has had no good read for ten minutes, or
//     holds a record signed ten minutes ago or more, whatever the key's
//     revoke (from always checks its table; home is the engine box, whose
//     table must be empty too).
//  4. A revoke a box has read stays in force there (§6.4: the floor refuses
//     every older record).
func (w *world) grantBreach(home, from *box, key string) string {
	c := &w.console
	now := w.now()
	newest := c.Records[c.Rev]
	if newest.Grants[key] && now >= newest.Expires {
		return fmt.Sprintf("the newest record (revision %d), which grants it, expired at %d, now %d", newest.Rev, newest.Expires, now)
	}
	if !newest.Grants[key] {
		since, ok := c.RevokedAt[key]
		if !ok {
			return fmt.Sprintf("no record has granted it (newest revision %d)", newest.Rev)
		}
		if now-since > staleTicks+pollTicks {
			return fmt.Sprintf("the newest record (revision %d) has not granted it since tick %d, now %d", newest.Rev, since, now)
		}
	}
	boxes := []*box{from}
	if home != from {
		boxes = append(boxes, home)
	}
	for _, b := range boxes {
		if why := w.tableStale(b); why != "" {
			return fmt.Sprintf("box%d admitted it on a table that %s", b.ID, why)
		}
	}
	if rr, ok := c.RevokedRev[key]; ok && !newest.Grants[key] {
		for _, b := range boxes {
			if b.ReadRev >= rr {
				return fmt.Sprintf("box%d had read revision %d, which revoked it (read %d)", b.ID, rr, b.ReadRev)
			}
		}
	}
	return ""
}

// tableStale says why b's table must be empty, or "".
func (w *world) tableStale(b *box) string {
	m, now := b.Mirror, w.now()
	switch {
	case m.Rec == nil:
		return "was never read"
	case now >= m.Rec.Expires:
		return fmt.Sprintf("holds revision %d, expired at %d, now %d", m.Rec.Rev, m.Rec.Expires, now)
	case now-m.ReadAt >= staleTicks:
		return fmt.Sprintf("has had no good read for %d ticks", now-m.ReadAt)
	case now-m.Rec.SignedAt >= staleTicks:
		return fmt.Sprintf("holds revision %d, signed at %d, %d ticks ago", m.Rec.Rev, m.Rec.SignedAt, now-m.Rec.SignedAt)
	}
	return ""
}

func procID(p *proc) any {
	if p == nil {
		return "none"
	}
	return p.ID
}

// INV-ARM (state): no unisolated tenant process exists on a box while an
// engine socket is open there. check() runs it.
func (w *world) checkArm() {
	for _, b := range w.boxes {
		if !b.Sockets {
			continue
		}
		for _, p := range b.Procs {
			if p.Unisolated {
				w.fail("INV-ARM", "box%d: engine sockets are open (armed %v) while process %d runs unisolated in %s", b.ID, b.Armed, p.ID, p.Slice)
			}
		}
	}
}

// residual records the stated residual name once: "residual:<name>: ...".
func (w *world) residual(name, format string, args ...any) {
	for _, r := range w.residuals {
		if strings.HasPrefix(r, "residual:"+name+":") {
			return
		}
	}
	w.residuals = append(w.residuals, "residual:"+name+": "+fmt.Sprintf(format, args...))
	w.logf("residual:%s recorded", name)
}

// failProc is fail for a breach process p on b causes. It records the stated
// residual p belongs to instead only when the breach is the residual's own:
// viaClassification says the breach came by a path the upgrade's 0 opened
// (I1 itself, the edge serving the group, a ports listener rendered for a
// public group), and the residual's window still holds (residualHolds). Any
// other breach of a tagged process is a violation.
func (w *world) failProc(b *box, p *proc, inv string, viaClassification bool, format string, args ...any) {
	if viaClassification && w.residualHolds(b, p) {
		w.residual(p.Residual, inv+": "+format, args...)
		return
	}
	w.fail(inv, format, args...)
}

// residualHolds: p is tagged with the unwritten-manifest residual and its
// group is still open, as the upgrade classified it. The window ends for good
// the first time the group is closed again (a grant, a gate's 1): the tag is
// cleared, so a later 0 (another rule's failure) is never misfiled as the
// upgrade's.
func (w *world) residualHolds(b *box, p *proc) bool {
	if p == nil || p.Residual == "" {
		return false
	}
	if w.closed(b, p.Group) {
		w.logf("box%d: %s is closed again: process %d's residual window (%s) ends", b.ID, p.Group, p.ID, p.Residual)
		p.Residual = ""
		return false
	}
	return true
}

// endResidualWindows runs residualHolds on every tagged process, so a window
// ends when its group closes even if nothing breaches meanwhile.
func (w *world) endResidualWindows() {
	for _, b := range w.boxes {
		for _, p := range b.Procs {
			if p.Residual != "" {
				w.residualHolds(b, p)
			}
		}
	}
}