Skip to content

🎯 Wave-33 Lane T' — Coq alphabet ext + TENET sparse-skip lemma #646

Description

@gHashTag

Local tracking issue for t27 Lane T' of Wave-33 L-DPC29 ONE SHOT (gHashTag/trinity-fpga#114).

Scope:

  • Extend coq/IGLA/RMarker.v holo_op alphabet with OP_SPARSE_SKIP (sacred 0xE1).
  • Add Lemma tenet_no_star.
  • Add trios-coq/IGLA/Tenet.v with depth-5 alphabet chain Theorem tenet_safe.

Refs gHashTag/trinity-fpga#114

— Vasilev Dmitrii admin@t27.ai

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    one-shotCross-repo trinity ONE SHOT lane

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions