package native

import (
	"errors"
	"math/big"

	"github.com/tutus-one/tutus-chain/pkg/core/dao"
	"github.com/tutus-one/tutus-chain/pkg/core/storage"
	"github.com/tutus-one/tutus-chain/pkg/util"
)

// ARCH-003: Formal Verification Invariants
// This file documents critical system invariants that must hold at all times.
// These invariants serve multiple purposes:
// 1. Runtime verification during testing and canary deployments
// 2. Documentation for formal verification tools (TLA+, Coq, etc.)
// 3. Post-deployment monitoring and alerting

// InvariantCategory categorizes invariants by domain.
type InvariantCategory uint8

const (
	InvariantCategoryToken InvariantCategory = iota
	InvariantCategoryIdentity
	InvariantCategoryGovernance
	InvariantCategoryEconomic
	InvariantCategorySecurity
	InvariantCategoryCrossContract
)

// InvariantSeverity indicates the impact of violation.
type InvariantSeverity uint8

const (
	// InvariantSeverityCritical means system halt required
	InvariantSeverityCritical InvariantSeverity = iota
	// InvariantSeverityHigh means immediate investigation required
	InvariantSeverityHigh
	// InvariantSeverityMedium means potential issue to investigate
	InvariantSeverityMedium
	// InvariantSeverityLow means informational anomaly
	InvariantSeverityLow
)

// Invariant represents a system invariant that must hold.
type Invariant struct {
	ID          string
	Name        string
	Description string
	Category    InvariantCategory
	Severity    InvariantSeverity
	// FormalSpec is TLA+/Coq-style formal specification
	FormalSpec string
}

// InvariantViolation records a violation of a system invariant.
type InvariantViolation struct {
	InvariantID  string
	BlockHeight  uint32
	Details      string
	ActualValue  string
	ExpectedSpec string
}

// Invariant violations are critical errors.
var (
	ErrInvariantViolation       = errors.New("invariant violation detected")
	ErrTokenSupplyMismatch      = errors.New("token supply invariant violated")
	ErrVitaUniqueness           = errors.New("vita uniqueness invariant violated")
	ErrRightsConsistency        = errors.New("rights consistency invariant violated")
	ErrBalanceNonNegative       = errors.New("balance non-negativity invariant violated")
	ErrCrossContractConsistency = errors.New("cross-contract consistency invariant violated")
)

// CriticalInvariants defines all system invariants that must always hold.
var CriticalInvariants = []Invariant{
	// ============================================
	// TOKEN INVARIANTS
	// ============================================
	{
		ID:          "TOK-001",
		Name:        "VTS Total Supply Conservation",
		Description: "Sum of all VTS balances must equal total supply minus burned amount",
		Category:    InvariantCategoryToken,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT VTSSupplyConservation ==
				\A state \in ValidStates:
					Sum({state.vts.balance[addr] : addr \in DOMAIN state.vts.balance})
					= state.vts.totalSupply - state.vts.burnedAmount
		`,
	},
	{
		ID:          "TOK-002",
		Name:        "Non-Negative Balances",
		Description: "No token balance can ever be negative",
		Category:    InvariantCategoryToken,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT NonNegativeBalances ==
				\A state \in ValidStates:
				\A addr \in DOMAIN state.vts.balance:
					state.vts.balance[addr] >= 0
		`,
	},
	{
		ID:          "TOK-003",
		Name:        "Lub Total Supply Conservation",
		Description: "Lub supply follows predictable generation schedule",
		Category:    InvariantCategoryToken,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT LubSupplyConservation ==
				\A state \in ValidStates:
					state.lub.totalSupply <= MaxLubSupply
					/\ Sum({state.lub.balance[addr] : addr \in DOMAIN state.lub.balance})
					   = state.lub.totalSupply
		`,
	},

	// ============================================
	// IDENTITY INVARIANTS
	// ============================================
	{
		ID:          "IDN-001",
		Name:        "Vita Uniqueness Per Person",
		Description: "Each natural person can hold at most one Vita token globally",
		Category:    InvariantCategoryIdentity,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT VitaUniqueness ==
				\A state \in ValidStates:
				\A p1, p2 \in state.vita.tokens:
					p1.biometricHash = p2.biometricHash => p1.tokenID = p2.tokenID
		`,
	},
	{
		ID:          "IDN-002",
		Name:        "Vita Non-Transferability",
		Description: "Vita tokens cannot be transferred except through death/recovery",
		Category:    InvariantCategoryIdentity,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT VitaNonTransferable ==
				\A state, state' \in ValidStates:
				\A vita \in state.vita.tokens:
					state'.vita.tokens[vita.tokenID].owner # vita.owner
					=> state'.vita.tokens[vita.tokenID].status \in {Suspended, Revoked}
					   \/ vita.owner.status = Deceased
		`,
	},
	{
		ID:          "IDN-003",
		Name:        "Vita Count Equals Active Citizens",
		Description: "Active Vita count must match registered citizen count",
		Category:    InvariantCategoryIdentity,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT VitaCountConsistency ==
				\A state \in ValidStates:
					Cardinality({v \in state.vita.tokens : v.status = Active})
					= state.vita.activeCount
		`,
	},

	// ============================================
	// GOVERNANCE INVARIANTS
	// ============================================
	{
		ID:          "GOV-001",
		Name:        "One Person One Vote",
		Description: "Each Vita holder can cast at most one vote per proposal",
		Category:    InvariantCategoryGovernance,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT OnePersonOneVote ==
				\A state \in ValidStates:
				\A p \in state.eligere.proposals:
				\A v \in state.vita.tokens:
					Cardinality({vote \in p.votes : vote.vitaID = v.tokenID}) <= 1
		`,
	},
	{
		ID:          "GOV-002",
		Name:        "Voting Age Enforcement",
		Description: "Only Vita holders >= voting age can vote",
		Category:    InvariantCategoryGovernance,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT VotingAgeEnforced ==
				\A state \in ValidStates:
				\A vote \in AllVotes(state):
					AgeOf(vote.vitaID, state.currentBlock) >= state.config.votingAge
		`,
	},
	{
		ID:          "GOV-003",
		Name:        "Committee Authority Separation",
		Description: "Domain committees have authority only within their domain",
		Category:    InvariantCategoryGovernance,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT CommitteeAuthoritySeparation ==
				\A state \in ValidStates:
				\A action \in state.actions:
					action.requiredDomain = DomainHealth
					=> action.authorizer \in state.committees.health
		`,
	},

	// ============================================
	// ECONOMIC INVARIANTS
	// ============================================
	{
		ID:          "ECO-001",
		Name:        "Tribute Conservation",
		Description: "Total tribute collected equals sum of redistributions plus treasury",
		Category:    InvariantCategoryEconomic,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT TributeConservation ==
				\A state \in ValidStates:
					state.tribute.totalCollected
					= state.tribute.totalRedistributed + state.treasury.tributeBalance
		`,
	},
	{
		ID:          "ECO-002",
		Name:        "Investment Opportunity Bounds",
		Description: "Investment totals cannot exceed opportunity limits",
		Category:    InvariantCategoryEconomic,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT InvestmentBounds ==
				\A state \in ValidStates:
				\A opp \in state.collocatio.opportunities:
					Sum({inv.amount : inv \in opp.investments}) <= opp.maxAmount
		`,
	},

	// ============================================
	// SECURITY INVARIANTS
	// ============================================
	{
		ID:          "SEC-001",
		Name:        "Rights Restriction Requires Due Process",
		Description: "Rights can only be restricted with valid judicial order",
		Category:    InvariantCategorySecurity,
		Severity:    InvariantSeverityCritical,
		FormalSpec: `
			INVARIANT RightsRestrictionDueProcess ==
				\A state \in ValidStates:
				\A restriction \in state.lex.restrictions:
					restriction.caseID # ""
					/\ restriction.authorizedBy \in state.roles.judges
					/\ restriction.expiresAt > state.currentBlock
		`,
	},
	{
		ID:          "SEC-002",
		Name:        "Role Expiry Enforcement",
		Description: "Expired roles grant no permissions",
		Category:    InvariantCategorySecurity,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT ExpiredRolesInactive ==
				\A state \in ValidStates:
				\A role \in state.roleRegistry.assignments:
					role.expiresAt <= state.currentBlock
					=> ~HasPermission(role.holder, role.roleID, state)
		`,
	},
	{
		ID:          "SEC-003",
		Name:        "Circuit Breaker Effectiveness",
		Description: "Open circuit breakers block all protected operations",
		Category:    InvariantCategorySecurity,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT CircuitBreakerEffective ==
				\A state \in ValidStates:
				\A breaker \in state.circuitBreakers:
					breaker.state = Open
					=> ~\E op \in state.operations:
						op.protected = breaker.name /\ op.status = Completed
		`,
	},

	// ============================================
	// CROSS-CONTRACT INVARIANTS
	// ============================================
	{
		ID:          "XCT-001",
		Name:        "Annos-Vita Consistency",
		Description: "Every Annos lifespan record has corresponding Vita token",
		Category:    InvariantCategoryCrossContract,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT AnnosVitaConsistency ==
				\A state \in ValidStates:
				\A record \in state.annos.lifespans:
					\E vita \in state.vita.tokens:
						vita.tokenID = record.vitaID
		`,
	},
	{
		ID:          "XCT-002",
		Name:        "Scire-Vita Consistency",
		Description: "Education accounts require valid Vita holders",
		Category:    InvariantCategoryCrossContract,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT ScireVitaConsistency ==
				\A state \in ValidStates:
				\A account \in state.scire.accounts:
					\E vita \in state.vita.tokens:
						vita.tokenID = account.vitaID /\ vita.status = Active
		`,
	},
	{
		ID:          "XCT-003",
		Name:        "Salus-Vita Consistency",
		Description: "Healthcare accounts require valid Vita holders",
		Category:    InvariantCategoryCrossContract,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT SalusVitaConsistency ==
				\A state \in ValidStates:
				\A account \in state.salus.accounts:
					\E vita \in state.vita.tokens:
						vita.tokenID = account.vitaID
		`,
	},
	{
		ID:          "XCT-004",
		Name:        "Federation Debt Balance",
		Description: "Inter-chain debts sum to zero globally",
		Category:    InvariantCategoryCrossContract,
		Severity:    InvariantSeverityHigh,
		FormalSpec: `
			INVARIANT FederationDebtBalance ==
				\A globalState \in ValidGlobalStates:
					Sum({chain.federation.debt[other] :
						chain \in globalState.chains,
						other \in globalState.chains})
					= 0
		`,
	},
}

// InvariantChecker provides runtime invariant verification.
type InvariantChecker struct {
	contractID int32
	violations []InvariantViolation
}

// NewInvariantChecker creates a new invariant checker.
func NewInvariantChecker(contractID int32) *InvariantChecker {
	return &InvariantChecker{
		contractID: contractID,
		violations: make([]InvariantViolation, 0),
	}
}

// CheckVTSSupplyInvariant verifies VTS supply conservation (TOK-001).
func (ic *InvariantChecker) CheckVTSSupplyInvariant(d *dao.Simple, vtsContractID int32) error {
	// Get total supply
	supplyKey := []byte{0x11} // VTS total supply prefix
	supplyData := d.GetStorageItem(vtsContractID, supplyKey)
	if supplyData == nil {
		return nil // Not initialized
	}
	totalSupply := new(big.Int).SetBytes(supplyData)

	// Sum all balances
	balanceSum := big.NewInt(0)
	balancePrefix := []byte{0x14} // VTS balance prefix

	d.Seek(vtsContractID, storage.SeekRange{Prefix: balancePrefix}, func(k, v []byte) bool {
		balance := new(big.Int).SetBytes(v)
		balanceSum.Add(balanceSum, balance)
		return true
	})

	if totalSupply.Cmp(balanceSum) != 0 {
		ic.recordViolation("TOK-001", 0, "Supply mismatch",
			balanceSum.String(), totalSupply.String())
		return ErrTokenSupplyMismatch
	}

	return nil
}

// CheckVitaUniquenessInvariant verifies Vita uniqueness (IDN-001).
func (ic *InvariantChecker) CheckVitaUniquenessInvariant(d *dao.Simple, vitaContractID int32) error {
	biometricHashes := make(map[util.Uint256]uint64)
	tokenPrefix := []byte{0x01} // Vita token prefix

	var violation bool
	d.Seek(vitaContractID, storage.SeekRange{Prefix: tokenPrefix}, func(k, v []byte) bool {
		if len(v) < 32 {
			return true
		}
		// Extract biometric hash from token data
		var bioHash util.Uint256
		copy(bioHash[:], v[:32])

		if existingID, exists := biometricHashes[bioHash]; exists {
			ic.recordViolation("IDN-001", 0, "Duplicate biometric hash",
				"Multiple tokens", "Single token per biometric")
			_ = existingID // Reference to suppress unused warning
			violation = true
			return false
		}

		// Extract token ID from key
		if len(k) >= 8 {
			tokenID := uint64(k[0])<<56 | uint64(k[1])<<48 | uint64(k[2])<<40 |
				uint64(k[3])<<32 | uint64(k[4])<<24 | uint64(k[5])<<16 |
				uint64(k[6])<<8 | uint64(k[7])
			biometricHashes[bioHash] = tokenID
		}
		return true
	})

	if violation {
		return ErrVitaUniqueness
	}
	return nil
}

// CheckNonNegativeBalances verifies no negative balances exist (TOK-002).
func (ic *InvariantChecker) CheckNonNegativeBalances(d *dao.Simple, contractID int32, balancePrefix byte) error {
	prefix := []byte{balancePrefix}

	var violation bool
	d.Seek(contractID, storage.SeekRange{Prefix: prefix}, func(k, v []byte) bool {
		balance := new(big.Int).SetBytes(v)
		if balance.Sign() < 0 {
			ic.recordViolation("TOK-002", 0, "Negative balance detected",
				balance.String(), ">= 0")
			violation = true
			return false
		}
		return true
	})

	if violation {
		return ErrBalanceNonNegative
	}
	return nil
}

// CheckRightsConsistency verifies rights restrictions have valid due process (SEC-001).
func (ic *InvariantChecker) CheckRightsConsistency(d *dao.Simple, lexContractID int32, currentBlock uint32) error {
	restrictionPrefix := []byte{0x20} // Lex restriction prefix

	var violation bool
	d.Seek(lexContractID, storage.SeekRange{Prefix: restrictionPrefix}, func(k, v []byte) bool {
		if len(v) < 40 {
			return true
		}

		// Check if restriction has case ID (non-empty)
		caseIDLen := v[0]
		if caseIDLen == 0 {
			ic.recordViolation("SEC-001", currentBlock,
				"Rights restriction without case ID", "empty", "non-empty case ID")
			violation = true
			return false
		}

		return true
	})

	if violation {
		return ErrRightsConsistency
	}
	return nil
}

// recordViolation records an invariant violation.
func (ic *InvariantChecker) recordViolation(invariantID string, blockHeight uint32, details, actual, expected string) {
	ic.violations = append(ic.violations, InvariantViolation{
		InvariantID:  invariantID,
		BlockHeight:  blockHeight,
		Details:      details,
		ActualValue:  actual,
		ExpectedSpec: expected,
	})
}

// GetViolations returns all recorded violations.
func (ic *InvariantChecker) GetViolations() []InvariantViolation {
	return ic.violations
}

// ClearViolations clears recorded violations.
func (ic *InvariantChecker) ClearViolations() {
	ic.violations = make([]InvariantViolation, 0)
}

// RunAllCriticalChecks runs all critical invariant checks.
func (ic *InvariantChecker) RunAllCriticalChecks(d *dao.Simple, contracts ContractIDs, currentBlock uint32) []InvariantViolation {
	ic.ClearViolations()

	// Run critical checks
	_ = ic.CheckVTSSupplyInvariant(d, contracts.VTS)
	_ = ic.CheckVitaUniquenessInvariant(d, contracts.Vita)
	_ = ic.CheckNonNegativeBalances(d, contracts.VTS, 0x14)
	_ = ic.CheckNonNegativeBalances(d, contracts.Tutus, 0x14)
	_ = ic.CheckNonNegativeBalances(d, contracts.Lub, 0x14)
	_ = ic.CheckRightsConsistency(d, contracts.Lex, currentBlock)

	return ic.GetViolations()
}

// ContractIDs holds contract identifiers for invariant checking.
type ContractIDs struct {
	VTS    int32
	Vita   int32
	Tutus  int32
	Lub    int32
	Lex    int32
	Annos  int32
	Scire  int32
	Salus  int32
}