make pow opaque

[ahuoguo]

@parno spotted pow function is not marked as opaque even though it's revealed everywhere.

For context, Dafny standard library also did not mark it as opaque now, even though it was marked as opaque before.

Seems like part of the reason I did not mark opaque is because I wanted to reveal(pow) in the spec function of pow2

verus/source/vstd/arithmetic/power2.rs

Lines 26 to 37 in 20c3b08

	pub open spec fn pow2(e: nat) -> nat
	decreases
	e // ensures pow2(e) > 0
	// cannot have ensurs clause in spec functions
	// a workaround is the lemma_pow2_pos below
	,
	{
	// you cannot reveal in a spec function, which cause more reveals clauses
	// for the proof
	// reveal(pow);
	pow(2, e) as nat
	}

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[parno]

This seems like the right, conservative thing to do. Can you check on veritas to see how much it breaks?