MCPcopy Create free account
hub / github.com/argumentcomputer/ix / prop_univ_eq_implies_geq_both_ways

Function prop_univ_eq_implies_geq_both_ways

crates/kernel/src/level.rs:1108–1124  ·  view source on GitHub ↗
()

Source from the content-addressed store, hash-verified

1106 }
1107
1108 // =========================================================================
1109 // Property-style tests for universe-level algebra invariants.
1110 //
1111 // Use a deterministic seeded generator (xorshift) to produce randomized
1112 // `KUniv<Anon>` values of bounded depth and check algebraic laws:
1113 // reflexivity, symmetry of equality, transitivity of geq, and interaction
1114 // between geq and eq.
1115 // =========================================================================
1116
1117 struct UPrng(u64);
1118 impl UPrng {
1119 fn new(seed: u64) -> Self {
1120 UPrng(seed.wrapping_mul(0x9E37_79B9_7F4A_7C15) ^ 0xDEAD_BEEF_CAFE_BABE)
1121 }
1122 fn next_u64(&mut self) -> u64 {
1123 let mut x = self.0;
1124 x ^= x << 13;
1125 x ^= x >> 7;
1126 x ^= x << 17;
1127 self.0 = x;

Callers

nothing calls this directly

Calls 2

gen_univFunction · 0.85
univ_eqFunction · 0.85

Tested by

no test coverage detected