Repository navigation
Tags: strandsrocq/strandsrocq
Tags
Announce the September 2026 release in the README
Implements the partial order semantics, as described in the paper sub… …mitted to JLAMP.
refactor: restructure bundle graph representation and modularize fram…
…ework
### Major Changes
- **Introduce `bundle_graph` record** (`Common/Bundles.v`): replaces the
flat `edge_set__t` bundle representation with a structured record
separating `nodes`, `intra` (intrastrand) and `inter` (interstrand)
edges. `is_bundle`, `is_sub`, and related predicates are updated
accordingly. Variable names `C` → `B` / `E` throughout.
- **New `Universe` abstraction** (`Common/Universe.v`, `Common/UniverseNat.v`):
introduces `UniverseSig` module type for the term universe, with a `nat`
instantiation.
- **Functor-based modularization**: core modules refactored as functors:
- `Common/StrandsTacticsFunctor.v` (rename of `StrandsTactics.v`)
- `Common/DefaultInstanceFunctor.v` (new; assembles tactics + bundle + MPT)
- `Common/EmbeddedTraceStrandsFunctor.v` (new; strand sig over nat-indexed
lists, replaces `StrandList`)
- **Replace `StrandList` with `EmbeddedTraceStrands`**
(`Instances/EmbeddedTraceStrands.v`): new instance wiring `TermNat` with
the embedded-trace strand space. `Instances/StrandList.v` deleted.
- **Simplify `DefaultInstances`**: now delegates entirely to
`MakeDefaultInstance` functor; removes redundant re-exports.
### Minor Changes
- `BundleRelations`: rename edge-set variable `C` → `E` in all lemmas for
clarity; add new lemmas `bundle_le_sub` and `bundle_le_union`.
- `Common/Strands.v`: remove `nodes_of`, `is_node_of`, `node_subset_of`,
`is_strand_of`, `is_sub`, and `is_edge_of_implies_is_node_of` from
`StrandSpaceSig` (now live in `BundleSig` / `DefaultInstanceFunctor`).
- `Instances/Penetrator.v`: update all bundle-section variables from
`C : edge_set__t` to `B : bundle_graph`; introduce local notation
`E := edges B`.
- All example files (`Examples/kmp`, `Examples/ns_original`,
`Examples/nsl`, `Examples/simple_auth`): updated imports and variable
names to match new bundle/instance structure.
- `dune` / `dune-project`: migrate from `(using coq 0.8)` /
`(lang dune 3.9)` to `(using rocq 0.11)` / `(lang dune 3.21)`;
switch `coq.theory` → `rocq.theory`.
- `README.md`: minor wording updates; drop `coq-core` installation
requirement from build instructions.