/
Поиск
RU
ENRU

Словарь языка

Термины kola на одной странице — в том значении, в каком их используют сообщения компилятора и обе карты: SPEC-CARD.md для языка и STD-CARD.md для стандартной библиотеки (kola help spec-card, kola help std-card).

Значения и типы

  • данные (data): простые копируемые значения, внутри которых нет ничего владеющего: целые числа, bool, (), char, f64, ссылки, а также составленные из них структуры, перечисления и кортежи. Копируются свободно и сравниваются через == по значению, в том числе через ссылки (по содержимому, никогда по адресу).

  • владеющее значение (owning value): значение, которое перемещается и никогда не копируется: владеющий Vec[T] (Vec по значению), Map, значение, содержащее &mut, и всё, что несёт что-то из этого в поле или в полезной нагрузке. Передача по значению его перемещает, и читать источник после этого — ошибка. Вместо этого его заимствуют через &v или &mut v.

  • ресурс (resource): линейное значение, объявленное через resource struct: файл, сокет, дескриптор потока, капабилити. Его нельзя скопировать и нельзя молча потерять. Многие ресурсы оборачивают дескриптор операционной системы, например файловый дескриптор (небольшое целое число, которым ОС обозначает открытый файл или сокет), и закрыть его нужно ровно один раз.

  • линейность (linearity): правило, по которому ресурс расходуется ровно один раз на каждом пути выполнения. Забыть о нём — ошибка компиляции (resource `t` is not consumed on this return path), израсходовать дважды — тоже.

  • расходование (consumption): способы завершить жизнь ресурса: передать его функции, принимающей его по значению (self: T), вернуть, переместить дальше или разобрать.

  • разбор (destructuring): разбиение значения на поля с помощью образца, как в let Wal { entries: _ } = self;. Для ресурса так расходующая функция заканчивает значение. Каждое поле должно быть названо; .. нет.

  • перемещение (move): передача значения новому владельцу. Любая позиция, типизированная по значению, перемещает владеющее значение или ресурс: аргумент вызова, let, поле в литерале структуры, полезная нагрузка варианта вроде Some(v), сообщение в канал, контекст потока, присваивание в поле, возврат. Данные в таких позициях копируются.

  • unit (): тип с единственным значением, которое тоже пишется (). Его возвращает функция без -> T.

  • литерал (literal): значение, записанное прямо в исходнике: 42, 0x2A, 0o644, 0b1010, 1.5, "text", f"n={n}", b"bytes", r"raw", [1u8, 2u8], Point { x: 1, y: 2 }. _ между цифрами — разделитель. Символьного литерала нет.

  • суффикс типа (type suffix): 3u64 — это число 3 типа u64. Литерал без суффикса берёт ширину из контекста (аннотация, параметр, другой операнд, позиция индекса, где это usize). Если ширину ничто не задаёт, это u64, или i64, если туда когда-нибудь попадает отрицательное значение.

  • widen / narrow / wrap: единственные преобразования между числовыми типами, все явные. widen[u64](x) расширяет без потерь, narrow[u8](x) возвращает Option[u8], wrap[i16](x) переосмысливает младшие биты и никогда не вызывает трап. as нет.

  • срез (slice): представление массива или Vec, тип &[u64] или &r [u8]. У него есть .len, индексация xs[i] и подсрезы xs[a..b]. Ничего не копируется.

  • правило представлений (view rule): пока представление места (&v[i], подсрез, обход v циклом for) ещё используется, это место нельзя записывать, увеличивать, уменьшать или перемещать ни под каким другим именем. Исправление: сначала закончить чтение, скопировать значение или сохранить индекс и прочитать заново после изменения.

  • str: представление текста в UTF-8 в виде пары (указатель, длина). .len — длина в байтах, .bytes — то же представление как &[u8]. Обычный литерал "..." — статические данные и подходит любому региону.

  • подстановка (interpolation): литерал f"..." подставляет выражения в текст: f"n={n} sum={a + b}". Обычный "..." ничего не подставляет. Привязанный к имени f-литерал выделяет память: в регионе места назначения, если тип назначения его называет, иначе в ближайшем открытом region, а если нет и его, компилятор литерал отвергает. Переданный прямо в параметр &str на время вызова, он ничего не выделяет.

  • дженерик (generic): параметр в квадратных скобках. Имена с заглавной буквы обозначают типы, со строчной — регионы: fn first[T: data](xs: &[T]) -> Option[T]. Неограниченный T считается линейным; T: data делает его копируемым; T: move допускает данные и владеющие значения, но не ресурсы. Параметр [const N: usize] связывает число времени компиляции, которое можно использовать как длину массива. Угловых скобок нет.

  • мономорфизация (monomorphization): компиляция дженерика созданием отдельной специализированной копии для каждого набора типовых аргументов — примерно так, как если бы вы вручную написали first_u64 и first_u8. Каждый вызов идёт прямо к известной функции; никакого поиска нужной функции во время выполнения, как с виртуальными методами C++, нет.

  • fn-ссылка (fn reference): имя функции верхнего уровня, использованное как значение, как в seq::sort(xs, less_u64). В её тип входит ряд эффектов: fn(u64) -> u64 !{}. Она ничего не захватывает, потому что замыканий нет.

  • тип уровня модуля (module-scoped type): struct или enum принадлежит своему модулю, как функция. Внутри модуля тип называют просто по имени; снаружи — через use M::T; и затем T, либо M::T в позиции типа.

Память

  • арена (arena): блок памяти, который раздаёт выделения по порядку, сдвигая указатель за каждое из них, и освобождается целиком. Поэтому выделение очень дёшево. По отдельности в арене ничего не освобождается.

  • регион (region): лексический блок region r { ... } со своей ареной. Всё, что в нём выделено, освобождается на закрывающей скобке. region r from m { ... } берёт память для арены из бюджета m.

  • alloc in: выделение в регионе: alloc in r mut Vec::new() даёт &r mut Vec[T]. Изменяемость выбирается там, где значение выделяется.

  • heap: встроенный регион, который живёт столько же, сколько программа. Сборщика мусора нет; память heap возвращается, когда процесс завершается. Обычный строковый литерал — статические данные и может иметь тип &heap str. Хранилище владеющего Vec всегда лежит в heap, поэтому его рост — эффект alloc(heap).

  • ссылка в регион &r T: ссылка, в тип которой входит её регион. Её можно свободно копировать, но она не может пережить регион, и это проверяется при компиляции.

  • ссылка на время вызова &T / &mut T: ссылка, которая бывает только типом параметра. Вызываемая функция пользуется ею, пока идёт вызов, но не может её сохранить или вернуть. Это форма параметра по умолчанию.

  • параметр-регион (region parameter): имя со строчной буквы в квадратных скобках, как в fn body[r](b: &r [u8]) -> &r [u8]: функция работает с тем регионом, который есть у вызывающего. При вызове регион не пишут, он выводится.

  • lend: разделяемое представление ресурса на время региона: let v: &r Wal = lend wal in r;. Ресурс заморожен, пока регион не закроется. lend mut нет.

  • Pool[T]: слэб (фиксированный массив ячеек одного размера) для долгоживущих данных со структурой графа, где ячейки можно освобождать по одной, чего регион не умеет. Ёмкость резервируется в new и целиком списывается с бюджета, но страницы памяти затрагиваются, только когда ячейка используется впервые. insert при заполненном пуле вызывает трап TrapKind::Capacity; try_insert вместо этого возвращает элемент обратно. drain_next извлекает произвольную занятую ячейку при разборе пула. Pool не может пересечь границу потока.

  • поколенческий дескриптор Gen[T]: квиток, который возвращает insert. Он отвечает на два вопроса: та ли это ещё ячейка, которую вам дали (после remove старый дескриптор даёт None, даже если ячейка занята снова), и из этого ли пула вообще дескриптор (дескриптор, использованный с другим пулом, детерминированно промахивается).

  • владеющий Vec: Vec::new(), привязанный по значению, с хранилищем в heap. Его буфер переходит между потоками без копирования. Если память должна вернуться на скобке, Vec выделяют в регионе.

Эффекты и капабилити

  • эффект (effect): какого рода действия функция может совершать. Их пять: alloc(r) (выделяет память в регионе r), io (обращается к внешнему миру через капабилити), hw (привилегированная или чувствительная к порядку машинная операция), block (может заблокироваться или уснуть) и log (пишет в журнал процесса). Эффекты говорят, что за действие; капабилити — над чем.

  • ряд эффектов (effect row): !{...} в конце сигнатуры, после типа результата: fn f(x: &T) -> u32 !{io}. Каждая публичная функция его указывает; закрытая может оставить его на вывод.

  • чистая функция (pure function): функция с рядом !{}: доказуемо не выделяет память, не выполняет ввода-вывода и не блокируется.

  • hw: машинный эффект — для операций, которые ядро или драйвер выполняют над самим железом: маскирование прерываний, обслуживание кэшей и TLB (кэша процессора для трансляции адресов), барьеры памяти (инструкции, не дающие процессору переставлять обращения к памяти через них), MMIO и атомики. В ct fn он запрещён, а сами операции никогда не переставляются и не удаляются. Обычные чтение и запись через RamWindow остаются под io.

  • капабилити (capability): значение, дающее доступ к одной части мира. Полномочий из воздуха нет, поэтому каждая библиотечная операция с эффектом принимает капабилити. Маркеры полномочий вроде Clock, Rng, Fs, Dir, Dial, Stdout можно просто бросить. Mem и линейные дескрипторы вроде File, Conn, Child нужно израсходовать.

  • Sys: корневой набор, который среда выполнения передаёт в main и больше никуда: sys.clock, sys.rng, sys.mem, sys.fs, sys.dial, sys.listen, sys.stdout, sys.stdin, sys.stderr, sys.args, sys.env, sys.tty, sys.ping, sys.proc, sys.netlink, sys.raw_ip, sys.mmio, sys.cpu, sys.dev, sys.window и sys.inherited. main принимает его по значению или не принимает ничего.

  • полномочия из воздуха (ambient authority): власть, доступная откуда угодно, — глобальный print, файловая система или часы. В kola их нет.

  • ослабление (attenuation): сужение полномочий при передаче вниз по вызовам. main держит всё и передаёт помощнику только &sys.clock. Часть сужения выражена в типах: dir.ro() даёт DirRo без операций записи, w.atomic() оставляет окну только атомарные операции, а dial.to_host(host, port) достаёт до одного адреса. Капабилити перемещается один раз, поэтому clock.split(), rng.split() и dial.split() выдают рабочему потоку его собственную.

  • выдача (grant): полномочия за пределами рабочего каталога и самого процесса (каталог, бинарник, устройство, аппаратное окно), которые выдаёт по имени тот, кто запускает программу. kola run --fs-root db:ro=/abs выдаёт, а sys.fs.root(b"db") ищет, возвращая None, если ничего не выдано. У каждого флага есть двойник в окружении, например KOLA_FS_ROOT_db. Выдачи исходят от оператора и никогда — от родительского процесса.

  • log: единственный эффект, которому не нужна капабилити, потому что приёмник работает только на запись: программа не может прочитать написанное и, значит, не может через него управлять ходом выполнения. Приёмник и уровень выбираются один раз — флагами --log и --log-level или переменными KOLA_LOG и KOLA_LOG_LEVEL. Функции — std::log::{error, warn, info, debug}.

  • бюджет памяти (memory budget): часть капабилити Mem, отрезанная через sys.mem.split(n). Она питает регион (region r from m), а линейность заставляет вернуть её через sys.mem.absorb(m). Превышение бюджета вызывает трап TrapKind::Budget.

  • окно (window): выданный диапазон памяти или адресного пространства с длиной и непрозрачной базой. kola работает со смещениями, а не с указателями. RamWindow — память, общая с железом, например кольцо дескрипторов буферов, которое читает сетевая карта. MmioWindow — регистры устройства, отображённые в память (MMIO, memory-mapped I/O: чтение или запись по такому адресу обращается к устройству, а не к RAM). IoWindow — портовый ввод-вывод x86, старое отдельное адресное пространство для устройств. У каждого обращения есть контракт границ, и прувер может снять его так же, как для индекса массива.

  • модель устройства (device model): при обычном run или test за окном или выданным устройством нет настоящего железа, поэтому его поведение задаёт модель на kola, подключаемая через --sim-mmio, --sim-io или --sim-dev. Выдача без модели отвергает тест при запуске.

  • Proc / Child: sys.proc.spawn(bin, argv, env, disp, slots) запускает бинарник, выданный оператором по имени (--proc-bin ffmpeg=/abs). env задаётся явно, так что ничего неявного в дочерний процесс не попадает. disp: Stdio — это Inherit, Piped или Null. Child линейный: его расходует wait или kill. ExitStatus — это Code(u8) или Signaled(Signal), и сигнал — это имя, никогда не число.

Ошибки и контракты

  • трап (trap): детерминированная остановка, когда нарушено допущение: переполнение, выход за границы, ложный контракт, unwrap от None, явный trap("msg"). Никакой раскрутки стека и никакого продолжения с мусором.

  • домен отказа (fault domain): то, что убивает трап. По умолчанию — весь процесс (в тесте — тест). Блок domain d { ... } recover(t: Trap) { ... } сужает его до блока: трап в теле разбирает d и запускает recover. Домен — это регион, который ещё и перехватывает трап. Трап внутри recover фатален.

  • Trap: простые данные, которые получает recover. t.kind — одно из Bounds, Arith, Req, Ens, Inv, Assert, Unwrap, Explicit, Budget или Capacity, а t.site — module:line, никогда не путь в файловой системе.

  • контракт (contract): проверяемое условие в сигнатуре. Соблюдается всегда: либо доказывается при компиляции, и тогда проверка исчезает, либо проверяется во время выполнения с трапом. Режима сборки, который его убирает, нет.

  • req: предусловие, обязанность вызывающего: req i < xs.len.

  • ens: постусловие, обещание функции; ret обозначает результат: ens ret <= 100.

  • inv: инвариант структуры-ресурса, записываемый последним элементом её тела: resource struct Ring { head: usize, inv head < 8 }. Проверяется при создании и на границах функций.

  • assert: проверяемое утверждение внутри тела, с тем же правилом снятия, что и у контрактов. Его выражение ничего не должно менять.

  • Option / Result: ожидаемые исходы в виде значений. Option[T] — есть или нет; Result[T, E] — успех или ожидаемая ошибка.

  • ?: досрочный возврат. Достаёт v из Ok(v), а при Err возвращает ошибку из текущей функции. Живой ресурс в точке ? — ошибка линейности.

  • отброшенный Result: ошибка компиляции. Его обрабатывают через match, ? или .unwrap() либо отбрасывают намеренно: let _ = ...;.

  • unwrap: достаёт значение из Option или Result и вызывает трап на None или Err. Перемещает своего получателя.

  • соглашение о результатах ОС: операция, обращающаяся к ОС, отвечает Result[T, (E, OsErr)], где E — семейство действия (FsErr, NetErr, IoErr, DevErr, ProcErr, NetlinkErr), а OsErr — собственное обозначение ошибки в ОС, например NoEnt. «Пока ничего нет» никогда не ошибка: операция try_* отвечает Ok(None).

  • layout_assert: элемент уровня модуля, layout_assert[Point](8, 4);, утверждающий размер и выравнивание типа в C. C-бэкенд превращает его в _Static_assert; интерпретатор считает его пустой операцией. size_of в kola нет.

Данные, которым нельзя доверять, и данные, которые нельзя раскрыть

  • untrusted: маркер параметра для входа от атакующего: байтов из сети, файла, стандартного ввода или от другого процесса. От него не может зависеть ни req, ни ens, ни inv, потому что контракт — утверждение о вызывающем, а у этих байтов вызывающего нет. Значение проверяют во время выполнения и возвращают Result или Option. kola report tainted-reqs находит кандидатов в существующем коде.

  • Secret[T]: непрозрачная линейная коробка для данных, которые нельзя раскрыть. Secret::wrap(x) кладёт значение в коробку, Secret::expose(&s) — единственный способ прочитать, Secret::wipe(s) расходует и затирает, Secret::eq(&a, &b) сравнивает за константное время, а Secret::wipe_bytes(&mut buf) затирает буфер, коробкой которого вы не владеете. Секрет длины, известной только во время выполнения, — это Secret[Vec[u8]]. Ссылку в коробку положить нельзя: затёртый указатель оставил бы байты за ним нетронутыми.

  • Entropy[[u8; N]]: коробка, которая помнит происхождение байтов: энтропия ОС, непредсказуемая для противника. Entropy::draw[[u8; N]](&mut rng) создаёт её, Entropy::expose(&e) читает. Entropy::of(x) для тестовых векторов kola audit отвергает на любом пути, который начинается не в test. Она не линейна и не является Secret; ключу может понадобиться и то и другое.

  • ct fn: функция константного времени. Время её работы и порядок обращений к памяти могут зависеть от формы параметров (ширины, длины), но не от их значений. Для криптографии это важно: если сравнение пароля или ключа завершается быстрее, когда неверен первый байт, атакующий, способный засекать время, восстановит секрет байт за байтом. Внутри такой функции каждый параметр секретен, если не помечен pub, и чекер отвергает над производными от секрета значениями ветвление, индексацию, деление, арифметику с трапом и секретную величину сдвига, а также вызовы функций без ct. См. Константное время.

Инструменты и проект

  • SPEC-CARD: весь язык на одной карте и источник истины. Диагностики ссылаются на её разделы, как в error[card §8]. Чего нет на карте, того нет в языке. Её спутник, STD-CARD, описывает стандартную библиотеку: типы, операции капабилити и SIMD.

  • golden: каталог golden/ в репозитории с эталонными примерами программ — от hello world до песочницы и диспетчера выходов виртуальной машины. Все они компилируются и проходят тесты.

  • kola: компилятор, один бинарник со встроенной стандартной библиотекой. Команды: check, run, test, build, ir, report, query, audit, pack, security, cc, lsp, mcp и help. См. Под капотом.

  • интерпретатор (interpreter): исполнитель за kola run и kola test и эталон, с которым сравнивается каждый бэкенд. Работает вместе с JIT; --no-jit даёт чистый обход дерева.

  • дифференциальный тест (differential test): kola test запускает каждый тест в интерпретаторе и через C-бэкенд и сравнивает ответы; расхождение даёт код выхода 3. --interp или --native запускают только одну сторону.

  • KIR: проверенное промежуточное представление, которое потребляет каждый бэкенд; в нём записано решение по каждой проверке. Его печатает kola ir. См. IR-0.

  • report checks: список всех обязательств в файле с пометкой, доказано ли каждое при компиляции или оставлено проверкой времени выполнения. «0 runtime» — планка для кода уровня ядра. Родственные отчёты — reachable, leaks, regions, effects, secrets, tainted-reqs и stack-frames; полный список даёт kola help report.

  • прогон с зерном (seeded run): прогон, в котором весь недетерминизм (случайность, время, порядок ввода-вывода, планирование потоков) выводится из одного числа. kola test --sim --seed N повторяет тот же прогон бит в бит.

  • симулятор (--sim): капабилити, подменённые детерминированными двойниками: виртуальные часы, источник случайности от зерна, симулированные файловая система и сеть с внесением сбоев, пустое окружение. У Proc двойника нет; выданный запуск процесса действительно выполняется.

  • kola.pack: манифест пакета: имя, версия, корень исходников, зависимости и бюджет капабилити [caps] allowed с поимёнными списками (fs_roots, proc_bins, devices, dial_hosts, netlink, списки окон и другие). [caps.tests] и [caps.examples] расширяют его только для тестов и примеров. kola audit завершается ошибкой, если код выходит за бюджет. Бюджет ограничивает то, что пакет может взять из корневого набора; полномочия, полученные параметром, перечисляются отдельно, в строке reaches: отчёта аудита.

  • журнал путаницы (confusion log): docs/confusion-log.md в репозитории — запись конструкций, в которых люди или модели устойчиво ошибаются. Конструкция, которая сбивает с толку, считается дефектом самой конструкции или карты.