Структурный размер значения доказывается тотальным, если спускаться в поле образца, а не в результат поиска по ключу
flang/self/bounded.flang считает «Размер значения» ОБЫЧНОЙ функцией, не тотальной, и причина названа там же: чтобы отличить вариант от записи, он ищет ключ fields поиском по ключу, а анализ убывания результат поиска спуском не признаёт — он признаёт поле образца, поле записи и элемент коллекции.
Ту же величину можно посчитать ТОТАЛЬНОЙ формой, и правка — не в анализе, а в арифметике: размер варианта РАВЕН размеру самого fields (единица за узел плюс части — в обоих случаях одно и то же число). Значит вместо «взять поле fields и сложить его части» достаточно «взять поле fields и позвать себя на нём», а это уже спуск в «голова».«значение» из образца голова и хвост.
Чем подтверждено. flang/self/hotswap.flang (ветка work/goryachaya-zamena): четыре функции — «Размер узла», «Есть поля варианта», «Размер по всем полям», «Размер по полям варианта» — объявлены тотальными и доказаны структурой (flang check --proof). Числа совпадают с размерЗначения свидетеля побайтово на всех 4918 случаях сверки, включая 21 настоящее накопленное состояние процессов.
Чем ограничено. Первая редакция была отвергнута анализом с точным объяснением: список полей передавался вторым доводом, а спуск шёл по первому — «аргумент 1 — часть параметра «остаток», а сравнивается с параметром «все» на своей позиции». Пришлось развести поиск ключа и сумму по всем полям в две функции, каждая об одном доводе. Правило общее: если в цикле рекурсии убывает не тот довод, который стоит на первой позиции, анализ откажет — и откажет по делу.