fsdoc: no-summary-found
fsdoc: no-comment-found
let (is_subset_vec (#n:pos) (a:bv_t n) (b:bv_t n)):forall i:nat.{:pattern } ==>(<(i, n), ==>(=(index b i, false), =(index a i, false)))is_subset_vec is the property that the zero bits of b are also zero in a. I.e. that a is a subset of b.
let (is_superset_vec (#n:pos) (a:bv_t n) (b:bv_t n)):forall i:nat.{:pattern } ==>(<(i, n), ==>(=(index b i, true), =(index a i, true)))is_superset_vec is the property that the non-zero bits of b are also non-zero in a. I.e. that a is a superset of b.
val lemma_slice_subset_vec:Unidentified product: [#n:pos] Unidentified product: [a:bv_t n] Unidentified product: [b:bv_t n] Unidentified product: [i:nat] Unidentified product: [j:j:nat:{&&(<(i, j), <=(j, n))}] (Lemma ((requires is_subset_vec a b)) ((ensures (match n with 1 -> True | _ -> is_subset_vec #(-(j, i)) (slice a i j) (slice b i j)))))lemma_slice_subset_vec proves that the subset property is conserved in subslices.
val lemma_slice_superset_vec:Unidentified product: [#n:pos] Unidentified product: [a:bv_t n] Unidentified product: [b:bv_t n] Unidentified product: [i:nat] Unidentified product: [j:j:nat:{&&(<(i, j), <=(j, n))}] (Lemma ((requires is_superset_vec a b)) ((ensures (match n with 1 -> True | _ -> is_superset_vec #(-(j, i)) (slice a i j) (slice b i j)))))lemma_slice_superset_vec proves that the superset property is conserved in subslices.