@@ -205,11 +205,11 @@ sar = op2 SAR (\x y ->
205205-- | Extracts the byte at a given index from a Buf.
206206--
207207-- We do our best to return a concrete value wherever possible, but fallback to
208- -- an abstract expresion if nescessary . Note that a Buf is an infinite
208+ -- an abstract expression if necessary . Note that a Buf is an infinite
209209-- structure, so reads outside of the bounds of a ConcreteBuf return 0. This is
210210-- inline with the semantics of calldata and memory, but not of returndata.
211211
212- -- fuly concrete reads
212+ -- fully concrete reads
213213readByte :: Expr EWord -> Expr Buf -> Expr Byte
214214readByte (Lit x) (ConcreteBuf b)
215215 = if x <= unsafeInto (maxBound :: Int ) && i < BS. length b
@@ -235,7 +235,7 @@ readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst
235235 then readByte (Lit $ x - (dstOffset - srcOffset)) src
236236 else readByte i dst
237237readByte i@ (Lit x) buf@ (CopySlice _ (Lit dstOffset) (Lit size) _ dst)
238- -- the byte we are trying to read is compeletely outside of the sliced region
238+ -- the byte we are trying to read is completely outside of the sliced region
239239 = if x - dstOffset >= size
240240 then readByte i dst
241241 else ReadByte (Lit x) buf
@@ -269,7 +269,7 @@ readWord idx b@(WriteWord idx' val buf)
269269readWord (Lit idx) b@ (CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst)
270270 -- the region we are trying to read is enclosed in the sliced region
271271 | (idx - dstOff) < size && 32 <= size - (idx - dstOff) = readWord (Lit $ srcOff + (idx - dstOff)) src
272- -- the region we are trying to read is compeletely outside of the sliced region
272+ -- the region we are trying to read is completely outside of the sliced region
273273 | (idx - dstOff) >= size && (idx - dstOff) <= (maxBound :: W256 ) - 31 = readWord (Lit idx) dst
274274 -- the region we are trying to read partially overlaps the sliced region
275275 | otherwise = readWordFromBytes (Lit idx) b
@@ -343,7 +343,7 @@ copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e
343343-- copying 32 bytes can be rewritten to a WriteWord on dst (e.g. CODECOPY of args during constructors)
344344copySlice srcOffset dstOffset (Lit 32 ) src dst = writeWord dstOffset (readWord srcOffset src) dst
345345
346- -- concrete indicies & abstract src (may produce a concrete result if we are
346+ -- concrete indices & abstract src (may produce a concrete result if we are
347347-- copying from a concrete region of src)
348348copySlice s@ (Lit srcOffset) d@ (Lit dstOffset) sz@ (Lit size) src ds@ (ConcreteBuf dst)
349349 | dstOffset < maxBytes, size < maxBytes, srcOffset + (size- 1 ) > srcOffset = let
@@ -355,7 +355,7 @@ copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf
355355 else CopySlice s d sz src ds
356356 | otherwise = CopySlice s d sz src ds
357357
358- -- abstract indicies
358+ -- abstract indices
359359copySlice srcOffset dstOffset size src dst = CopySlice srcOffset dstOffset size src dst
360360
361361
@@ -412,7 +412,7 @@ writeWord offset val src = WriteWord offset val src
412412-- | Returns the length of a given buffer
413413--
414414-- If there are any writes to abstract locations, or CopySlices with an
415- -- abstract size or dstOffset, an abstract expresion will be returned.
415+ -- abstract size or dstOffset, an abstract expression will be returned.
416416bufLength :: Expr Buf -> Expr EWord
417417bufLength = bufLengthEnv mempty False
418418
@@ -473,12 +473,12 @@ concretePrefix b = V.create $ do
473473 inputLen = case bufLength b of
474474 Lit s -> if s > maxIdx
475475 then internalError " concretePrefix: input buffer size exceeds 500mb"
476- -- unafeInto : s is <= 500,000,000
476+ -- unsafeInto : s is <= 500,000,000
477477 else Just (unsafeInto s)
478478 _ -> Nothing
479479
480- -- recursively reads succesive bytes from `b` until we reach a symbolic
481- -- byte returns the larged index read from and a reference to the mutable
480+ -- recursively reads successive bytes from `b` until we reach a symbolic
481+ -- byte returns the large index read from and a reference to the mutable
482482 -- vec (might not be the same as the input because of the call to grow)
483483 go :: forall s . Int -> MVector s Word8 -> ST s (Int , MVector s Word8 )
484484 go i v
@@ -529,7 +529,7 @@ toList buf = case bufLength buf of
529529fromList :: V. Vector (Expr Byte ) -> Expr Buf
530530fromList bs = case Prelude. and (fmap isLitByte bs) of
531531 True -> ConcreteBuf . BS. pack . V. toList . V. mapMaybe maybeLitByte $ bs
532- -- we want to minimize the size of the resulting expresion , so we do two passes:
532+ -- we want to minimize the size of the resulting expression , so we do two passes:
533533 -- 1. write all concrete bytes to some base buffer
534534 -- 2. write all symbolic writes on top of this buffer
535535 -- this is safe because each write in the input vec is to a single byte at a distinct location
@@ -640,7 +640,7 @@ readStorage w st = go (simplify w) st
640640
641641 -- the chance of adding a value <= 2^32 to any given keccack output
642642 -- leading to an overflow is effectively zero. the chance of an overflow
643- -- occuring here is 2^32/2^256 = 2^-224, which is close enough to zero
643+ -- occurring here is 2^32/2^256 = 2^-224, which is close enough to zero
644644 -- for our purposes. This lets us completely simplify reads from write
645645 -- chains involving writes to arrays at literal offsets.
646646 (Lit a, Add (Lit b) (Keccak _) ) | a < 256 , b < maxW32 -> go slot prev
@@ -1147,7 +1147,7 @@ simplifyProp prop =
11471147 where
11481148 go :: Prop -> Prop
11491149
1150- -- LT/LEq comparisions
1150+ -- LT/LEq comparisons
11511151 go (PLT (Var _) (Lit 0 )) = PBool False
11521152 go (PLEq (Lit 0 ) (Var _)) = PBool True
11531153 go (PLT (Lit val) (Var _)) | val == maxLit = PBool False
@@ -1298,7 +1298,7 @@ indexWord :: Expr EWord -> Expr EWord -> Expr Byte
12981298-- Simplify masked reads:
12991299--
13001300--
1301- -- reads across the mask boundry
1301+ -- reads across the mask boundary
13021302-- return an abstract expression
13031303-- │
13041304-- │
@@ -1322,7 +1322,7 @@ indexWord :: Expr EWord -> Expr EWord -> Expr Byte
13221322-- indexWord 31 reads from the LSB
13231323--
13241324indexWord i@ (Lit idx) e@ (And (Lit mask) w)
1325- -- if the mask is all 1s then read from the undelrying word
1325+ -- if the mask is all 1s then read from the underlying word
13261326 -- we need this case to avoid overflow
13271327 | mask == fullWordMask = indexWord (Lit idx) w
13281328 -- if the index is a read from the masked region then read from the underlying word
@@ -1337,7 +1337,7 @@ indexWord i@(Lit idx) e@(And (Lit mask) w)
13371337 , isByteAligned mask
13381338 , idx < unmaskedBytes
13391339 = LitByte 0
1340- -- if the mask is not a power of 2, or it does not align with a byte boundry return an abstract expression
1340+ -- if the mask is not a power of 2, or it does not align with a byte boundary return an abstract expression
13411341 | idx <= 31 = IndexWord i e
13421342 -- reads outside the range of the source word return 0
13431343 | otherwise = LitByte 0
0 commit comments