toulmin — движок правил, вычисляющий контракты

Движки правил стояли на одной и той же предпосылке 60 лет. Объект проверки — это «факт (fact)».

Drools помещает Java-объекты как «fact» в working memory. Rego обращается с input как с заведомо истинными данными. JSON Schema считает структуру документа данностью. Все основаны на одном допущении — входные данные являются фактом.

Но в чём вообще смысл существования движка правил? Проверять, соответствуют ли данные правилам. Называть объект, нуждающийся в проверке, «уже истинным» — это противоречие.

Не факт, а утверждение

Объект проверки — не fact, а claim (утверждение). Это заявление, которое может оказаться истинным или ложным. Его обоснованность должна быть определена правилами.

JWT уже следует этому принципу. sub, exp, iss называются не «facts», а «claims». Это утверждения эмитента токена. Только после проверки подписи, срока действия и сверки issuer им можно доверять.

Эта структура была описана ещё в 1958 году.

Модель аргументации Тулмина

Стивен Тулмин в 1958 году разложил структуру аргументации на 6 элементов:

• Claim (утверждение): объект оценки. То, что нужно проверить — истинно или ложно.
• Ground (основание): данные-доказательства, используемые для оценки.
• Warrant (гарантия): правило, определяющее, что основание поддерживает утверждение.
• Backing (подкрепление): обоснование того, почему правило действительно.
• Qualifier (квалификатор): степень уверенности в оценке.
• Rebuttal (опровержение): исключительные условия, при которых утверждение не выполняется.

Формальная логика гласит: «если посылки истинны, то и заключение истинно». Тулмин мыслил иначе. «Утверждение поддерживается основанием и правилом, но при наличии исключений оно опровергается.» Любой аргумент может быть опровергнут.

Движки правил 60 лет стояли на стороне формальной логики. Вход — fact, результат — allow/deny, исключения — отдельный механизм. Тулмин был на другой стороне. Вход — claim, результат — степень (degree), исключения — встроены.

Проблема в том, что книга Тулмина стояла на полке философии. На полке движков правил её не было видно. 60 лет недостающего звена.

Поэтому я создал движок правил

toulmin — это реализация модели аргументации Тулмина в виде движка правил на Go.

Требования эволюционируют

Посмотрим, как if-else и toulmin справляются с одной и той же эволюцией требований.

// Понедельник: "Доступ только для аутентифицированных, блокировка по IP, внутренняя сеть освобождена от блокировки"
g := toulmin.NewGraph("api:access")
auth    := g.Warrant(isAuthenticated, nil, 1.0)
blocked := g.Rebuttal(isIPBlocked, nil, 1.0)
exempt  := g.Defeater(isInternalIP, nil, 1.0)
g.Defeat(blocked, auth)
g.Defeat(exempt, blocked)

// Вторник: "Добавить Rate limiting"
limited := g.Rebuttal(isRateLimited, nil, 1.0)
g.Defeat(limited, auth)

// Среда: "Премиум-пользователи освобождены от Rate limit"
premium := g.Defeater(isPremiumUser, nil, 1.0)
g.Defeat(premium, limited)

// Четверг: "Во время инцидента ограничены даже премиум-пользователи"
incident := g.Rebuttal(isIncidentMode, nil, 1.0)
g.Defeat(incident, premium)

Каждый день 2 строки добавляются, существующий код не меняется. Та же эволюция на if-else:

// Понедельник
if user != nil {
    if blockedIPs[ip] {
        if strings.HasPrefix(ip, "10.") {
            allow = true
        }
    } else {
        allow = true
    }
}

// Четверг — 4 уровня вложенности, структуру невозможно понять
if user != nil {
    if blockedIPs[ip] {
        if strings.HasPrefix(ip, "10.") {
            allow = true
        }
    } else if isRateLimited(ip) {
        if isPremium(user) {
            if !incidentMode {
                allow = true
            }
        }
    } else {
        allow = true
    }
}

toulmin: 2 строки на требование, структура неизменна. if-else: каждый раз перестраивается вся структура.

Правила — это функции Go

func(claim any, ground any, backing any) (bool, any)

• ground = материал для оценки, меняющийся с каждым запросом (пользователь, IP, контекст)
• backing = критерий оценки, фиксируемый при объявлении графа (пороговые значения, имена ролей, настройки)
• Возврат = (результат оценки, доказательство). Доказательство — произвольный тип, зависящий от домена.

func CheckOneFileOneFunc(claim, ground, backing any) (bool, any) {
    g := ground.(*FileGround)
    if len(g.Funcs) > 1 {
        return true, &Evidence{Got: len(g.Funcs), Expected: 1}
    }
    return false, nil
}

Не нужно учить новый язык, как Rego. Достаточно писать функции на Go.

backing — одна функция, разные критерии оценки

backing передаёт критерий оценки правила как значение времени выполнения. Одна и та же функция, зарегистрированная с разным backing, становится отдельным правилом:

g := toulmin.NewGraph("access")
admin  := g.Warrant(isInRole, "admin", 1.0)
editor := g.Warrant(isInRole, "editor", 0.8)

g := toulmin.NewGraph("line-limit")
strict  := g.Warrant(CheckLineCount, &LineLimit{Max: 100}, 0.7)
relaxed := g.Warrant(CheckLineCount, &LineLimit{Max: 200}, 0.5)
g.Defeat(relaxed, strict)

Если backing равен nil, значит правилу не нужен критерий оценки.

Исключения объявляются как граф

С помощью Graph Builder API объявляются отношения между правилами, а движок обрабатывает их автоматически. Функция — это идентификатор. Строковые имена не нужны.

g := toulmin.NewGraph("filefunc")
w := g.Warrant(CheckOneFileOneFunc, nil, 1.0)
d := g.Defeater(TestFileException, nil, 1.0)
g.Defeat(d, w)

results, _ := g.Evaluate(claim, ground)

Одну и ту же функцию можно переиспользовать в другом графе с другими отношениями поражения:

strictGraph := toulmin.NewGraph("strict")
strictGraph.Warrant(CheckOneFileOneFunc, nil, 1.0)
// Без исключений — тестовые файлы тоже не допускаются

lenientGraph := toulmin.NewGraph("lenient")
w := lenientGraph.Warrant(CheckOneFileOneFunc, nil, 1.0)
r1 := lenientGraph.Rebuttal(TestFileException, nil, 1.0)
r2 := lenientGraph.Rebuttal(GeneratedFileException, nil, 0.8)
lenientGraph.Defeat(r1, w)
lenientGraph.Defeat(r2, w)
// Тестовые + сгенерированные файлы — оба исключения

Отслеживание обоснования оценки

EvaluateTrace отслеживает не только verdict, но и какие правила активировались и какие правила победили другие:

traced := g.EvaluateTrace(claim, ground)
// traced[0].Verdict: +0.6
// traced[0].Trace: [
//   {Name: "CheckOneFileOneFunc", Role: "warrant",  Activated: true,  Qualifier: 1.0},
//   {Name: "TestFileException",   Role: "rebuttal", Activated: true,  Qualifier: 1.0},
// ]

Когда правил десятки, человек может прочитать «почему получился именно такой verdict».

Оценка вычисляется одной формулой

Применён h-Categoriser Амгу (2013):

raw = w / (1 + Σ raw(attackers))
verdict = 2 × raw - 1

• +1.0 — нарушение подтверждено
• 0.0 — оценка невозможна
• -1.0 — опровержение подтверждено

Когда правило срабатывает, оно становится warrant. Когда исключение тоже срабатывает, оно становится attacker. Формула вычисляет баланс сил и выдаёт verdict. А если есть исключение из исключения? Оно становится attacker атакера, и исходное правило восстанавливается. Принцип компенсации (Compensation) — свойство, которому удовлетворяет только h-Categoriser.

Три уровня силы правил

Применена классификация Нюта (1994):

Strict-правила отклоняют атакующие рёбра. Defeater только атакует, собственной оценки не имеет. Это структурно выражает уровень принудительности правила.

Чем отличается от Rego

Rego — широкий: экосистема интеграций с Kubernetes, Terraform, Envoy. toulmin — глубокий: в нём есть то, чего нет в Rego (defeasibility, qualifier, backing).

Перемещение Qualifier

В оригинальной модели Тулмина Qualifier прикреплён к Claim. «Вероятно, этому пациенту следует назначить пенициллин» — модальный квалификатор, выражающий степень уверенности в утверждении.

Движок toulmin переместил Qualifier с Claim на каждое Rule. В движке правил claim — это всего лишь объект проверки. «В этом файле 3 функции» — констатация факта, к которой степень уверенности неприменима. Качество оценки определяется уверенностью в правиле:

• «Одна функция на файл» — qualifier 1.0 (определённое правило)
• «Рекомендуется до 100 строк» — qualifier 0.7 (гибкое правило)

Qualifier каждого Rule становится начальным весом w(a) в h-Categoriser, а итоговый verdict выполняет роль, которую в оригинальной модели Тулмина играл Qualifier, — степень уверенности в оценке.

Эмпирическая проверка: преобразование 22 правил filefunc в модель Тулмина

filefunc — инструмент для конвенций структуры кода при LLM-нативной разработке на Go. Все 22 правила были преобразованы в warrant модели Тулмина.

Классификация по силе

Большинство — strict. Конвенции структуры кода по своей природе минимизируют исключения.

Количественные результаты

В fullend количество файлов выросло с 87 до 1 260. Файлов стало значительно больше, но средний LOC упал с 244 до 25.4. Нарушения SRP — 66, нарушения depth — 148, все сведены к нулю.

Теоретическая основа

Оригинальных теорий нет. Всё основано на существующих исследованиях:

Оригинальность — в открытии того, что они связаны. 60 лет философия (Toulmin), логика (Nute) и теория аргументации (Amgoud) существовали по отдельности, и все они сошлись в одной точке — программном движке правил.

Вычисление контрактов

Верховенство права работает не потому, что судья умён. А потому, что структура принуждает к вынесению решения. Есть правила, объявлены исключения, и по доказательствам выносится приговор.

toulmin перенёс эту структуру в код.

• Warrant = статья закона
• Backing = цель законодателя
• Strength = императивная норма vs диспозитивная норма
• Rebuttal = исключительная оговорка
• Claim = дело
• Ground = доказательства
• h-Categoriser = приговор

Объявляется контракт (warrant), объявляются исключения (rebuttal), подставляются доказательства (ground), и вычисляется оценка (verdict).

Не человек решает. Формула вычисляет.

Acc(a) = w(a) / (1 + Σ Acc(attackers))

Граф можно определить в YAML

Без Go-кода структура графа объявляется в YAML, из которого генерируется код:

graph: filefunc
rules:
  - name: CheckOneFileOneFunc
    role: warrant
    qualifier: 1.0
  - name: TestFileException
    role: rebuttal
    qualifier: 1.0
defeats:
  - from: TestFileException
    to: CheckOneFileOneFunc

toulmin graph filefunc.yaml    # генерация graph_gen.go

Достаточно написать функции правил на Go. Структуру графа объявляет YAML.

MIT License. github.com/park-jun-woo/toulmin