1. Куча / Говнокод #29291

    0

    1. 1
    2. 2
    3. 3
    4. 4
    5. 5
    6. 6
    7. 7
    8. 8
    9. 9
    Let ValidVM : Type := {vm : VM | Fresh.is_valid_ref parent (ref_ctr vm) = true}.

    #[refine]
    Definition spawn : MFun ValidVM VM :=
      {| morphism (vm0 : ValidVM) (vm : VM) :=
          let (vm0, Hparent_valid) := vm0 in
          do_spawn vm0 vm Hparent_valid
      |}.
...

    Запостил: CHayT, 26 Октября 2026

    Комментарии (10) RSS

    • ava CHayT 9 дней назад # 0

      Продолжаем цирк с формализованными клоунами акторами. Как я уже жаловался, питух нашёл дыру в моей изначально красивой теории, которую пришлось закрыть одним глупым инвариантом. И эта тварь теперь лезет повсюду. Вот такие говноморфизмы в категории говнобинарных говноотношений между говноквоитентными говномножествами пришлось пилить, например.
      Ответить

      • ava CHayT 9 дней назад # 0

        Суть дыры, кстати, в следующем: есть планировщик кок-акторов, в котором они живут. Его можно представить как некий курятник. Акторы могут нести яички, из которых вылупляются новые акторы. У каждого актора есть уникальное имя, которое, для того, чтобы вылупление новых цыплят коммутировало, генерится из родословной. Идея в том, что все курочки в курятнике ведут родословную от одного яичка, то есть кличка у каждой курочки уникальная. Теперь представим, что в курятник каким-то образом попало постороннее яичко. Из него может вылупиться курочка с дублированной кличкой, и тогда owari da, the курятник has fallen.
        Ответить

        • ava j123123 Вчера # 0

          Почему б не сделать дерево питушни? Вылупившееся знает о своем родителе. Если в курятник попадает посторонее яичко, оно знает, что снесено от другой курочки в другом курятнике. Можно условиться, что курицы в другом курятнике обязаны всегда наследоваться от куриц, которые так или иначе по цепочке связаны с главной первородной курицей из какого-то курятника
          Ответить

          • ava CHayT Вчера # 0

            Дерево медленно. Его же надо будет полностью обходить каждый шаг симуляции. Писать зипперы деревьев на Coq я ещё не совсем ебанулся. Плюс, это приведёт к зомби-курицам. Инвореант же нужно апдейтить только когда курочка вылупляется или отправляется в лучший мир.
            Ответить

            • ava CHayT Вчера # 0

              P.S. Недавно, кстати, попробовал на этом проекте нейропитуха, результат следующий: он напрувил кучу лемм, перепахал весь код, заменив половину тактик на exact, и в результате получил такую-то хорошую теорию, жаль только она оказалась vacous. Потом чистил вилкой это всё долго. Такие дела.
              Ответить

    • ava nemyx 9 дней назад # 0

      Ничего не понимаю. Переведи на «PHP».
      Ответить

      • ava Rooster 9 дней назад # 0

        Тоже не понимаю. Сложна.

        Понял только из комментов ЧайТа, что там что-то про дискриминацию кур по происхождению.

        А может и не понял.
        Ответить

        • ava CHayT 9 дней назад # 0

          Проблема в требовании, чтобы все айдишники процессов были уникальными, что в совокупности с методом их генерации приводит к багру.

          > что-то про дискриминацию кур по происхождению

          Слова-триггеры сработали ^___~ Знячит возможно, что сейчас кто-то трясётся от невозможности оставить анонимный ответ, сравнивающий меня со своим нелюбимым тиктокером. Извлекаем профит из унылого октябрьского пиздеца.
          Ответить

    • ava CHayT 6 дней назад # 0

      Всё, этот инвариант убил к хуям коммутацию, RIP:

      (** [quasi_commute f g f' g']: [f] followed by [g] quasi-commutes
      with [g'] followed by [f'].

      The difference from [commute]: plain commutation of [f] and [g]
      reorders the very same two operations — the swapped run
      performs [g] after [f].  Here the swapped run performs the
      *re-parameterized versions* [g'] and [f'] of the two operations,
      while the order of the given run is preserved up to the
      equivalence of results.

      With [f' := f] and [g' := g] this is exactly [commute f g]. *)
  Definition quasi_commute_def (f g f' g' : T) (x y : A) :=
      (x ~[g ∘ f]~> y -> exists{y' == y}, x ~[f' ∘ g']~> y') /\
      (x ~[f ∘ g]~> y -> exists{y' == y}, x ~[g' ∘ f']~> y').


      Добро пожаловать в т.н. ``квази-коммутацию''. Но зато теперь вылупление и подыхание акторов ``квази-коммутирует'', почти как и задумывалось.
      Ответить

      • ava CHayT 6 дней назад # 0

        Теперь дело за малым, лол: квази-адаптировать вот это говно: https://govnokod.ru/27116
        Ответить

    Добавить комментарий