- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
(* https://coq.inria.fr/library/Coq.Init.Datatypes.html *)
(* Basic boolean operators *)
Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
Definition orb (b1 b2:bool) : bool := if b1 then true else b2.
Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
Definition xorb (b1 b2:bool) : bool :=
match b1, b2 with
| true, true => false
| true, false => true
| false, true => true
| false, false => false
end.
Definition negb (b:bool) := if b then false else true.
Infix "||" := orb : bool_scope.
Infix "&&" := andb : bool_scope.
На первый взгляд этот ваш Coq (питух) выглядит как очередной ML-язычок.
Follow us!
Или NOR: https://en.wikipedia.org/wiki/NOR_logic
Поэтому в булеанах нет ничего специального, можешь сам такие же запилить.
А так -- да, ML'ка по синтаксису. OCaml, емнип, вообще пилили специально чтобы петуха на нём писать.
А зачем делать такой сложный базис? В "Metamath" базис намного проще.
Почему Coq не сделали с гомоиконностью?
Из-за этого минималистичный CoC (calculus of constructions) превратился в раздутый CIC (calculus of inductive constructions).
Разговаривать словечки
Выясняли кто умней
У кого матан сложней!
Х.з., видимо нотации показались более удобными. Они и при отладочном выводе работают в обратную сторону, в отличие от универсальных гомоикон. Ну и на ядро никак не влияют.
А ltac тьюринг полный, что в ядро тащить вообще нельзя.
А почему они показались более удобными? Тут наверное причина только в том, что люди, запиливавшие Coq, были ML-еблюбами
Фиг знает, потому что это чисто синтаксическое преобразование без всяких подводных камней?
На s-выражениях такая фича выглядела бы как макрос с дословной подстановкой аргументов без какой-либо обработки данных.
Да, это называется "макрос".
> На s-выражениях такая фича выглядела бы как макрос с дословной подстановкой аргументов без какой-либо обработки данных.
И в чем проблема?
В общем моя твоя не понимать
Т.е. если "нотация" -- это "макрос", то очень-очень ограниченный.
Можно даже сделать специальный макрос, который принимает макрос в качестве аргумента и убеджается в том, что этот макрос соответствует некоторым критериям, и вот только тогда он в что-то раскрывается. А иначе ошибка компиляции.
Не вижу проблемы короче. Вот если б наоборот, макросы были более ограничеными...
А сама гомоиконичность это не только про макросы, а и про удобство работы с AST.
https://archive.jlongster.com/Lisp--It-s-Not-About-Macros,-It-s-About-Read
Собственно:
> Once you understand that Lisp code is data (lists of atoms), you realize that you can use read to read in Lisp code as data. And since Lisp comes with a set of functions for elegantly processing lists, suddenly it's really easy to parse Lisp code.
> You just wrote a parser that turns all define expressions into lambda expressions.
> That should impress you. How would you do that in Python? Or Javascript? You need access to the AST and need to learn all the internal methods for parsing it. Lisp code is an AST.
Т.е. профит тут в синтаксиальной однородности, что можно легко генерить и легко читать эту хрень, не думая при чтении/генерации о всякой срани типа "Precedence" и "Associativity" как в https://coq.inria.fr/refman/language/coq-library.html#init-notations
А суть не в макросах, а в однородном синтаксисе. Полноценные макросы могут тоже присутствовать, только они могут раскрываться как какой-нибудь сишный препроцессор, и потом уже над "раскрытым" представлением можно делать какие-то манипуляции.
Зачем однородный синтаксис? Чтобы удобно конструировать и читать это всё, чтобы можно было удобно это в что-то другое экспортнуть. Чтобы не держать в голове правила приоритетов каких-то операций, и что какая-то там функция может быть размазана на несколько "инфиксных операций". Вот например https://coq.inria.fr/refman/language/coq-library.html#init-notations
Тут есть такая штука "_ <= _ <= _" напоминающая какой-то японский смайлик. А по-сути эта функция от трех аргументов, которая про "(a <= b) && (b <= c)" А в каком-нибудь лиспе это можно записать как (and (<= a b) (<= b c)) и это дерево.
И я допустим могу по этому дереву ходить какими-то "итераторами" и что-то в нем добавлять/переставлять, это просто и понятно. А зачем это делать через два инфиксных оператора? И еще приоритеты какие-то? Зачем? Зачем?
Но проблемы с приоритетом операций тут не будет, и такой макрос до раскрытия тоже можно рассматривать как дерево
А как мне рассматривать "как дерево" эти нотации с приоритетами?
Просто для удобства пользователя эта штука вводится и выводится как a <= b <= c.
Не нравятся нотации? Выруби их в переменной или галочкой в IDE. Будешь читать портянки говна именно так, как их видит прувер.
Правда вместо чисел у тебя будут S (S (S (S O)))). Но это ведь мелочи...
https://youtube.com/watch?v=TJKgq_DcJCw
А почему б пруверу сами эти нотации не видеть как дерево, и не оттранслировать теоремы-леммы в теоремы-леммы в терминах этой другой нотации? Например, если мне надо что-то доказать, что завязано на десятичную систему счисления, ну скажем https://ru.wikipedia.org/wiki/Проблема_196
и вот я описываю правила отображения S (S (S ... в какой-то там (DEC 1 9 6), и этот S ( S ( S ... может сложиться в этот DEC и наоборот. И описываю теорему про (DEC 1 9 6) и пруваю в терминах этой же нотации
> Правда вместо чисел у тебя будут S (S (S (S O)))). Но это ведь мелочи...
А обязательно ли числа "хранить" такой питушней в представлении для прувера? Можно ж как-нибудь
Ну и какая-то питушня может биективно отобразить (DEC 1 1) в (S (S (S (S (S (S (S (S (S (S O)))))))))) и наоборот.
Нет, но эта форма очень удобна для индуктивных пруфов.
А если у тебя какое-то очень большое число, которое в S (S (S (S ... форме не будет помещаться в оперативной памяти? Например, если ты захочешь взять самое большое число, для которого доказана его простота, и захочешь это проверить в Coq, как ты с этим числом будешь работать?
Например https://ru.wikipedia.org/wiki/Наибольшее_известное_простое_число
А если это будет простое число, которое числом Мерсенна не является?
Ну тут скорее я буду доказывать, что мой тест простоты в общем виде соответствует спеке.
А потом уже выгружать код из петуха и гонять его на твоём числе.
А для доказательств в общем виде большие числа обычно не нужны.
Мне в нотациях не нравится, что там какие-то "приоритеты" и "ассоциативность" есть, которые надо иметь в виду для понимания смысла. Можно сделать нотации на макросне, где ничего такого нет. Вот вместо "a <= b <= c" сделать "(@N a <= b <= c)" - и нету никаких проблем с ассоциативностью. Если надо записать "a <= b <= c + d" то просто пишешь "(@N a <= b <= (@N c + d))" и нет никаких неоднозначностей.
И эту макросню точно так же можно зажимать и разжимать
Дык всё просто...
Я пишу a <= b <= c. Петух это видит как and (le a b) (le b c), но выводит мне как a <= b <= c.
Я пишу remember (a <= b) as d. Петух видит результат этой замены как and d (le b c), но выводит мне d /\ b <= c.
А если ты напишешь "and (le a b) (le b c)" то он тебе все равно выведет "a <= b <= c"? Т.е. туда понапихали какую-то логику зажатия питушни в эту вот нотацию? А по какому алгоритму оно в эти нотации зажимает? Я могу эти правила зажатия реальной питушни в нотацию контролировать?
Именно так.
> А по какому алгоритму оно в эти нотации зажимает?
А фиг знает, я особо не вникала. Первую подходящую, скорее всего. Или по приоритетам которые на них написаны.
Ты пишешь что-то в духе Notation "a <= b <= c" := and (le a b) (le b c) чтобы ввести новую нотацию. И она начинает в обе стороны работать.
В сишке некоторые макросы необратимы (конкатенация, стрингификация).
И, кстати, почему для asciiz-строк puts, а не putz?
Да, например представим что есть код, в котором очень много повторяющейся хуйни, которую можно свернуть в макросню. Я пишу макросню, а потом каким-то хреном этот код зожимаю в эту макросню, чтоб читабельнее было. Какие-нибудь говноIDE так умеют?
Это будет дорогостильноIDE томущо задача нетривиальная
Лучше уж сразу pituz
Вообще, хуита эти ващи нотации-наняции, декоративная питушня какая-то. То ли дело работа напрямую с AST. А нотации эту работу затрудняют т.к. загораживают собой этот самый AST
Можно сделать препроцессор под такую хуйню - один препроцессор раскрывает нотации в AST, другой пытается этот AST обратно зожать в какие-то нотации по хуй знает каким эвристикам.
Точно так же можно рассматривать, как в примере с "@N", потому что это то же самое получилось, только "@N" вдруг сам разрешил конфликты между правилами.
Никак не матчить. Написать что это ambiguous.
> А "a <= b <= (c <= d)".
Как "(and (<= a b) (<= b (<= c d)) )"
> Это красиво звучит, но как этот макрос будет разрешать s-s, s-r конфликты?
Он будет предлагать расставить скобки, чтобы никаких конфликтов не было. Например, если есть "a + b * c * d + e", это никак не будет матчиться.
Если же "a + ( b * c * d ) + e" то тогда всё четко. Т.е. идем от самых глубоко вложенных скобок, видим "( b * c * d )" - есть какое-то общее правило для заматчивания умножений кучи штук, и это раскрывается в (* b (* c d)) допустим. Потом уровнем выше там "a + (* b (* c d)) + e" и тут срабатывает правило для сложения кучи штук, получаем "(+ a (+ (* b (* c d)) e))"
> Придется передавать макросу ассоциативность и приоритет.
Не нужна ни ассоциативность, ни приоритет. (Примечание: ассоциативность не нужна конкретно на уровне матчера "нотаций-макросов", а вообще нужна и полезна, как свойство для доказательства чего-то. Как впрочем и дистрибутивность. Но ты ж не за то, чтобы тебе нотации a*(b+c) перписывали в (a*b)+(a*c), верно?)
Нет никакого высшего глубокого смысла в том, что в математической записи вида "2 + 2 * 2" надо сначала умножать 2 на 2 и потом прибавлять 2 к получившемуся результату. Ккогда-то давно математики так договорились, что у нас вот будут какие-то там приоритеты, вот и всё. Ничего разумного, доброго, вечного в этом нет.
И вообще, надо чтоб префиксная нотация
Тебе нужна ЙАЖА:
1) Инфиксные операторы перегружать нельзя, и пользоваться ими нельзя.
2) Не надо думать ни про какие приоритеты.
Идеальный язык!
Не, я скорее за LISP и FORTH в этом плане. А жаба говно, там даже беззнакового int не сделали.
Любишь беззнаковый size_t в с++?
Так же можно организовать ленивость для логических операций в любом ЯП.
«Хипстеры, хипстеры, эти хипстера – и у них откуда-то денег дохера».
Минимализм это хорошо. Проще реализовывать язык.
Средствами языка можно описывать сложные конструкты..
Другой вопрос как реализовали сам if ... then ... else ...
> синтаксический сахарок для match типов
А match тоже собирают из чего-то более примитивного?
Нет, это полностью аналогично haskell'ному
Логическая импликация.
Вот и в документации пишут:
> (IF_then_else P Q R), written IF P then Q else R denotes either P and Q, or ~P and R
> Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
Второй просто предикат для рассуждений.
Разные логики. Prop — пропозиция конструктивистской логики, а bool — булевской. Второе можно определить внутри первого.
Фу, анскилл. Как на этом сделать логику без анскильного tertium non datur?
Можно на чистом лямбда-исчислении замутить.
Видимо по-другому сложно ограничить рекурсию?
Нет, насколько я знаю, он часть формальной системы.
Как тернарный оператор в сишке наверное
В языке SMTLib для этого есть "ite"
Например вот: https://blog.mikrotik.com/security/meris-botnet.html
Два года назад у чуваков через открытый порт для winbox на микротах увели базу логинов-паролей.
А сегодня по этим паролям к ним зашли, и включили ботнет.
Тут прекрасно всё: и торчащий наружу порт, и аутентификация по паролю в 2021-м году. И это полупрофессиональное оборудование!
> и аутентификация по паролю в 2021-м году
А как надо?
Аунетрифицироваться надо всегда по ключу.
Во-первых его хрен подберешь.
Во-вторых если хакер скоммуниздит базу публичных ключей с устройства, то это не поможет ему подобрать прив[ИНЬЮ_ЗАЕБАЛ_ФИЛЬТР]тный.
В случае пароля конечно тоже не шибко поможет если хеш с солью, наверное
А ключ это асиметричное шифрование. Привтный ключ только у меня есть, а на сервере от него публичный.
Если ты взломал сервер, то ты можешь оттуда получить только публичные ключи пользователей, но не привтные
Если с солью, то будешь брутить. Сбрутить ключ нереально. Насколько реально сбрутить пароль с большой солью и sha2 я не знаю, но думаю что тоже очень сложно
Хакер приходит и спрашивает: ты пароли или ключи принимаешь?
Сервер отвечает: иди нахуй
Но учти, что это security through obscurity т.к. твой сервак всё-таки принимает пароли. И какой-нибудь достаточно тупой бот забудет проверить поддерживаемые способы аутентификации и случайно залогинится, лол.
Ну так а я о чём? ))
> Увидев ключ хакер просто уйдёт в другое место
А на самом деле сервак может принимать пароли тоже
Поэтому такая защита от засирания логов пока что оправдана.
Обычно в протоколах клиент и сервер договариваются о способоах аутентификации
Правда хороший пароль еще хрен сделаешь, а ключ хорош сам по себе.
А еще всякие ботнеты обычно не брутят ключи, бо бессмысленно.
Если включить аунтентификацию по паролю, то будут постоянно лезть "admin pa$$w0rd"
А если про сервер не рассказывать на говнокоде?
Если унесешь порт с 22 куда-то за эвфемерные порты типа 50123, то будут срать чуть меньше.
Если настроишь SSHGuard, то еще меньше будут срать.
Но всё равно найдут, и будут брутить.
RDP и SSH всегда брутят
Больше половины трафика типичного сервера — это китайские и американские боты, пытающиеся набрутить пароль к SSH.
Про диапазоны: «Интернет» разделён на сегменты:
• RIPE — зарубежная Европа и СНГ.
• APNIC — «азиатско-тихоокеанский регион» на муриканском жаргоне — это как раз индусы и китайцы. И Австралия вроде.
• ARIN — североамериканцы.
• LACNIC — латиноамериканцы.
• AFRINIC — африканцы.
Айпишники, принадлежащие этим сегментам, найти очень легко. Для средств администрирования можно оставить RIPE.
Вот пускай лучше эту дыру ковыряют десять ботов из Европы чем десять миллионов ботов из КНР, Индии и Африки.
Это не только ssh касается, но и вообще любого сервиса
ну в общем старое админское правило "чем меньше всего можно -- тем лучше"
А логины тоже брутят?
Да не особо поможет, как мне кажется. Сетки хостеров и интервал, с которым они раздают подсети, точно так же известны будут, а ты в своей подсети вряд ли будешь брать рандомный айпишник из середины. То на то и выйдет.
Хорошо, да. Но одного этого мало, так как ты можешь оказаться за каким-то глубоким NATом, и нок откроется для всей сети
Особенно круто, когда постучал из «жопореза», в котором на одном айпишнике сорок тысяч обезьян.
Вот ты должен послать в порт 1234 пакет, я его дропну
Затем в порт 4234, я его тоже дропну
И только тогда я открою 22
Чел снаружи даже не догадается вообеще что тут что-то есть
Какие обскурити )))
Так надо открывать для одного source port.
Выбирать его самому при подключении что ли?
Если порт тебе назначит операционка, то на каждый сокет будет свой порт
Или вы хотите как-то переиспользовать сокет из которого стучитесь?
С натом — смотря как нат устроен: если он выделяет по порту на каждое логическое соединение — то никак, да; а если он жадный и просто маппит source port клиента в случайный (но фиксированный в рамках сессии) внешний source port — то всё будет работать как и без ната.
Но в общем случае какой-нить тупой клиент этого не умеет, а если я попрошу пользователя стукнуться телнетом или браузером, то ничего не сработает.
А значит нужно нужно или делать умный клиент, или реализовывать нокающий прокси
Вполне возможно, такой у knockd уже и есть
Если нет, надо написать :))
Серверу приходит правильная последовательность с 1.2.3.4:1234, где 1.2.3.4 — внешний IP ната, 1234 — случайно выбранный натом source port. Сервер открывает заветный 22 только для 1.2.3.4:1234. Клиент, которому нат выделил этот порт, радуется, остальные занатовцы зайти не могут.
https://www.cisco.com/c/en/us/support/docs/security-vpn/lock-key/7604-13.html
Дан Makefile
Известно, что ``/opt/petuh/petuh`` существует, и доступен для запуска. Однако же файл не работает ни из какой папки, кроме ``/opt/petuh``.
В чем дело?
Окружение между строчками мейкфайла не передаётся?
Так что если ты хочешь их объеденить, то нужно писать "cd /foo && petuh" например.
Это бывает неожиданно
> Однако же файл не работает ни из какой папки, кроме `/opt/petuh`.
То есть cd /opt && ./petuh/petuh всё таки будет работать?
под "файл" я имел ввиду Makefile
Представляете как удобно писать цикл for, например?
Выглядит как макрос
Потому что у автора "make-файла" случился внезапный приступ эпилепсии, и он посреди ввода путя нажал "return", точку и слеш и вместо "cd /opt/petuh/petuh" написал XYNTY?
Кстати, я еще ни разу не читал мейкфайлы: если они не работают, я просто охуеваю и устанавливаю что-нибудь другое.